A quantifier $\exists !$ that binds a variable $x$ in a formula $\phi \left(x\right)$ and is evaluated as true when there exists a single element that satisfies $\phi \left(x\right)$. In first-order classical logic, the uniqueness quantifier can be defined so that $\exists !\phi \left(x\right)$ is captured by the formula:

• • $\exists x\left(\phi \left(x\right)\wedge \forall y\left(\phi \left(y\right)\to x=y\right)\right)$