# Metamath Proof Explorer

## Theorem cbvalw

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017)

Ref Expression
Hypotheses cbvalw.1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
cbvalw.2 ${⊢}¬{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
cbvalw.3 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
cbvalw.4 ${⊢}¬{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}¬{\phi }$
cbvalw.5 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion cbvalw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 cbvalw.1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 cbvalw.2 ${⊢}¬{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
3 cbvalw.3 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
4 cbvalw.4 ${⊢}¬{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}¬{\phi }$
5 cbvalw.5 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
6 5 biimpd ${⊢}{x}={y}\to \left({\phi }\to {\psi }\right)$
7 1 2 6 cbvaliw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
8 5 biimprd ${⊢}{x}={y}\to \left({\psi }\to {\phi }\right)$
9 8 equcoms ${⊢}{y}={x}\to \left({\psi }\to {\phi }\right)$
10 3 4 9 cbvaliw ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
11 7 10 impbii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$