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.


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.

  1. $ \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.

  2. $\exists x \forall y: [P(y) \Leftrightarrow y = x]$
    This is sometimes used for brevity.

Reference: Wikipedia


$\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.