Theorem dmopab

Description: The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995) (Revised by Mario Carneiro, 4-Dec-2016)

	Ref	Expression
Assertion	dmopab	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\phi \right\}=\left\{x|\exists y\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	dfdmf	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\phi \right\}=\left\{x|\exists yx\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 yx\left\{⟨x,y⟩|\phi \right\}y\leftrightarrow \exists y\phi$$
8	7	abbii	$$⊢\left\{x|\exists yx\left\{⟨x,y⟩|\phi \right\}y\right\}=\left\{x|\exists y\phi \right\}$$
9	3 8	eqtri	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\phi \right\}=\left\{x|\exists y\phi \right\}$$