Pair

🅟 Feb 16, 2026

  🅤 Apr 19, 2026

PAIR#DEF. 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\lrimp\enspace x=a\lor x=b.\]

The existence of $X$ is justified by Axiom of Pairing and its uniqueness is justified by Axiom of Extensionality.


PAIR#PROP-UO. Unorderedness.

For any $a$ and $b$,

\[\{a,b\} = \{b,a\}.\]

PAIR#PROP-CARD.

For any $a\neq b$,

\[\big\lvert\{a,b\}\big\rvert = 2.\]

Proof.$\{(a,0),(b,1)\}$ is a bijection from $\{a,b\}$ to $2$.