\begin{definition}[Definition:Existential Quantifier/Unique/Definition 1]
There exists a unique object $x$ such that $\map P x$, denoted $\exists ! x: \map P x$, {{iff}}:
:$\exists x : \paren {\map P x \land \forall y : \paren {\map P y \implies x = y} }$
In natural language, this means:
::''There exists exactly one $x$ with the property $P$''
: is logically equivalent to:
::''There exists an $x$ such that $x$ has the property $P$, and for every $y$, $y$ has the property $P$ only if $x$ and $y$ are the same object.''
\end{definition}