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∃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 anbi1d ⊢y=B→z=x∧w=y∧φ↔z=x∧w=B∧φ
4 3 2exbidv ⊢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 anbi1d ⊢x=A→z=x∧w=B∧φ↔z=A∧w=B∧φ
11 10 2exbidv ⊢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 sbc5 ⊢[˙x/z]˙[˙y/w]˙φ↔∃zz=x∧[˙y/w]˙φ
15 19.42v ⊢∃wz=x∧w=y∧φ↔z=x∧∃ww=y∧φ
16 anass ⊢z=x∧w=y∧φ↔z=x∧w=y∧φ
17 16 exbii ⊢∃wz=x∧w=y∧φ↔∃wz=x∧w=y∧φ
18 sbc5 ⊢[˙y/w]˙φ↔∃ww=y∧φ
19 18 anbi2i ⊢z=x∧[˙y/w]˙φ↔z=x∧∃ww=y∧φ
20 15 17 19 3bitr4ri ⊢z=x∧[˙y/w]˙φ↔∃wz=x∧w=y∧φ
21 20 exbii ⊢∃zz=x∧[˙y/w]˙φ↔∃z∃wz=x∧w=y∧φ
22 14 21 bitr2i ⊢∃z∃wz=x∧w=y∧φ↔[˙x/z]˙[˙y/w]˙φ
23 7 13 22 vtocl2g ⊢B∈D∧A∈C→∃z∃wz=A∧w=B∧φ↔[˙A/z]˙[˙B/w]˙φ
24 23 ancoms ⊢A∈C∧B∈D→∃z∃wz=A∧w=B∧φ↔[˙A/z]˙[˙B/w]˙φ