Theorem dfoprab3s

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

	Ref	Expression
Assertion	dfoprab3s	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨w,z⟩|\left(w\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)\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		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi$$
3	2	19.41	$$⊢\exists x\left(\exists yw=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\exists x\exists yw=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
4		sbcopeq1a	$$⊢w=⟨x,y⟩\to \left(\underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
5	4	pm5.32i	$$⊢\left(w=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(w=⟨x,y⟩\wedge \phi \right)$$
6	5	exbii	$$⊢\exists y\left(w=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \exists y\left(w=⟨x,y⟩\wedge \phi \right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}y{1}^{st}\left(w\right)$$
8		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi$$
9	7 8	nfsbcw	$$⊢Ⅎy\underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi$$
10	9	19.41	$$⊢\exists y\left(w=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\exists yw=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
11	6 10	bitr3i	$$⊢\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(\exists yw=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
12	11	exbii	$$⊢\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\left(\exists yw=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
13		elvv	$$⊢w\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists yw=⟨x,y⟩$$
14	13	anbi1i	$$⊢\left(w\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\exists x\exists yw=⟨x,y⟩\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
15	3 12 14	3bitr4i	$$⊢\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(w\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)$$
16	15	opabbii	$$⊢\left\{⟨w,z⟩|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}=\left\{⟨w,z⟩|\left(w\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)\right\}$$
17	1 16	eqtri	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨w,z⟩|\left(w\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \underset{\dot{}}{[}{1}^{st}\left(w\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(w\right)/y\underset{\dot{}}{]}\phi \right)\right\}$$