# Metamath Proof Explorer

## Theorem cbvalv1

Description: Rule used to change bound variables, using implicit substitution. Version of cbval with a disjoint variable condition, which does not require ax-13 . See cbvalvw for a version with two disjoint variable conditions, requiring fewer axioms, and cbvalv for another variant. (Contributed by NM, 13-May-1993) (Revised by BJ, 31-May-2019)

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

### Proof

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