Definable element of a first-order structure (source code)

= Definable element of a first-order structure

An element $a$ of a structure $M$ is definable without parameters when some <first-order formula> $\varphi(x)$ uniquely identifies it:
$$
M\models\forall x\,(x=a\leftrightarrow\varphi(x)).
$$