[[Class]]
# Subclass

Let $A,B$ be [[Class|classes]].
A **subclass** $A \sube B$ is a class whose elements are all elements of $B$, #m/def/set i.e.
$$
\begin{align*}
A \sube B \stackrel{\text{def}}{\iff} (\forall x)[x \in A \implies x \in B]
\end{align*}
$$
A  **proper subclass** is is a subset that is not equal to its superset, i.e.
$$
A \subsetneq B \stackrel{\text{def}}\iff [A \sube B \land A \neq B]
$$
noting the [[Axiom of Extensionality#Axiom of Extensionality for Classes]].
Note these definitions are identical to that of a [[subset]], but with set replaced by class.

#
---
#state/tidy | #lang/en | #SemBr