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∀wz=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∀wz=x∧w=y→φ↔∀z∀wz=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∀wz=x∧w=y→φ↔[˙x/z]˙[˙y/w]˙φ↔∀z∀wz=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∀wz=x∧w=B→φ↔∀z∀wz=A∧w=B→φ
12 dfsbcq ⊢x=A→[˙x/z]˙[˙B/w]˙φ↔[˙A/z]˙[˙B/w]˙φ
13 11 12 bibi12d ⊢x=A→∀z∀wz=x∧w=B→φ↔[˙x/z]˙[˙B/w]˙φ↔∀z∀wz=A∧w=B→φ↔[˙A/z]˙[˙B/w]˙φ
14 vex ⊢x∈V
15 14 sbc6 ⊢[˙x/z]˙[˙y/w]˙φ↔∀zz=x→[˙y/w]˙φ
16 19.21v ⊢∀wz=x→w=y→φ↔z=x→∀ww=y→φ
17 impexp ⊢z=x∧w=y→φ↔z=x→w=y→φ
18 17 albii ⊢∀wz=x∧w=y→φ↔∀wz=x→w=y→φ
19 vex ⊢y∈V
20 19 sbc6 ⊢[˙y/w]˙φ↔∀ww=y→φ
21 20 imbi2i ⊢z=x→[˙y/w]˙φ↔z=x→∀ww=y→φ
22 16 18 21 3bitr4ri ⊢z=x→[˙y/w]˙φ↔∀wz=x∧w=y→φ
23 22 albii ⊢∀zz=x→[˙y/w]˙φ↔∀z∀wz=x∧w=y→φ
24 15 23 bitr2i ⊢∀z∀wz=x∧w=y→φ↔[˙x/z]˙[˙y/w]˙φ
25 7 13 24 vtocl2g ⊢B∈D∧A∈C→∀z∀wz=A∧w=B→φ↔[˙A/z]˙[˙B/w]˙φ
26 25 ancoms ⊢A∈C∧B∈D→∀z∀wz=A∧w=B→φ↔[˙A/z]˙[˙B/w]˙φ