This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 )