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 Ay=⟨x,B⟩\right\}$$
5		velsn	$$⊢y\in \left\{⟨x,B⟩\right\}\leftrightarrow y=⟨x,B⟩$$
6	5	rexbii	$$⊢\exists x\in Ay\in \left\{⟨x,B⟩\right\}\leftrightarrow \exists x\in Ay=⟨x,B⟩$$
7	6	abbii	$$⊢\left\{y|\exists x\in Ay\in \left\{⟨x,B⟩\right\}\right\}=\left\{y|\exists x\in Ay=⟨x,B⟩\right\}$$
8	4 7	eqtr4i	$$⊢\mathrm{ran}\left(x\in A⟼⟨x,B⟩\right)=\left\{y|\exists x\in Ay\in \left\{⟨x,B⟩\right\}\right\}$$
9		df-iun	$$⊢\bigcup _{x\in A}\left\{⟨x,B⟩\right\}=\left\{y|\exists x\in Ay\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)$$