Theorem rnopab

Description: The range of a class of ordered pairs. (Contributed by NM, 14-Aug-1995) (Revised by Mario Carneiro, 4-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		nfopab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨x,y⟩|\phi \right\}$$
2		nfopab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨x,y⟩|\phi \right\}$$
3	1 2	dfrnf	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\phi \right\}=\left\{y|\exists xx\left\{⟨x,y⟩|\phi \right\}y\right\}$$
4		df-br	$$⊢x\left\{⟨x,y⟩|\phi \right\}y\leftrightarrow ⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}$$
5		opabidw	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \phi$$
6	4 5	bitri	$$⊢x\left\{⟨x,y⟩|\phi \right\}y\leftrightarrow \phi$$
7	6	exbii	$$⊢\exists xx\left\{⟨x,y⟩|\phi \right\}y\leftrightarrow \exists x\phi$$
8	7	abbii	$$⊢\left\{y|\exists xx\left\{⟨x,y⟩|\phi \right\}y\right\}=\left\{y|\exists x\phi \right\}$$
9	3 8	eqtri	$$⊢\mathrm{ran}\left\{⟨x,y⟩|\phi \right\}=\left\{y|\exists x\phi \right\}$$