Theorem rnmpt

Description: The range of a function in maps-to notation. (Contributed by Scott Fenton, 21-Mar-2011) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	rnmpt.1	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	rnmpt	$$⊢\mathrm{ran}F=\left\{y|\exists x\in Ay=B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rnmpt.1	$$⊢F=\left(x\in A⟼B\right)$$
2		rnopab	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}=\left\{y|\exists x\left(x\in A\wedge y=B\right)\right\}$$
3		df-mpt	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
4	1 3	eqtri	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
5	4	rneqi	$$⊢\mathrm{ran}F=\mathrm{ran}\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
6		df-rex	$$⊢\exists x\in Ay=B\leftrightarrow \exists x\left(x\in A\wedge y=B\right)$$
7	6	abbii	$$⊢\left\{y|\exists x\in Ay=B\right\}=\left\{y|\exists x\left(x\in A\wedge y=B\right)\right\}$$
8	2 5 7	3eqtr4i	$$⊢\mathrm{ran}F=\left\{y|\exists x\in Ay=B\right\}$$