# Metamath Proof Explorer

## Theorem cbvaldw

Description: Deduction used to change bound variables, using implicit substitution. Version of cbvald with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 2-Jan-2002) (Revised by Gino Giotto, 10-Jan-2024)

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

### Proof

Step Hyp Ref Expression
1 cbvaldw.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 cbvaldw.2 ${⊢}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
3 cbvaldw.3 ${⊢}{\phi }\to \left({x}={y}\to \left({\psi }↔{\chi }\right)\right)$
4 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
5 nfvd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
6 4 1 2 5 3 cbv2w ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$