Metamath Proof Explorer

Theorem fvelrnb

Description: A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995)

Ref Expression
Assertion fvelrnb ${⊢}{F}Fn{A}\to \left({B}\in \mathrm{ran}{F}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={B}\right)$

Proof

Step Hyp Ref Expression
1 fnrnfv ${⊢}{F}Fn{A}\to \mathrm{ran}{F}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}$
2 1 eleq2d ${⊢}{F}Fn{A}\to \left({B}\in \mathrm{ran}{F}↔{B}\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}\right)$
3 fvex ${⊢}{F}\left({x}\right)\in \mathrm{V}$
4 eleq1 ${⊢}{F}\left({x}\right)={B}\to \left({F}\left({x}\right)\in \mathrm{V}↔{B}\in \mathrm{V}\right)$
5 3 4 mpbii ${⊢}{F}\left({x}\right)={B}\to {B}\in \mathrm{V}$
6 5 rexlimivw ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={B}\to {B}\in \mathrm{V}$
7 eqeq1 ${⊢}{y}={B}\to \left({y}={F}\left({x}\right)↔{B}={F}\left({x}\right)\right)$
8 eqcom ${⊢}{B}={F}\left({x}\right)↔{F}\left({x}\right)={B}$
9 7 8 syl6bb ${⊢}{y}={B}\to \left({y}={F}\left({x}\right)↔{F}\left({x}\right)={B}\right)$
10 9 rexbidv ${⊢}{y}={B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={B}\right)$
11 6 10 elab3 ${⊢}{B}\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={B}$
12 2 11 syl6bb ${⊢}{F}Fn{A}\to \left({B}\in \mathrm{ran}{F}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={B}\right)$