DefIsProperClass (3.03, Definition): “Is a proper class” predicate

DefIsProperClass (3.03) — “Is a proper class” predicate

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	“Is a proper class” predicate `#DefIsProperClass` `#label-is-a-proper-class-predicate`
Classification	Definition
Formula	0(∀(K:Class)((K proper )⟷(¬(K set )))) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{K} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{K} \href{../symbols/proper-pred.html}{\mathsf{proper}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/neg-conn.html}{\neg} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{K} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`TpProper`
Scheme of Types	0`(∀([K@Variable]:[Class@Type])(([K@Class.Expression] proper)⟷(¬([K@Class.Expression] set))))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefIsProperClass`) → · (3.03) · `#DefIsProperClass`