Theorem rnoprab

Description: The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004) (Revised by David Abernethy, 19-Apr-2013)

	Ref	Expression
Assertion	rnoprab	$$⊢\mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{z|\exists x\exists y\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfoprab2	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨w,z⟩|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}$$
2	1	rneqi	$$⊢\mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\mathrm{ran}\left\{⟨w,z⟩|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}$$
3		rnopab	$$⊢\mathrm{ran}\left\{⟨w,z⟩|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}=\left\{z|\exists w\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}$$
4		exrot3	$$⊢\exists w\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\exists w\left(w=⟨x,y⟩\wedge \phi \right)$$
5		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
6	5	isseti	$$⊢\exists ww=⟨x,y⟩$$
7		19.41v	$$⊢\exists w\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(\exists ww=⟨x,y⟩\wedge \phi \right)$$
8	6 7	mpbiran	$$⊢\exists w\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \phi$$
9	8	2exbii	$$⊢\exists x\exists y\exists w\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\phi$$
10	4 9	bitri	$$⊢\exists w\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\phi$$
11	10	abbii	$$⊢\left\{z|\exists w\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}=\left\{z|\exists x\exists y\phi \right\}$$
12	2 3 11	3eqtri	$$⊢\mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{z|\exists x\exists y\phi \right\}$$