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 ⊢ A B ∈ x y | φ ↔ [˙A / x]˙ [˙B / y]˙ φ

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 vex ⊢ y ∈ V
3 1 2 opnzi ⊢ x y ≠ ∅
4 simpl ⊢ ∅ = x y ∧ φ → ∅ = x y
5 4 eqcomd ⊢ ∅ = x y ∧ φ → x y = ∅
6 5 necon3ai ⊢ x y ≠ ∅ → ¬ ∅ = x y ∧ φ
7 3 6 ax-mp ⊢ ¬ ∅ = x y ∧ φ
8 7 nex ⊢ ¬ ∃ y ∅ = x y ∧ φ
9 8 nex ⊢ ¬ ∃ x ∃ y ∅ = x y ∧ φ
10 elopab ⊢ ∅ ∈ x y | φ ↔ ∃ x ∃ y ∅ = x y ∧ φ
11 9 10 mtbir ⊢ ¬ ∅ ∈ x y | φ
12 eleq1 ⊢ A B = ∅ → A B ∈ x y | φ ↔ ∅ ∈ x y | φ
13 11 12 mtbiri ⊢ A B = ∅ → ¬ A B ∈ x y | φ
14 13 necon2ai ⊢ A B ∈ x y | φ → A B ≠ ∅
15 opnz ⊢ A B ≠ ∅ ↔ A ∈ V ∧ B ∈ V
16 14 15 sylib ⊢ A B ∈ x y | φ → A ∈ V ∧ B ∈ V
17 sbcex ⊢ [˙A / x]˙ [˙B / y]˙ φ → A ∈ V
18 spesbc ⊢ [˙A / x]˙ [˙B / y]˙ φ → ∃ x [˙B / y]˙ φ
19 sbcex ⊢ [˙B / y]˙ φ → B ∈ V
20 19 exlimiv ⊢ ∃ x [˙B / y]˙ φ → B ∈ V
21 18 20 syl ⊢ [˙A / x]˙ [˙B / y]˙ φ → B ∈ V
22 17 21 jca ⊢ [˙A / x]˙ [˙B / y]˙ φ → A ∈ V ∧ B ∈ V
23 opeq1 ⊢ z = A → z w = A w
24 23 eleq1d ⊢ z = A → z w ∈ x y | φ ↔ A w ∈ x y | φ
25 dfsbcq2 ⊢ z = A → z x w y φ ↔ [˙A / x]˙ w y φ
26 24 25 bibi12d ⊢ z = A → z w ∈ x y | φ ↔ z x w y φ ↔ A w ∈ x y | φ ↔ [˙A / x]˙ w y φ
27 opeq2 ⊢ w = B → A w = A B
28 27 eleq1d ⊢ w = B → A w ∈ x y | φ ↔ A B ∈ x y | φ
29 dfsbcq2 ⊢ w = B → w y φ ↔ [˙B / y]˙ φ
30 29 sbcbidv ⊢ w = B → [˙A / x]˙ w y φ ↔ [˙A / x]˙ [˙B / y]˙ φ
31 28 30 bibi12d ⊢ w = B → A w ∈ x y | φ ↔ [˙A / x]˙ w y φ ↔ A B ∈ x y | φ ↔ [˙A / x]˙ [˙B / y]˙ φ
32 vopelopabsb ⊢ z w ∈ x y | φ ↔ z x w y φ
33 26 31 32 vtocl2g ⊢ A ∈ V ∧ B ∈ V → A B ∈ x y | φ ↔ [˙A / x]˙ [˙B / y]˙ φ
34 16 22 33 pm5.21nii ⊢ A B ∈ x y | φ ↔ [˙A / x]˙ [˙B / y]˙ φ