Definition 1. The empty set $\empt$ is the unique set such that
\[\forall x : x \notin \empt.\]The existence of $\empt$ is justified by Axiom of Empty Set, Axiom of Existence or Axiom of Infinity. Its uniqueness is justified by Axiom of Extensionality.
A set $A$ is non-empty if $A \neq \empt$, i.e.
\[\exists x : x \in A.\]