Empty Set

🅟 Feb 24, 2026

  🅤 Mar 07, 2026

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, Axiom of Existence or Axiom of Infinity. Its uniqueness is justified by Axiom of Extensionality.


PROP-EMP-CARD.

\[\lvert\varnothing\rvert = 0.\]

Proof.$\varnothing$ is a bijection from $\varnothing$ to $0$.