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	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	opnzi	⊢ ⟨ 𝑥 , 𝑦 ⟩ ≠ ∅
4		simpl	⊢ ( ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ∅ = ⟨ 𝑥 , 𝑦 ⟩ )
5	4	eqcomd	⊢ ( ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ⟨ 𝑥 , 𝑦 ⟩ = ∅ )
6	5	necon3ai	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ≠ ∅ → ¬ ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
7	3 6	ax-mp	⊢ ¬ ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
8	7	nex	⊢ ¬ ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
9	8	nex	⊢ ¬ ∃ 𝑥 ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
10		elopab	⊢ ( ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
11	9 10	mtbir	⊢ ¬ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
12		eleq1	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ∅ → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∅ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
13	11 12	mtbiri	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ∅ → ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
14	13	necon2ai	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ⟨ 𝐴 , 𝐵 ⟩ ≠ ∅ )
15		opnz	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ∅ ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
16	14 15	sylib	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
17		sbcex	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 → 𝐴 ∈ V )
18		spesbc	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 → ∃ 𝑥 [ 𝐵 / 𝑦 ] 𝜑 )
19		sbcex	⊢ ( [ 𝐵 / 𝑦 ] 𝜑 → 𝐵 ∈ V )
20	19	exlimiv	⊢ ( ∃ 𝑥 [ 𝐵 / 𝑦 ] 𝜑 → 𝐵 ∈ V )
21	18 20	syl	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 → 𝐵 ∈ V )
22	17 21	jca	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
23		opeq1	⊢ ( 𝑧 = 𝐴 → ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝐴 , 𝑤 ⟩ )
24	23	eleq1d	⊢ ( 𝑧 = 𝐴 → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ⟨ 𝐴 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
25		dfsbcq2	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) )
26	24 25	bibi12d	⊢ ( 𝑧 = 𝐴 → ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ( ⟨ 𝐴 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ) )
27		opeq2	⊢ ( 𝑤 = 𝐵 → ⟨ 𝐴 , 𝑤 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
28	27	eleq1d	⊢ ( 𝑤 = 𝐵 → ( ⟨ 𝐴 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
29		dfsbcq2	⊢ ( 𝑤 = 𝐵 → ( [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] 𝜑 ) )
30	29	sbcbidv	⊢ ( 𝑤 = 𝐵 → ( [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) )
31	28 30	bibi12d	⊢ ( 𝑤 = 𝐵 → ( ( ⟨ 𝐴 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) ) )
32		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
33	32	nfel2	⊢ Ⅎ 𝑥 ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
34		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑
35	33 34	nfbi	⊢ Ⅎ 𝑥 ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
36		opeq1	⊢ ( 𝑥 = 𝑧 → ⟨ 𝑥 , 𝑤 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ )
37	36	eleq1d	⊢ ( 𝑥 = 𝑧 → ( ⟨ 𝑥 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
38		sbequ12	⊢ ( 𝑥 = 𝑧 → ( [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) )
39	37 38	bibi12d	⊢ ( 𝑥 = 𝑧 → ( ( ⟨ 𝑥 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ) )
40		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
41	40	nfel2	⊢ Ⅎ 𝑦 ⟨ 𝑥 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
42		nfs1v	⊢ Ⅎ 𝑦 [ 𝑤 / 𝑦 ] 𝜑
43	41 42	nfbi	⊢ Ⅎ 𝑦 ( ⟨ 𝑥 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑤 / 𝑦 ] 𝜑 )
44		opeq2	⊢ ( 𝑦 = 𝑤 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑤 ⟩ )
45	44	eleq1d	⊢ ( 𝑦 = 𝑤 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ⟨ 𝑥 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
46		sbequ12	⊢ ( 𝑦 = 𝑤 → ( 𝜑 ↔ [ 𝑤 / 𝑦 ] 𝜑 ) )
47	45 46	bibi12d	⊢ ( 𝑦 = 𝑤 → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜑 ) ↔ ( ⟨ 𝑥 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑤 / 𝑦 ] 𝜑 ) ) )
48		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜑 )
49	43 47 48	chvarfv	⊢ ( ⟨ 𝑥 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑤 / 𝑦 ] 𝜑 )
50	35 39 49	chvarfv	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
51	26 31 50	vtocl2g	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) )
52	16 22 51	pm5.21nii	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )