DefEmptySet (3.04, Definition): Empty set

Standalone kernel entity record from 3. Set/Class-Theoretic Foundations (3.01–3.78) — View in Complete Entity Database (#DefEmptySet) →

Formula Display:
Proof Trees:

DefEmptySet (3.04) — Empty 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)
3.04
Title Empty set #DefEmptySet #label-empty-set
Classification Definition
Formula
0(∅={x|⊥})
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/bot-const.html}{\bot} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST CpEmptySet
Scheme of Types 0(∅={[x@Class.Expression]|⊥})
Verification Definitional (Kernel AST) · Standalone Entry (DefEmptySet) → · (3.04) · #DefEmptySet