Theorem dmoprab

Description: The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995) (Revised by David Abernethy, 19-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		dfoprab2	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨w,z⟩|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}$$
2	1	dmeqi	$$⊢\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\mathrm{dom}\left\{⟨w,z⟩|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}$$
3		dmopab	$$⊢\mathrm{dom}\left\{⟨w,z⟩|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}=\left\{w|\exists z\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}$$
4		exrot3	$$⊢\exists z\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\exists z\left(w=⟨x,y⟩\wedge \phi \right)$$
5		19.42v	$$⊢\exists z\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(w=⟨x,y⟩\wedge \exists z\phi \right)$$
6	5	2exbii	$$⊢\exists x\exists y\exists z\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge \exists z\phi \right)$$
7	4 6	bitri	$$⊢\exists z\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge \exists z\phi \right)$$
8	7	abbii	$$⊢\left\{w|\exists z\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \exists z\phi \right)\right\}$$
9		df-opab	$$⊢\left\{⟨x,y⟩|\exists z\phi \right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \exists z\phi \right)\right\}$$
10	8 9	eqtr4i	$$⊢\left\{w|\exists z\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}=\left\{⟨x,y⟩|\exists z\phi \right\}$$
11	2 3 10	3eqtri	$$⊢\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨x,y⟩|\exists z\phi \right\}$$