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 ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ ran ⁡ F

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ x = A → x ∈ dom ⁡ F ↔ A ∈ dom ⁡ F
2 1 anbi2d ⊢ x = A → Fun ⁡ F ∧ x ∈ dom ⁡ F ↔ Fun ⁡ F ∧ A ∈ dom ⁡ F
3 fveq2 ⊢ x = A → F ⁡ x = F ⁡ A
4 3 eleq1d ⊢ x = A → F ⁡ x ∈ ran ⁡ F ↔ F ⁡ A ∈ ran ⁡ F
5 2 4 imbi12d ⊢ x = A → Fun ⁡ F ∧ x ∈ dom ⁡ F → F ⁡ x ∈ ran ⁡ F ↔ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ ran ⁡ F
6 funfvop ⊢ Fun ⁡ F ∧ x ∈ dom ⁡ F → x F ⁡ x ∈ F
7 vex ⊢ x ∈ V
8 opeq1 ⊢ y = x → y F ⁡ x = x F ⁡ x
9 8 eleq1d ⊢ y = x → y F ⁡ x ∈ F ↔ x F ⁡ x ∈ F
10 7 9 spcev ⊢ x F ⁡ x ∈ F → ∃ y y F ⁡ x ∈ F
11 6 10 syl ⊢ Fun ⁡ F ∧ x ∈ dom ⁡ F → ∃ y y F ⁡ x ∈ F
12 fvex ⊢ F ⁡ x ∈ V
13 12 elrn2 ⊢ F ⁡ x ∈ ran ⁡ F ↔ ∃ y y F ⁡ x ∈ F
14 11 13 sylibr ⊢ Fun ⁡ F ∧ x ∈ dom ⁡ F → F ⁡ x ∈ ran ⁡ F
15 5 14 vtoclg ⊢ A ∈ dom ⁡ F → Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ ran ⁡ F
16 15 anabsi7 ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ ran ⁡ F