Theorem cbval2vw

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.) Avoid [ax-13]. (Revised by GG, 10-Jan-2024.)

Hypothesis

cbval2vw.1

\( \vdash x = z \wedge y = w \rightarrow (\varphi \leftrightarrow \psi) \)

Conclusion

\( \vdash \forall x \, \forall y \, \varphi \leftrightarrow \forall z \, \forall w \, \psi \)

Proof

cbval2vw.1

cbvaldvaw _

cbvalvw _