Theorem opabdm

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

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

Proof

Step	Hyp	Ref	Expression
1		df-dm	$$⊢\mathrm{dom}R=\left\{x|\exists yxRy\right\}$$
2		nfopab1	$$⊢\underset{\_}{Ⅎ}x\left\{⟨x,y⟩|\phi \right\}$$
3	2	nfeq2	$$⊢ℲxR=\left\{⟨x,y⟩|\phi \right\}$$
4		nfopab2	$$⊢\underset{\_}{Ⅎ}y\left\{⟨x,y⟩|\phi \right\}$$
5	4	nfeq2	$$⊢ℲyR=\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	syl5bb	$$⊢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 yxRy\leftrightarrow \exists y\phi \right)$$
12	3 11	abbid	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \left\{x|\exists yxRy\right\}=\left\{x|\exists y\phi \right\}$$
13	1 12	eqtrid	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \mathrm{dom}R=\left\{x|\exists y\phi \right\}$$