\begin{definition}[Definition:Existential Quantifier/Unique/Definition 2]
There exists a unique object $x$ such that $\map P x$, denoted $\exists ! x: \map P x$, {{iff}}:
:$\exists x : \forall y : \paren {\map P y \iff x = y}$
\end{definition}