This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. C /\ B e. D ) -> ( A. z A. w ( ( z = A /\ w = B ) -> ph ) <-> [. A / z ]. [. B / w ]. ph ) )

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 ) -> ph ) <-> ( ( z = x /\ w = B ) -> ph ) ) )
4 3 2albidv 
 |-  ( y = B -> ( A. z A. w ( ( z = x /\ w = y ) -> ph ) <-> A. z A. w ( ( z = x /\ w = B ) -> ph ) ) )
5 dfsbcq 
 |-  ( y = B -> ( [. y / w ]. ph <-> [. B / w ]. ph ) )
6 5 sbcbidv 
 |-  ( y = B -> ( [. x / z ]. [. y / w ]. ph <-> [. x / z ]. [. B / w ]. ph ) )
7 4 6 bibi12d 
 |-  ( y = B -> ( ( A. z A. w ( ( z = x /\ w = y ) -> ph ) <-> [. x / z ]. [. y / w ]. ph ) <-> ( A. z A. w ( ( z = x /\ w = B ) -> ph ) <-> [. x / z ]. [. B / w ]. ph ) ) )
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 ) -> ph ) <-> ( ( z = A /\ w = B ) -> ph ) ) )
11 10 2albidv 
 |-  ( x = A -> ( A. z A. w ( ( z = x /\ w = B ) -> ph ) <-> A. z A. w ( ( z = A /\ w = B ) -> ph ) ) )
12 dfsbcq 
 |-  ( x = A -> ( [. x / z ]. [. B / w ]. ph <-> [. A / z ]. [. B / w ]. ph ) )
13 11 12 bibi12d 
 |-  ( x = A -> ( ( A. z A. w ( ( z = x /\ w = B ) -> ph ) <-> [. x / z ]. [. B / w ]. ph ) <-> ( A. z A. w ( ( z = A /\ w = B ) -> ph ) <-> [. A / z ]. [. B / w ]. ph ) ) )
14 vex 
 |-  x e. _V
15 14 sbc6 
 |-  ( [. x / z ]. [. y / w ]. ph <-> A. z ( z = x -> [. y / w ]. ph ) )
16 19.21v 
 |-  ( A. w ( z = x -> ( w = y -> ph ) ) <-> ( z = x -> A. w ( w = y -> ph ) ) )
17 impexp 
 |-  ( ( ( z = x /\ w = y ) -> ph ) <-> ( z = x -> ( w = y -> ph ) ) )
18 17 albii 
 |-  ( A. w ( ( z = x /\ w = y ) -> ph ) <-> A. w ( z = x -> ( w = y -> ph ) ) )
19 vex 
 |-  y e. _V
20 19 sbc6 
 |-  ( [. y / w ]. ph <-> A. w ( w = y -> ph ) )
21 20 imbi2i 
 |-  ( ( z = x -> [. y / w ]. ph ) <-> ( z = x -> A. w ( w = y -> ph ) ) )
22 16 18 21 3bitr4ri 
 |-  ( ( z = x -> [. y / w ]. ph ) <-> A. w ( ( z = x /\ w = y ) -> ph ) )
23 22 albii 
 |-  ( A. z ( z = x -> [. y / w ]. ph ) <-> A. z A. w ( ( z = x /\ w = y ) -> ph ) )
24 15 23 bitr2i 
 |-  ( A. z A. w ( ( z = x /\ w = y ) -> ph ) <-> [. x / z ]. [. y / w ]. ph )
25 7 13 24 vtocl2g 
 |-  ( ( B e. D /\ A e. C ) -> ( A. z A. w ( ( z = A /\ w = B ) -> ph ) <-> [. A / z ]. [. B / w ]. ph ) )
26 25 ancoms 
 |-  ( ( A e. C /\ B e. D ) -> ( A. z A. w ( ( z = A /\ w = B ) -> ph ) <-> [. A / z ]. [. B / w ]. ph ) )