DEF-EMP. Empty Set.
The empty set $\varnothing$ is the unique set such that
\[\forall x : x\notin\varnothing.\]The existence of $\varnothing$ is justified by Axiom of Empty Set or Axiom of Infinity. The uniqueness is justified by Axiom of Extensionality.