DefUniversalClass (3.05, Definition): Universal class

DefUniversalClass (3.05) — Universal class

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	Universal class `#DefUniversalClass` `#label-universal-class`
Classification	Definition
Formula	0(V={x\|⊤}) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/top-const.html}{\top} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PKernelDef_prf`
Scheme of Types	0`(V={[x@Class.Expression]\|⊤})`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefUniversalClass`) → · (3.05) · `#DefUniversalClass`