# Metamath Proof Explorer

## Theorem 2sbc6g

Description: Theorem *13.21 in WhiteheadRussell p. 179. (Contributed by Andrew Salmon, 3-Jun-2011)

Ref Expression
Assertion 2sbc6g

### Proof

Step Hyp Ref Expression
1 eqeq2 ${⊢}{y}={B}\to \left({w}={y}↔{w}={B}\right)$
2 1 anbi2d ${⊢}{y}={B}\to \left(\left({z}={x}\wedge {w}={y}\right)↔\left({z}={x}\wedge {w}={B}\right)\right)$
3 2 imbi1d ${⊢}{y}={B}\to \left(\left(\left({z}={x}\wedge {w}={y}\right)\to {\phi }\right)↔\left(\left({z}={x}\wedge {w}={B}\right)\to {\phi }\right)\right)$
4 3 2albidv ${⊢}{y}={B}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({z}={x}\wedge {w}={y}\right)\to {\phi }\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({z}={x}\wedge {w}={B}\right)\to {\phi }\right)\right)$
5 dfsbcq
6 5 sbcbidv
7 4 6 bibi12d
8 eqeq2 ${⊢}{x}={A}\to \left({z}={x}↔{z}={A}\right)$
9 8 anbi1d ${⊢}{x}={A}\to \left(\left({z}={x}\wedge {w}={B}\right)↔\left({z}={A}\wedge {w}={B}\right)\right)$
10 9 imbi1d ${⊢}{x}={A}\to \left(\left(\left({z}={x}\wedge {w}={B}\right)\to {\phi }\right)↔\left(\left({z}={A}\wedge {w}={B}\right)\to {\phi }\right)\right)$
11 10 2albidv ${⊢}{x}={A}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({z}={x}\wedge {w}={B}\right)\to {\phi }\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({z}={A}\wedge {w}={B}\right)\to {\phi }\right)\right)$
12 dfsbcq
13 11 12 bibi12d
14 vex ${⊢}{x}\in \mathrm{V}$
15 14 sbc6
16 19.21v ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}={x}\to \left({w}={y}\to {\phi }\right)\right)↔\left({z}={x}\to \forall {w}\phantom{\rule{.4em}{0ex}}\left({w}={y}\to {\phi }\right)\right)$
17 impexp ${⊢}\left(\left({z}={x}\wedge {w}={y}\right)\to {\phi }\right)↔\left({z}={x}\to \left({w}={y}\to {\phi }\right)\right)$
18 17 albii ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left(\left({z}={x}\wedge {w}={y}\right)\to {\phi }\right)↔\forall {w}\phantom{\rule{.4em}{0ex}}\left({z}={x}\to \left({w}={y}\to {\phi }\right)\right)$
19 vex ${⊢}{y}\in \mathrm{V}$
20 19 sbc6
21 20 imbi2i
22 16 18 21 3bitr4ri
23 22 albii
24 15 23 bitr2i
25 7 13 24 vtocl2g
26 25 ancoms