# Metamath Proof Explorer

## Theorem fnasrn

Description: A function expressed as the range of another function. (Contributed by Mario Carneiro, 22-Jun-2013) (Proof shortened by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis dfmpt.1 ${⊢}{B}\in \mathrm{V}$
Assertion fnasrn ${⊢}\left({x}\in {A}⟼{B}\right)=\mathrm{ran}\left({x}\in {A}⟼⟨{x},{B}⟩\right)$

### Proof

Step Hyp Ref Expression
1 dfmpt.1 ${⊢}{B}\in \mathrm{V}$
2 1 dfmpt ${⊢}\left({x}\in {A}⟼{B}\right)=\bigcup _{{x}\in {A}}\left\{⟨{x},{B}⟩\right\}$
3 eqid ${⊢}\left({x}\in {A}⟼⟨{x},{B}⟩\right)=\left({x}\in {A}⟼⟨{x},{B}⟩\right)$
4 3 rnmpt ${⊢}\mathrm{ran}\left({x}\in {A}⟼⟨{x},{B}⟩\right)=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}=⟨{x},{B}⟩\right\}$
5 velsn ${⊢}{y}\in \left\{⟨{x},{B}⟩\right\}↔{y}=⟨{x},{B}⟩$
6 5 rexbii ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left\{⟨{x},{B}⟩\right\}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}=⟨{x},{B}⟩$
7 6 abbii ${⊢}\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left\{⟨{x},{B}⟩\right\}\right\}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}=⟨{x},{B}⟩\right\}$
8 4 7 eqtr4i ${⊢}\mathrm{ran}\left({x}\in {A}⟼⟨{x},{B}⟩\right)=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left\{⟨{x},{B}⟩\right\}\right\}$
9 df-iun ${⊢}\bigcup _{{x}\in {A}}\left\{⟨{x},{B}⟩\right\}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left\{⟨{x},{B}⟩\right\}\right\}$
10 8 9 eqtr4i ${⊢}\mathrm{ran}\left({x}\in {A}⟼⟨{x},{B}⟩\right)=\bigcup _{{x}\in {A}}\left\{⟨{x},{B}⟩\right\}$
11 2 10 eqtr4i ${⊢}\left({x}\in {A}⟼{B}\right)=\mathrm{ran}\left({x}\in {A}⟼⟨{x},{B}⟩\right)$