Unique existential quantifier

\[\begin{align*}
  \exists! x \>\> P(x), \\
  \exists_{= 1} x \>\> P(x),
\end{align*}
\]

and read

“there exists exactly one \(x\) such that \(P(x)\)”

which is equivalent to

\[\begin{equation*}
  \forall x \exits y : P(x) \iff x = y
\end{equation*}
\]

where \(P\) is the quantified predicate.