# Metamath Proof Explorer

## Theorem 2sbc5g

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

Ref Expression
Assertion 2sbc5g

### 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 anbi1d ${⊢}{y}={B}\to \left(\left(\left({z}={x}\wedge {w}={y}\right)\wedge {\phi }\right)↔\left(\left({z}={x}\wedge {w}={B}\right)\wedge {\phi }\right)\right)$
4 3 2exbidv ${⊢}{y}={B}\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left(\left({z}={x}\wedge {w}={y}\right)\wedge {\phi }\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left(\left({z}={x}\wedge {w}={B}\right)\wedge {\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 anbi1d ${⊢}{x}={A}\to \left(\left(\left({z}={x}\wedge {w}={B}\right)\wedge {\phi }\right)↔\left(\left({z}={A}\wedge {w}={B}\right)\wedge {\phi }\right)\right)$
11 10 2exbidv ${⊢}{x}={A}\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left(\left({z}={x}\wedge {w}={B}\right)\wedge {\phi }\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left(\left({z}={A}\wedge {w}={B}\right)\wedge {\phi }\right)\right)$
12 dfsbcq
13 11 12 bibi12d
14 sbc5
15 19.42v ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\left({z}={x}\wedge \left({w}={y}\wedge {\phi }\right)\right)↔\left({z}={x}\wedge \exists {w}\phantom{\rule{.4em}{0ex}}\left({w}={y}\wedge {\phi }\right)\right)$
16 anass ${⊢}\left(\left({z}={x}\wedge {w}={y}\right)\wedge {\phi }\right)↔\left({z}={x}\wedge \left({w}={y}\wedge {\phi }\right)\right)$
17 16 exbii ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\left(\left({z}={x}\wedge {w}={y}\right)\wedge {\phi }\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\left({z}={x}\wedge \left({w}={y}\wedge {\phi }\right)\right)$
18 sbc5
19 18 anbi2i
20 15 17 19 3bitr4ri
21 20 exbii
22 14 21 bitr2i
23 7 13 22 vtocl2g
24 23 ancoms