Theorem fvelrn

Description: A function's value belongs to its range. (Contributed by NM, 14-Oct-1996)

	Ref	Expression
Assertion	fvelrn	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ dom 𝐹 ↔ 𝐴 ∈ dom 𝐹 ) )
2	1	anbi2d	⊢ ( 𝑥 = 𝐴 → ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) ↔ ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) ) )
3		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
4	3	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 ↔ ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 ) )
5	2 4	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 ) ↔ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 ) ) )
6		funfvop	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 )
7		vex	⊢ 𝑥 ∈ V
8		opeq1	⊢ ( 𝑦 = 𝑥 → ⟨ 𝑦 , ( 𝐹 ‘ 𝑥 ) ⟩ = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ )
9	8	eleq1d	⊢ ( 𝑦 = 𝑥 → ( ⟨ 𝑦 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 ) )
10	7 9	spcev	⊢ ( ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 → ∃ 𝑦 ⟨ 𝑦 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 )
11	6 10	syl	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ∃ 𝑦 ⟨ 𝑦 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 )
12		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
13	12	elrn2	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 ↔ ∃ 𝑦 ⟨ 𝑦 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝐹 )
14	11 13	sylibr	⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
15	5 14	vtoclg	⊢ ( 𝐴 ∈ dom 𝐹 → ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 ) )
16	15	anabsi7	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )