# Metamath Proof Explorer

## Theorem cbvexvw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017)

Ref Expression
Hypothesis cbvalvw.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion cbvexvw ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 cbvalvw.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
2 1 notbid ${⊢}{x}={y}\to \left(¬{\phi }↔¬{\psi }\right)$
3 2 cbvalvw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}¬{\psi }$
4 3 notbii ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\forall {y}\phantom{\rule{.4em}{0ex}}¬{\psi }$
5 df-ex ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }$
6 df-ex ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\forall {y}\phantom{\rule{.4em}{0ex}}¬{\psi }$
7 4 5 6 3bitr4i ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }$