Theorem cbveuvw

Change bound variable. Uses only Tarski's FOL axiom schemes. See cbveu for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 25-Nov-1994.) (Revised by GG, 30-Sep-2024.)

Hypothesis
cbveuvw.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists{!} y \, \psi \)
Proof
cbveuvw.1
l1
cbvexvw _
cbveuvw.1
cbvmovw _
l4
anbi12i l1 _
\( \vdash \exists x \, \varphi \wedge \exists^\ast x \, \varphi \leftrightarrow \exists y \, \psi \wedge \exists^\ast y \, \psi \)
l5
df-eu
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists^\ast x \, \varphi \)
df-eu
\( \vdash \exists{!} y \, \psi \leftrightarrow \exists y \, \psi \wedge \exists^\ast y \, \psi \)
3bitr4i l4 l5 _