# Metamath Proof Explorer

## Theorem cbvald

Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim . Usage of this theorem is discouraged because it depends on ax-13 . See cbvaldw for a version with x , y disjoint, not depending on ax-13 . (Contributed by NM, 2-Jan-2002) (Revised by Mario Carneiro, 6-Oct-2016) (Revised by Wolf Lammen, 13-May-2018) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 cbvald.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 cbvald.2 ${⊢}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
3 cbvald.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 cbv2 ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$