Subclass

Let $𝐴, 𝐵$ be classes. A subclass $𝐴 \subseteq 𝐵$ is a class whose elements are all elements of $𝐵$ , #m/def/set i.e.

𝐴 \subseteq 𝐵 d e f ⟺ (\forall 𝑥) [𝑥 \in 𝐴 ⟹ 𝑥 \in 𝐵]

A proper subclass is is a subset that is not equal to its superset, i.e.

𝐴 ⊊ 𝐵 d e f ⟺ [𝐴 \subseteq 𝐵 \land 𝐴 \neq 𝐵]

noting the 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