User:Dfeuer/Empty Class Exists and is Unique

Theorem

There is a unique class $\varnothing$ such that:

$\forall x: x \notin \varnothing$

Proof

Let $\varphi(x) \iff x \ne x$.

Note: the essential idea here is that $\varphi(x)$ is false for every $x$. Any contradiction will do.

Then by User:Dfeuer/Axiom Schema of Separation, there is a class $\varnothing$ such that for each $x \in \mathbb U$:

$x \in \varnothing \iff x \ne x$

If $x$ is any set, $x = x$, so $x \notin \varnothing$.

$\varnothing$ is unique by the User:Dfeuer/Axiom of Extensionality.

$\blacksquare$