Theorem dmopab3

Description: The domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004)

	Ref	Expression
Assertion	dmopab3	$$⊢\forall x\in A\exists y\phi \leftrightarrow \mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		df-ral	$$⊢\forall x\in A\exists y\phi \leftrightarrow \forall x\left(x\in A\to \exists y\phi \right)$$
2		pm4.71	$$⊢\left(x\in A\to \exists y\phi \right)\leftrightarrow \left(x\in A\leftrightarrow \left(x\in A\wedge \exists y\phi \right)\right)$$
3	2	albii	$$⊢\forall x\left(x\in A\to \exists y\phi \right)\leftrightarrow \forall x\left(x\in A\leftrightarrow \left(x\in A\wedge \exists y\phi \right)\right)$$
4		dmopab	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}=\left\{x|\exists y\left(x\in A\wedge \phi \right)\right\}$$
5		19.42v	$$⊢\exists y\left(x\in A\wedge \phi \right)\leftrightarrow \left(x\in A\wedge \exists y\phi \right)$$
6	5	abbii	$$⊢\left\{x|\exists y\left(x\in A\wedge \phi \right)\right\}=\left\{x|\left(x\in A\wedge \exists y\phi \right)\right\}$$
7	4 6	eqtri	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}=\left\{x|\left(x\in A\wedge \exists y\phi \right)\right\}$$
8	7	eqeq1i	$$⊢\mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}=A\leftrightarrow \left\{x|\left(x\in A\wedge \exists y\phi \right)\right\}=A$$
9		eqcom	$$⊢A=\left\{x|\left(x\in A\wedge \exists y\phi \right)\right\}\leftrightarrow \left\{x|\left(x\in A\wedge \exists y\phi \right)\right\}=A$$
10		abeq2	$$⊢A=\left\{x|\left(x\in A\wedge \exists y\phi \right)\right\}\leftrightarrow \forall x\left(x\in A\leftrightarrow \left(x\in A\wedge \exists y\phi \right)\right)$$
11	8 9 10	3bitr2ri	$$⊢\forall x\left(x\in A\leftrightarrow \left(x\in A\wedge \exists y\phi \right)\right)\leftrightarrow \mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}=A$$
12	1 3 11	3bitri	$$⊢\forall x\in A\exists y\phi \leftrightarrow \mathrm{dom}\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}=A$$