DefSemiSingleton (3.35, Definition): “Semi-singleton” predicate

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

Formula Display:
Proof Trees:

DefSemiSingleton (3.35) — “Semi-singleton” 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)
3.35
Title “Semi-singleton” predicate #DefSemiSingleton #label-semi-singleton-predicate
Classification Definition
Formula
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{s} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \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/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{y} \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/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{s} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{y} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{s} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{y} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST TpSemiSingleton
Scheme of Types 0(∀([s@Variable]:[Class@Type])∀([x@Variable]:[Class@Type])∀([y@Variable]:[Class@Type])((([x@Class.Expression]∈[s@Class.Expression])∧([y@Class.Expression]∈[s@Class.Expression]))→([x@Class.Expression]=[y@Class.Expression])))
Verification Definitional (Kernel AST) · Standalone Entry (DefSemiSingleton) → · (3.35) · #DefSemiSingleton