Metamath Proof Explorer

Theorem fnrnfv

Description: The range of a function expressed as a collection of the function's values. (Contributed by NM, 20-Oct-2005) (Proof shortened by Mario Carneiro, 31-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 dffn5 ${⊢}{F}Fn{A}↔{F}=\left({x}\in {A}⟼{F}\left({x}\right)\right)$
2 rneq ${⊢}{F}=\left({x}\in {A}⟼{F}\left({x}\right)\right)\to \mathrm{ran}{F}=\mathrm{ran}\left({x}\in {A}⟼{F}\left({x}\right)\right)$
3 1 2 sylbi ${⊢}{F}Fn{A}\to \mathrm{ran}{F}=\mathrm{ran}\left({x}\in {A}⟼{F}\left({x}\right)\right)$
4 eqid ${⊢}\left({x}\in {A}⟼{F}\left({x}\right)\right)=\left({x}\in {A}⟼{F}\left({x}\right)\right)$
5 4 rnmpt ${⊢}\mathrm{ran}\left({x}\in {A}⟼{F}\left({x}\right)\right)=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}$
6 3 5 syl6eq ${⊢}{F}Fn{A}\to \mathrm{ran}{F}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={F}\left({x}\right)\right\}$