Theorem
eumo
Existential uniqueness implies uniqueness. (Contributed by NM, 23-Mar-1995.)
Conclusion
\( \vdash \exists{!} x \, \varphi \rightarrow \exists^\ast x \, \varphi \)
Proof
df-eu
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists^\ast x \, \varphi \)
simprbi
_
This is the content in the right pane.