RulClassComprehension (3.01, Inference Rule): Class comprehension

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

Formula Display:

Proof Trees:

RulClassComprehension (3.01) — Class comprehension

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	Class comprehension `#RulClassComprehension` `#label-class-comprehension`
Classification	Inference Rule
Formula	0((⦃x⦄∈{⦃x⦄\|⟦𝛗⟧})⟷((⦃x⦄ set )∧⟦𝛗⟧)) 0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/binder-brackets.html}{\{\!\lvert } \href{../symbols/variables.html}{x} \href{../symbols/binder-brackets.html}{\rvert\!\}} \href{../symbols/in-pred.html}{\in} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/binder-brackets.html}{\{\!\lvert } \href{../symbols/variables.html}{x} \href{../symbols/binder-brackets.html}{\rvert\!\}} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/binder-brackets.html}{\{\!\lvert } \href{../symbols/variables.html}{x} \href{../symbols/binder-brackets.html}{\rvert\!\}} \href{../symbols/set-pred.html}{\mathsf{set}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/antiquotation.html}{[\![ } \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/antiquotation.html}{ ]\!]} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST	`PComprAx_prf`
Scheme of Types	0`(([⦃[x@Variable.Expression]⦄@Class.Expression]∈{[⦃[x@Variable.Expression]⦄@Class.Expression]\|⟦[𝛗@Fm.Expression]⟧})⟷(([⦃[x@Variable.Expression]⦄@Class.Expression] set)∧⟦[𝛗@Fm.Expression]⟧))`
Judgements	1[(x:Name), (𝛗:Fm)] 1\(\href{../symbols/image-op.html}{[} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/typing-colon.html}{:} \href{../symbols/name-sort.html}{\mathsf{Name}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/comma-delim.html}{,} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/formula-metavariables.html}{\boldsymbol{\varphi}} \href{../symbols/typing-colon.html}{:} \href{../symbols/fm-sort.html}{\mathsf{Fm}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/image-op.html}{]} \)
Side Condition	1⊤ 1\(\href{../symbols/top-const.html}{\top} \)
Verification	Primitive / Derived Rule (Kernel) · Standalone Entry (`RulClassComprehension`) → · (3.01) · `#RulClassComprehension`