ThmEmptySetIsSubclass (3.07, Theorem): Example: “The empty class is a subclass of any class” statement

ThmEmptySetIsSubclass (3.07) — Example: “The empty class is a subclass of any class” statement

Morse-Kelley / Von Neumann-Bernays-Gödel class comprehension, sethood, ordinals, Dunaev pairs, cardinals, universes, and reflection.

Num Entity Database Record (Vertical Field Table)

Title	Example: “The empty class is a subclass of any class” statement `#ThmEmptySetIsSubclass` `#label-example-the-empty-class-is-a-subclass-of-any-class-statement`
Classification	Theorem
Formula	0(∀(X:Class)(∅⊆X)) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/sub-pred.html}{\subseteq} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PSubDef_prf`
Scheme of Types	0`(∀([X@Variable]:[Class@Type])(∅⊆[X@Class.Expression]))`
Verification	Verified (Kernel) · Standalone Entry (`ThmEmptySetIsSubclass`) → · (3.07) · `#ThmEmptySetIsSubclass`