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