Theorem opabrn

Description: Range of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017)

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

Proof

Step	Hyp	Ref	Expression
1		dfrn2	$$⊢\mathrm{ran}R=\left\{y|\exists xxRy\right\}$$
2		nfopab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨x,y⟩|\phi \right\}$$
3	2	nfeq2	$$⊢ℲyR=\left\{⟨x,y⟩|\phi \right\}$$
4		nfopab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨x,y⟩|\phi \right\}$$
5	4	nfeq2	$$⊢ℲxR=\left\{⟨x,y⟩|\phi \right\}$$
6		df-br	$$⊢xRy\leftrightarrow ⟨x,y⟩\in R$$
7		eleq2	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \left(⟨x,y⟩\in R\leftrightarrow ⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\right)$$
8		opabidw	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \phi$$
9	7 8	bitrdi	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \left(⟨x,y⟩\in R\leftrightarrow \phi \right)$$
10	6 9	bitrid	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \left(xRy\leftrightarrow \phi \right)$$
11	5 10	exbid	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \left(\exists xxRy\leftrightarrow \exists x\phi \right)$$
12	3 11	abbid	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \left\{y|\exists xxRy\right\}=\left\{y|\exists x\phi \right\}$$
13	1 12	eqtrid	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \mathrm{ran}R=\left\{y|\exists x\phi \right\}$$