Theorem eubi

Equivalence theorem for the unique existential quantifier. Theorem *14.271 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) Reduce dependencies on axioms. (Revised by BJ, 7-Oct-2022.)

Conclusion
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow (\exists{!} x \, \varphi \leftrightarrow \exists{!} x \, \psi) \)
Proof
l0
exbi
mobi
l2
anbi12d l0 _
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow (\exists x \, \varphi \wedge \exists^\ast x \, \varphi \leftrightarrow \exists x \, \psi \wedge \exists^\ast x \, \psi) \)
l3
df-eu
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists^\ast x \, \varphi \)
df-eu
\( \vdash \exists{!} x \, \psi \leftrightarrow \exists x \, \psi \wedge \exists^\ast x \, \psi \)
3bitr4g l2 l3 _