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 e. C /\ B e. D ) -> ( E. z E. 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 anbi1d 
 |-  ( y = B -> ( ( ( z = x /\ w = y ) /\ ph ) <-> ( ( z = x /\ w = B ) /\ ph ) ) )
4 3 2exbidv 
 |-  ( y = B -> ( E. z E. w ( ( z = x /\ w = y ) /\ ph ) <-> E. z E. 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 -> ( ( E. z E. w ( ( z = x /\ w = y ) /\ ph ) <-> [. x / z ]. [. y / w ]. ph ) <-> ( E. z E. 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 anbi1d 
 |-  ( x = A -> ( ( ( z = x /\ w = B ) /\ ph ) <-> ( ( z = A /\ w = B ) /\ ph ) ) )
11 10 2exbidv 
 |-  ( x = A -> ( E. z E. w ( ( z = x /\ w = B ) /\ ph ) <-> E. z E. 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 -> ( ( E. z E. w ( ( z = x /\ w = B ) /\ ph ) <-> [. x / z ]. [. B / w ]. ph ) <-> ( E. z E. w ( ( z = A /\ w = B ) /\ ph ) <-> [. A / z ]. [. B / w ]. ph ) ) )
14 sbc5 
 |-  ( [. x / z ]. [. y / w ]. ph <-> E. z ( z = x /\ [. y / w ]. ph ) )
15 19.42v 
 |-  ( E. w ( z = x /\ ( w = y /\ ph ) ) <-> ( z = x /\ E. w ( w = y /\ ph ) ) )
16 anass 
 |-  ( ( ( z = x /\ w = y ) /\ ph ) <-> ( z = x /\ ( w = y /\ ph ) ) )
17 16 exbii 
 |-  ( E. w ( ( z = x /\ w = y ) /\ ph ) <-> E. w ( z = x /\ ( w = y /\ ph ) ) )
18 sbc5 
 |-  ( [. y / w ]. ph <-> E. w ( w = y /\ ph ) )
19 18 anbi2i 
 |-  ( ( z = x /\ [. y / w ]. ph ) <-> ( z = x /\ E. w ( w = y /\ ph ) ) )
20 15 17 19 3bitr4ri 
 |-  ( ( z = x /\ [. y / w ]. ph ) <-> E. w ( ( z = x /\ w = y ) /\ ph ) )
21 20 exbii 
 |-  ( E. z ( z = x /\ [. y / w ]. ph ) <-> E. z E. w ( ( z = x /\ w = y ) /\ ph ) )
22 14 21 bitr2i 
 |-  ( E. z E. w ( ( z = x /\ w = y ) /\ ph ) <-> [. x / z ]. [. y / w ]. ph )
23 7 13 22 vtocl2g 
 |-  ( ( B e. D /\ A e. C ) -> ( E. z E. w ( ( z = A /\ w = B ) /\ ph ) <-> [. A / z ]. [. B / w ]. ph ) )
24 23 ancoms 
 |-  ( ( A e. C /\ B e. D ) -> ( E. z E. w ( ( z = A /\ w = B ) /\ ph ) <-> [. A / z ]. [. B / w ]. ph ) )