Metamath Proof Explorer


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