# Metamath Proof Explorer

## Theorem fvelrn

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

Ref Expression
Assertion fvelrn ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to {F}\left({A}\right)\in \mathrm{ran}{F}$

### Proof

Step Hyp Ref Expression
1 eleq1 ${⊢}{x}={A}\to \left({x}\in \mathrm{dom}{F}↔{A}\in \mathrm{dom}{F}\right)$
2 1 anbi2d ${⊢}{x}={A}\to \left(\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)↔\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\right)$
3 fveq2 ${⊢}{x}={A}\to {F}\left({x}\right)={F}\left({A}\right)$
4 3 eleq1d ${⊢}{x}={A}\to \left({F}\left({x}\right)\in \mathrm{ran}{F}↔{F}\left({A}\right)\in \mathrm{ran}{F}\right)$
5 2 4 imbi12d ${⊢}{x}={A}\to \left(\left(\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)\to {F}\left({x}\right)\in \mathrm{ran}{F}\right)↔\left(\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to {F}\left({A}\right)\in \mathrm{ran}{F}\right)\right)$
6 funfvop ${⊢}\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)\to ⟨{x},{F}\left({x}\right)⟩\in {F}$
7 vex ${⊢}{x}\in \mathrm{V}$
8 opeq1 ${⊢}{y}={x}\to ⟨{y},{F}\left({x}\right)⟩=⟨{x},{F}\left({x}\right)⟩$
9 8 eleq1d ${⊢}{y}={x}\to \left(⟨{y},{F}\left({x}\right)⟩\in {F}↔⟨{x},{F}\left({x}\right)⟩\in {F}\right)$
10 7 9 spcev ${⊢}⟨{x},{F}\left({x}\right)⟩\in {F}\to \exists {y}\phantom{\rule{.4em}{0ex}}⟨{y},{F}\left({x}\right)⟩\in {F}$
11 6 10 syl ${⊢}\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}⟨{y},{F}\left({x}\right)⟩\in {F}$
12 fvex ${⊢}{F}\left({x}\right)\in \mathrm{V}$
13 12 elrn2 ${⊢}{F}\left({x}\right)\in \mathrm{ran}{F}↔\exists {y}\phantom{\rule{.4em}{0ex}}⟨{y},{F}\left({x}\right)⟩\in {F}$
14 11 13 sylibr ${⊢}\left(\mathrm{Fun}{F}\wedge {x}\in \mathrm{dom}{F}\right)\to {F}\left({x}\right)\in \mathrm{ran}{F}$
15 5 14 vtoclg ${⊢}{A}\in \mathrm{dom}{F}\to \left(\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to {F}\left({A}\right)\in \mathrm{ran}{F}\right)$
16 15 anabsi7 ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\in \mathrm{dom}{F}\right)\to {F}\left({A}\right)\in \mathrm{ran}{F}$