Theorem cbvmo

Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on [ax-13]. Use the weaker cbvmow, cbvmovw when possible. (Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.) (Proof shortened by Wolf Lammen, 4-Jan-2023.) (New usage is discouraged.)

Hypotheses
cbvmo.1
\( \vdash \Finv y \, \varphi \)
cbvmo.2
\( \vdash \Finv x \, \psi \)
cbvmo.3
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists^\ast y \, \psi \)
Proof
cbvmo.1
l1
sb8mo _
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists^\ast y \, [ y / x ] \, \varphi \)
l2
cbvmo.2
cbvmo.3
sbie l2 _
mobii _
\( \vdash \exists^\ast y \, [ y / x ] \, \varphi \leftrightarrow \exists^\ast y \, \psi \)
bitri l1 _