Theorem eu4

Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.)

Hypothesis
eu4.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \forall x \, \forall y \, (\varphi \wedge \psi \rightarrow x = y) \)
Proof
l0
df-eu
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists^\ast x \, \varphi \)
eu4.1
mo4 _
anbi2i _
\( \vdash \exists x \, \varphi \wedge \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \forall x \, \forall y \, (\varphi \wedge \psi \rightarrow x = y) \)
bitri l0 _