Theorem cbvmovw

Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvmo and cbvmow for versions with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Mar-1995.) (Revised by GG, 30-Sep-2024.)

Hypothesis
cbvmovw.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists^\ast y \, \psi \)
Proof
l0
cbvmovw.1
equequ1
imbi12d l0 _
cbvalvw _
l4
exbii _
\( \vdash \exists z \, \forall x \, (\varphi \rightarrow x = z) \leftrightarrow \exists z \, \forall y \, (\psi \rightarrow y = z) \)
l5
dfmo
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
dfmo
\( \vdash \exists^\ast y \, \psi \leftrightarrow \exists z \, \forall y \, (\psi \rightarrow y = z) \)
3bitr4i l4 l5 _