Theorem cbvexvw

Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.)

Hypothesis
cbvalvw.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists x \, \varphi \leftrightarrow \exists y \, \psi \)
Proof
cbvalvw.1
notbid _
cbvalvw _
l3
notbii _
\( \vdash \neg \forall x \, \neg \varphi \leftrightarrow \neg \forall y \, \neg \psi \)
l4
df-ex
\( \vdash \exists x \, \varphi \leftrightarrow \neg \forall x \, \neg \varphi \)
df-ex
\( \vdash \exists y \, \psi \leftrightarrow \neg \forall y \, \neg \psi \)
3bitr4i l3 l4 _