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		vopelopabsb	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
33	26 31 32	vtocl2g	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ) )
34	16 22 33	pm5.21nii	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )

Metamath Proof Explorer

Theorem opelopabsb

Proof