Theorem cbvex4vw
Rule used to change bound variables, using implicit substitution.
Version of cbvex4v with more disjoint variable conditions, which
requires fewer axioms. (Contributed by NM, 26-Jul-1995.) Avoid
[ax-13]. (Revised by GG, 10-Jan-2024.)
Hypotheses
cbvex4vw.1
\( \vdash x = v \wedge y = u \rightarrow (\varphi \leftrightarrow \psi) \)
cbvex4vw.2
\( \vdash z = f \wedge w = g \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \exists x \, \exists y \, \exists z \, \exists w \, \varphi \leftrightarrow \exists v \, \exists u \, \exists f \, \exists g \, \chi \)
Proof
cbvex4vw.1
2exbidv _
l2
cbvex2vw _
\( \vdash \exists x \, \exists y \, \exists z \, \exists w \, \varphi \leftrightarrow \exists v \, \exists u \, \exists z \, \exists w \, \psi \)
cbvex4vw.2
cbvex2vw _
2exbii _
\( \vdash \exists v \, \exists u \, \exists z \, \exists w \, \psi \leftrightarrow \exists v \, \exists u \, \exists f \, \exists g \, \chi \)
bitri l2 _