# Metamath Proof Explorer

## Theorem cbvaldvaw

Description: Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017) (Revised by Gino Giotto, 10-Jan-2024) Reduce axiom usage, along an idea of Gino Giotto. (Revised by Wolf Lammen, 10-Feb-2024)

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

### Proof

Step Hyp Ref Expression
1 cbvaldvaw.1 ${⊢}\left({\phi }\wedge {x}={y}\right)\to \left({\psi }↔{\chi }\right)$
2 1 ancoms ${⊢}\left({x}={y}\wedge {\phi }\right)\to \left({\psi }↔{\chi }\right)$
3 2 pm5.74da ${⊢}{x}={y}\to \left(\left({\phi }\to {\psi }\right)↔\left({\phi }\to {\chi }\right)\right)$
4 3 cbvalvw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)$
5 19.21v ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
6 19.21v ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)↔\left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
7 4 5 6 3bitr3i ${⊢}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
8 7 pm5.74ri ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$