Theorem opelopabsb

Description: The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002) (Revised by Mario Carneiro, 18-Nov-2016)

	Ref	Expression
Assertion	opelopabsb	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2		vex	$$⊢y\in \mathrm{V}$$
3	1 2	opnzi	$$⊢⟨x,y⟩\ne \varnothing$$
4		simpl	$$⊢\left(\varnothing =⟨x,y⟩\wedge \phi \right)\to \varnothing =⟨x,y⟩$$
5	4	eqcomd	$$⊢\left(\varnothing =⟨x,y⟩\wedge \phi \right)\to ⟨x,y⟩=\varnothing$$
6	5	necon3ai	$$⊢⟨x,y⟩\ne \varnothing \to \neg \left(\varnothing =⟨x,y⟩\wedge \phi \right)$$
7	3 6	ax-mp	$$⊢\neg \left(\varnothing =⟨x,y⟩\wedge \phi \right)$$
8	7	nex	$$⊢\neg \exists y\left(\varnothing =⟨x,y⟩\wedge \phi \right)$$
9	8	nex	$$⊢\neg \exists x\exists y\left(\varnothing =⟨x,y⟩\wedge \phi \right)$$
10		elopab	$$⊢\varnothing \in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(\varnothing =⟨x,y⟩\wedge \phi \right)$$
11	9 10	mtbir	$$⊢\neg \varnothing \in \left\{⟨x,y⟩|\phi \right\}$$
12		eleq1	$$⊢⟨A,B⟩=\varnothing \to \left(⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \varnothing \in \left\{⟨x,y⟩|\phi \right\}\right)$$
13	11 12	mtbiri	$$⊢⟨A,B⟩=\varnothing \to \neg ⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}$$
14	13	necon2ai	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\to ⟨A,B⟩\ne \varnothing$$
15		opnz	$$⊢⟨A,B⟩\ne \varnothing \leftrightarrow \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
16	14 15	sylib	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
17		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \to A\in \mathrm{V}$$
18		spesbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \to \exists x\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi$$
19		sbcex	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \to B\in \mathrm{V}$$
20	19	exlimiv	$$⊢\exists x\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \to B\in \mathrm{V}$$
21	18 20	syl	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \to B\in \mathrm{V}$$
22	17 21	jca	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
23		opeq1	$$⊢z=A\to ⟨z,w⟩=⟨A,w⟩$$
24	23	eleq1d	$$⊢z=A\to \left(⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow ⟨A,w⟩\in \left\{⟨x,y⟩|\phi \right\}\right)$$
25		dfsbcq2	$$⊢z=A\to \left(\left[z/x\right]\left[w/y\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left[w/y\right]\phi \right)$$
26	24 25	bibi12d	$$⊢z=A\to \left(\left(⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \left[z/x\right]\left[w/y\right]\phi \right)\leftrightarrow \left(⟨A,w⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left[w/y\right]\phi \right)\right)$$
27		opeq2	$$⊢w=B\to ⟨A,w⟩=⟨A,B⟩$$
28	27	eleq1d	$$⊢w=B\to \left(⟨A,w⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow ⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\right)$$
29		dfsbcq2	$$⊢w=B\to \left(\left[w/y\right]\phi \leftrightarrow \underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \right)$$
30	29	sbcbidv	$$⊢w=B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left[w/y\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \right)$$
31	28 30	bibi12d	$$⊢w=B\to \left(\left(⟨A,w⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left[w/y\right]\phi \right)\leftrightarrow \left(⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \right)\right)$$
32		vopelopabsb	$$⊢⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \left[z/x\right]\left[w/y\right]\phi$$
33	26 31 32	vtocl2g	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \right)$$
34	16 22 33	pm5.21nii	$$⊢⟨A,B⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi$$