Theorem cbvex2vw

Rule used to change bound variables, using implicit substitution. Version of cbvex2vv with more disjoint variable conditions, which requires fewer axioms . (Contributed by NM, 26-Jul-1995.) Avoid [ax-13]. (Revised by GG, 10-Jan-2024.)

Hypothesis

cbval2vw.1

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

Conclusion

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

Proof

cbval2vw.1

cbvexdvaw _

cbvexvw _