Theorem dfopab2

Description: A way to define an ordered-pair class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	dfopab2	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{z\in \left(\mathrm{V}\times \mathrm{V}\right)|\underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi$$
2	1	19.41	$$⊢\exists x\left(\exists yz=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\exists x\exists yz=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)$$
3		sbcopeq1a	$$⊢z=⟨x,y⟩\to \left(\underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
4	3	pm5.32i	$$⊢\left(z=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(z=⟨x,y⟩\wedge \phi \right)$$
5	4	exbii	$$⊢\exists y\left(z=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \exists y\left(z=⟨x,y⟩\wedge \phi \right)$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}y{1}^{st}\left(z\right)$$
7		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi$$
8	6 7	nfsbcw	$$⊢Ⅎy\underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi$$
9	8	19.41	$$⊢\exists y\left(z=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\exists yz=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)$$
10	5 9	bitr3i	$$⊢\exists y\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(\exists yz=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)$$
11	10	exbii	$$⊢\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\left(\exists yz=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)$$
12		elvv	$$⊢z\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists yz=⟨x,y⟩$$
13	12	anbi1i	$$⊢\left(z\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\exists x\exists yz=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)$$
14	2 11 13	3bitr4i	$$⊢\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(z\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)$$
15	14	abbii	$$⊢\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}=\left\{z|\left(z\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)\right\}$$
16		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$
17		df-rab	$$⊢\left\{z\in \left(\mathrm{V}\times \mathrm{V}\right)|\underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right\}=\left\{z|\left(z\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right)\right\}$$
18	15 16 17	3eqtr4i	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{z\in \left(\mathrm{V}\times \mathrm{V}\right)|\underset{\dot{}}{[}{1}^{st}\left(z\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(z\right)/y\underset{\dot{}}{]}\phi \right\}$$