User:Dfeuer/Set has Unique Singleton

Theorem

Let $x$ be a set.

Then $x$ has a unique User:Dfeuer/Definition:Singleton.

Proof

By the User:Dfeuer/Axiom Schema of Separation, there is a class $S$ such that

$\forall y: y \in S \iff y = x$

By the User:Dfeuer/Axiom of Extensionality, this class is unique.

$\blacksquare$