> [!NOTE] Axiom (Unordered Pair) > For any two objects there is a [[Zermelo Frankel set theory (ZFC)|set]] that has both as elements (and no others). $\forall x \forall y \exists a \forall z (z\in a \leftrightarrow (z=x \lor z = y) )$ > It is a requirement of [[L2 (FOL)|L2]] that the domain of discourse is non-empty, and so the Unordered Pair Axiom implies the existence of a set that contains this object, whatever it is. From this set, we can use the Axiom of Separation to derive the existence of the empty set as the subset of this set whose elements satisfy $x \neq x.$ # Application The [[Ordered pair|ordered pair]] $(x,y)$ is defined as the set $\{ \{ x \}, \{ x,y \} \}.$