Subset

SUB#DEF. Subset.

• $X$ is a subset of $Y$, written

  \[X\subseteq Y,\]

  if

  \[\forall x :\enspace x\in X \enspace\rimp\enspace x\in Y.\]

• $X$ is a proper subset of $Y$, written

  \[X\subset Y,\]

  if

  \[X\subseteq Y \enspace\land\enspace X\neq Y.\]

SUB#PROP-EMP.

$\varnothing$ is the only set that is a subset of any non-empty set.

Proof.

• $\varnothing$ is a subset of any set since no $x\in\varnothing$.

• If $X$ is a subset of any non-empty set, then $X\subseteq\{X\}$. By ZF#PROP-SLF, $X\neq\{X\}$, so $X=\varnothing$.

​

SUB#PROP-REF. Reflexivity.

For any $X$,

\[X \subseteq X.\]

SUB#PROP-TRA. Transitivity.

For any $X$, $Y$ and $Z$,

\[X\subseteq Y \,\land\, Y\subseteq Z \enspace\rimp\enspace X\subseteq Z.\]

SUB#PROP-ATS. Antisymmetry.

For any $X$ and $Y$,

\[X\subseteq Y \,\land\, Y\subseteq X \enspace\rimp\enspace X=Y.\]

Proof.By Axiom of Extensionality.

SUB#PROP-PO.

$\subseteq$ is a partial order.

Proof.By reflexivity, transitivity and antisymmetry of $\subseteq$.