Uniqueness is equivalent to existence implying unique existence.
Alternate definition of the at-most-one quantifier, in terms of the
existential quantifier and the unique existential quantifier.
(Contributed by NM, 8-Mar-1995.) This used to be the definition of the
at-most-one quantifier, while [df-mo] was then proved as dfmo2.
(Revised by BJ, 30-Sep-2022.)
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \exists{!} x \, \varphi \)
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \exists^\ast x \, \varphi \)
\( \vdash \exists x \, \varphi \rightarrow \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \exists{!} x \, \varphi \)