DEF-PR. Pair.
The pair of $a$ and $b$, written as $\{a,b\}$, is the unique set $X$ such that
\[\forall x :\enspace x\in X \enspace\Leftrightarrow\enspace x=a\lor x=b.\]The existence of $X$ is justified by Axiom of Pairing and the uniqueness is justified by Axiom of Extensionality.
PROP-PR.
For any $a$ and $b$,
\[\{a,b\} = \{b,a\}.\]