$X$ and $Y$ are equinumerous, written $X\equ Y$, if there exists a bijection from $X$ onto $Y$.
$X\lequ Y$ if there exists an injection from $X$ to $Y$.
$X\lnequ Y$ if $X\lequ Y$ and $X\not\equ Y$.
PROP-EQU-REF. Reflexivity of $\equ$.
For any $X$,
\[X \equ X.\]
PROP-EQU-SYM. Symmetry of $\equ$.
For any $X$ and $Y$,
\[X\equ Y \enspace\rimp\enspace Y\equ X.\]
PROP-EQU-TR. Transitivity of $\equ$.
For any $X$, $Y$ and $Z$,
\[X\equ Y \,\land\, Y\equ Z \enspace\rimp\enspace X\equ Z.\]
As a result:
$\equ$ is an equivalence relation.
PROP-EQU-L-REF. Reflexivity of $\lequ$.
For any $X$,
\[X\lequ X.\]
PROP-EQU-L-TR. Transitivity of $\lequ$.
For any $X$, $Y$ and $Z$,
\[X\lequ Y \,\land\, Y\lequ Z \enspace\rimp\enspace X\lequ Z.\]
PROP-EQU-L-ATS. Antisymmetry of $\lequ$ (Schröder-Bernstein Theorem).
For any $X$ and $Y$,
\[X\lequ Y \,\land\, Y\lequ X \enspace\rimp\enspace X\equ Y.\]
PROP-EQU-L-CON. Connectivity of $\lequ$. $\lrimp\AC$
For any $X$ and $Y$,
\[X\lequ Y \enspace\lor\enspace Y\lequ X.\]
As a result:
$\lequ$ is a partial order. If $\AC$ is assumed, it is further a total order.
If $X\subseteq Y$, then $X\lequ Y$.
Proof.$\id_X:X\to Y$ is an injection.