DefSingletonSet (3.48, Definition): Singleton set

DefSingletonSet (3.48) — Singleton set

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	Singleton set `#DefSingletonSet` `#label-singleton-set`
Classification	Definition
Formula	0(∀(a:Class)({a}={x\|x=a})) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{a} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/singleton-op.html}{\}} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/variables.html}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{a} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`CpSingleton`
Scheme of Types	0`(∀([a@Variable]:[Class@Type])({[a@Class.Expression]}={[x@Class.Expression]\|[x@Class.Expression]=[a@Class.Expression]}))`
Verification	Definitional (Kernel AST) · Standalone Entry (`DefSingletonSet`) → · (3.48) · `#DefSingletonSet`