Uniqueness quantification

For definition of the word unique outside of mathematics, see wiktionary:unique.

In mathematical logic, uniqueness quantification, or unique existential quantification, is a type of quantification that asserts that a property is true for exactly one object in a certain domain.

Uniqueness quantification is denoted with the symbol "∃!", which is usually read "there exists one and only one", "there exists exactly one", or "there exists a unique". For example, the statement

$\exists !n\in \mathbb {N} \,(n-2=4)$

is read as "there is exactly one natural number n such that n - 2 = 4".

Uniqueness quantification can be expressed in terms of the existential and universal quantifiers of predicate logic by defining the formula ∃!x P(x) to mean

$\exists x\,(P(x)\And \forall y\,(P(y)\to x=y))$.

An equivalent definition that has the virtue of separating the notions of existence and uniqueness into two clauses, at the expense of brevity, is

$\exists x\,P(x)\And \forall y\,\forall z\,(P(y)\And P(z)\to y=z)$.

A generalization of uniqueness quantification is counting quantification.