Metamath Proof Explorer

Theorem cbval2vw

Description: Rule used to change bound variables, using implicit substitution. Version of cbval2vv with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 4-Feb-2005) (Revised by Gino Giotto, 10-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 cbval2vw.1 ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left({\phi }↔{\psi }\right)$
2 1 cbvaldvaw ${⊢}{x}={z}\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {w}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
3 2 cbvalvw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}{\psi }$