- $\exists ! x: \map P x$
- $\exists ! x: \map P x \dashv \vdash \exists x: \map P x \land \forall y: \map P y \implies x = y$
In natural language, this means:
- is logically equivalent to:
The symbol $\exists !$ is a variant of the existential quantifier $\exists$: there exists at least one.
The symbol $\exists_1$ is also found for the same concept, being an instance of the exact existential quantifier $\exists_n$.
Some sources, for example 1972: Patrick Suppes: Axiomatic Set Theory, use $\operatorname E !$, which is idiosyncratic, considering the use in the same source of $\exists$ for the general existential quantifier.