Subset

🅟 Feb 16, 2026

  🅤 Apr 04, 2026

DEF-SUB. 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$ and $X\neq Y$.


PROP-SUB-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 PROP-ZF-SLF, $X\neq\{X\}$, so $X=\varnothing$.


PROP-SUB-REF. Reflexivity.

For any $X$,

\[X\subseteq X.\]

PROP-SUB-TR. Transitivity.

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

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

PROP-SUB-ATS. Antisymmetry.

For any $X$ and $Y$,

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

As a result:

PROP-SUB-PO.

$\subseteq$ is a partial order.