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