Theorem eumoi

Uniqueness inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)

Hypothesis
eumoi.1
\( \vdash \exists{!} x \, \varphi \)
Conclusion
\( \vdash \exists^\ast x \, \varphi \)
Proof
l0
eumoi.1
\( \vdash \exists{!} x \, \varphi \)
eumo
\( \vdash \exists{!} x \, \varphi \rightarrow \exists^\ast x \, \varphi \)
ax-mp l0 _