Existence et unicité de l'ensemble vide

La formule $\exists A\, (A = A)$ est un théorème logique (Démonstrations formelles). L'axiome (2) donne $\vdash \forall A\, \neg(A = A) \to \neg(A = A)$, l'axiome (5) donne $\vdash A = A$, et l'instance de tautologie $(P \to \neg Q) \to (Q \to \neg P)$, avec $P = \forall A\, \neg(A = A)$ et $Q = (A = A)$, fournit par deux modus ponens $\vdash \neg\forall A\, \neg(A = A)$, c'est-à-dire $\vdash \exists A\, (A = A)$. Elle reflète la convention du domaine non vide.

Soit donc un ensemble $A$. Par séparation avec la formule $x \neq x$, l'ensemble $\{x \in A : x \neq x\}$ existe, et il n'a aucun élément.

Si $V$ et $V'$ n'ont aucun élément, la condition $x \in V \Leftrightarrow x \in V'$ est vraie pour tout $x$, les deux membres étant faux ; par extensionnalité, $V = V'$.