What does the "$\exists !$" modified quantifier mean in mathematical proof? eg, "$\exists\ !x \ P(x)$" I'm going through a book on mathematical proof and I recently read

In this section we consider proofs in which the goal has the form $\exists\ !x \ P(x)$.

It then proceeds to define this statement as $\exists x(P(x) \land \neg \exists y(P(y) \land y \neq x))$.
What exactly does the "$\exists !$" modified quantifier mean in mathematical proof? Based on the context, I assume it means that $x$ is unique in some way.
 A: Though there is a good answer I want to add some comments.
$\exists!$ is used to denote the unique existence of some mathematical object. $\exists!x: P(x)$ is a shorthand for
$$
\exists x: [P(x) \land \forall y: (P(y) \Rightarrow x = y)]
$$
and we say there is unique $x$ that satisfies $P$.
It can be easily shown that this is equivalent to your statement using the DeMorgan's law.
There are several useful equivalent expressions.

*

*$ \exists x: P(x) \land \forall x \forall y: [(P(x) \land P(y)) \Rightarrow x = y] $
We read $\exists x: P(x)$ as there is at least one $x$ such that $P(x)$, and read the second sentence as any two elements that satisfy $P$ are identical, that is, there is at most one such $x$. This is useful when you already show that $P(x)$ and still want to show that such $x$ is unique afterward.


*$\exists x \forall y: [P(y) \Leftrightarrow y = x]$
This is sometimes used for brevity.
Reference: Wikipedia
A: $\exists ! \ x$ means that there exists a unique $x$ that satisfies whatever you're given about it.
If you want, you can find a (large) list of common math symbols on websites like this one. In your case, the one you were searching for is in the "Basic Logic" section.
