Theorem cbvex4v
Rule used to change bound variables, using implicit substitution. Usage
of this theorem is discouraged because it depends on [ax-13]. Use the
weaker cbvex4vw if possible. (Contributed by NM, 26-Jul-1995.)
(New usage is discouraged.)
Hypotheses
cbvex4v.1
\( \vdash x = v \wedge y = u \rightarrow (\varphi \leftrightarrow \psi) \)
cbvex4v.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
cbvex4v.1
2exbidv _
l2
cbvex2vv _
\( \vdash \exists x \, \exists y \, \exists z \, \exists w \, \varphi \leftrightarrow \exists v \, \exists u \, \exists z \, \exists w \, \psi \)
cbvex4v.2
cbvex2vv _
2exbii _
\( \vdash \exists v \, \exists u \, \exists z \, \exists w \, \psi \leftrightarrow \exists v \, \exists u \, \exists f \, \exists g \, \chi \)
bitri l2 _