# 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 ) )`