User:Dfeuer/Definition:Unordered Pair

Definition

Let $a$ and $b$ be sets.

Then the unordered pair $\{ a, b \}$ is the class of all sets $x$ such that $x = a$ or $x = b$.

Remark

Such a class exists by the User:Dfeuer/Axiom Schema of Separation.

That class is unique by the User:Dfeuer/Axiom of Extensionality.

Also see

• User:Dfeuer/Axiom of Pairing