# Metamath Proof Explorer

## Theorem cbvex4vw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvex4v with more disjoint variable conditions, which requires fewer axioms. (Contributed by NM, 26-Jul-1995) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvex4vw.1 ${⊢}\left({x}={v}\wedge {y}={u}\right)\to \left({\phi }↔{\psi }\right)$
cbvex4vw.2 ${⊢}\left({z}={f}\wedge {w}={g}\right)\to \left({\psi }↔{\chi }\right)$
Assertion cbvex4vw ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}{\chi }$

### Proof

Step Hyp Ref Expression
1 cbvex4vw.1 ${⊢}\left({x}={v}\wedge {y}={u}\right)\to \left({\phi }↔{\psi }\right)$
2 cbvex4vw.2 ${⊢}\left({z}={f}\wedge {w}={g}\right)\to \left({\psi }↔{\chi }\right)$
3 1 2exbidv ${⊢}\left({x}={v}\wedge {y}={u}\right)\to \left(\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
4 3 cbvex2vw ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}{\psi }$
5 2 cbvex2vw ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}{\chi }$
6 5 2exbii ${⊢}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}{\chi }$
7 4 6 bitri ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {v}\phantom{\rule{.4em}{0ex}}\exists {u}\phantom{\rule{.4em}{0ex}}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}{\chi }$