Metamath Proof Explorer

Theorem 2sbc5g

Description: Theorem *13.22 in WhiteheadRussell p. 179. (Contributed by Andrew Salmon, 3-Jun-2011)

Ref Expression
Assertion 2sbc5g ⊢ A ∈ C ∧ B ∈ D → ∃ z ∃ w z = A ∧ w = B ∧ φ ↔ [˙A / z]˙ [˙B / w]˙ φ

Proof

Step Hyp Ref Expression
1 eqeq2 ⊢ y = B → w = y ↔ w = B
2 1 anbi2d ⊢ y = B → z = x ∧ w = y ↔ z = x ∧ w = B
3 2 anbi1d ⊢ y = B → z = x ∧ w = y ∧ φ ↔ z = x ∧ w = B ∧ φ
4 3 2exbidv ⊢ y = B → ∃ z ∃ w z = x ∧ w = y ∧ φ ↔ ∃ z ∃ w z = x ∧ w = B ∧ φ
5 dfsbcq ⊢ y = B → [˙y / w]˙ φ ↔ [˙B / w]˙ φ
6 5 sbcbidv ⊢ y = B → [˙x / z]˙ [˙y / w]˙ φ ↔ [˙x / z]˙ [˙B / w]˙ φ
7 4 6 bibi12d ⊢ y = B → ∃ z ∃ w z = x ∧ w = y ∧ φ ↔ [˙x / z]˙ [˙y / w]˙ φ ↔ ∃ z ∃ w z = x ∧ w = B ∧ φ ↔ [˙x / z]˙ [˙B / w]˙ φ
8 eqeq2 ⊢ x = A → z = x ↔ z = A
9 8 anbi1d ⊢ x = A → z = x ∧ w = B ↔ z = A ∧ w = B
10 9 anbi1d ⊢ x = A → z = x ∧ w = B ∧ φ ↔ z = A ∧ w = B ∧ φ
11 10 2exbidv ⊢ x = A → ∃ z ∃ w z = x ∧ w = B ∧ φ ↔ ∃ z ∃ w z = A ∧ w = B ∧ φ
12 dfsbcq ⊢ x = A → [˙x / z]˙ [˙B / w]˙ φ ↔ [˙A / z]˙ [˙B / w]˙ φ
13 11 12 bibi12d ⊢ x = A → ∃ z ∃ w z = x ∧ w = B ∧ φ ↔ [˙x / z]˙ [˙B / w]˙ φ ↔ ∃ z ∃ w z = A ∧ w = B ∧ φ ↔ [˙A / z]˙ [˙B / w]˙ φ
14 sbc5 ⊢ [˙x / z]˙ [˙y / w]˙ φ ↔ ∃ z z = x ∧ [˙y / w]˙ φ
15 19.42v ⊢ ∃ w z = x ∧ w = y ∧ φ ↔ z = x ∧ ∃ w w = y ∧ φ
16 anass ⊢ z = x ∧ w = y ∧ φ ↔ z = x ∧ w = y ∧ φ
17 16 exbii ⊢ ∃ w z = x ∧ w = y ∧ φ ↔ ∃ w z = x ∧ w = y ∧ φ
18 sbc5 ⊢ [˙y / w]˙ φ ↔ ∃ w w = y ∧ φ
19 18 anbi2i ⊢ z = x ∧ [˙y / w]˙ φ ↔ z = x ∧ ∃ w w = y ∧ φ
20 15 17 19 3bitr4ri ⊢ z = x ∧ [˙y / w]˙ φ ↔ ∃ w z = x ∧ w = y ∧ φ
21 20 exbii ⊢ ∃ z z = x ∧ [˙y / w]˙ φ ↔ ∃ z ∃ w z = x ∧ w = y ∧ φ
22 14 21 bitr2i ⊢ ∃ z ∃ w z = x ∧ w = y ∧ φ ↔ [˙x / z]˙ [˙y / w]˙ φ
23 7 13 22 vtocl2g ⊢ B ∈ D ∧ A ∈ C → ∃ z ∃ w z = A ∧ w = B ∧ φ ↔ [˙A / z]˙ [˙B / w]˙ φ
24 23 ancoms ⊢ A ∈ C ∧ B ∈ D → ∃ z ∃ w z = A ∧ w = B ∧ φ ↔ [˙A / z]˙ [˙B / w]˙ φ