Metamath Proof Explorer

Theorem 2sbc6g

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

Ref Expression
Assertion 2sbc6g ⊢ 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 imbi1d ⊢ y = B → z = x ∧ w = y → φ ↔ z = x ∧ w = B → φ
4 3 2albidv ⊢ 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 imbi1d ⊢ x = A → z = x ∧ w = B → φ ↔ z = A ∧ w = B → φ
11 10 2albidv ⊢ 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 vex ⊢ x ∈ V
15 14 sbc6 ⊢ [˙x / z]˙ [˙y / w]˙ φ ↔ ∀ z z = x → [˙y / w]˙ φ
16 19.21v ⊢ ∀ w z = x → w = y → φ ↔ z = x → ∀ w w = y → φ
17 impexp ⊢ z = x ∧ w = y → φ ↔ z = x → w = y → φ
18 17 albii ⊢ ∀ w z = x ∧ w = y → φ ↔ ∀ w z = x → w = y → φ
19 vex ⊢ y ∈ V
20 19 sbc6 ⊢ [˙y / w]˙ φ ↔ ∀ w w = y → φ
21 20 imbi2i ⊢ z = x → [˙y / w]˙ φ ↔ z = x → ∀ w w = y → φ
22 16 18 21 3bitr4ri ⊢ z = x → [˙y / w]˙ φ ↔ ∀ w z = x ∧ w = y → φ
23 22 albii ⊢ ∀ z z = x → [˙y / w]˙ φ ↔ ∀ z ∀ w z = x ∧ w = y → φ
24 15 23 bitr2i ⊢ ∀ z ∀ w z = x ∧ w = y → φ ↔ [˙x / z]˙ [˙y / w]˙ φ
25 7 13 24 vtocl2g ⊢ B ∈ D ∧ A ∈ C → ∀ z ∀ w z = A ∧ w = B → φ ↔ [˙A / z]˙ [˙B / w]˙ φ
26 25 ancoms ⊢ A ∈ C ∧ B ∈ D → ∀ z ∀ w z = A ∧ w = B → φ ↔ [˙A / z]˙ [˙B / w]˙ φ