DefKuratowskiPair (3.52, Definition): Ordered pair(Kuratowsky's)

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

Formula Display:
Proof Trees:

DefKuratowskiPair (3.52) — Ordered pair(Kuratowsky's)

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.52
Title Ordered pair(Kuratowsky's) #DefKuratowskiPair #label-ordered-pair-kuratowsky-s
Classification Definition
Formula
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/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{b} \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}{a} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{b} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/upair-op.html}{\{} \href{../symbols/upair-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{a} \href{../symbols/upair-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/upair-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/comma-delim.html}{,} \href{../symbols/variables.html}{b} \href{../symbols/upair-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST CpKuratowskiPair
Scheme of Types 0(∀([a@Variable]:[Class@Type])∀([b@Variable]:[Class@Type])(([a@Class.Expression],[b@Class.Expression])={{[a@Class.Expression],[a@Class.Expression]},{[a@Class.Expression],[b@Class.Expression]}}))
Verification Definitional (Kernel AST) · Standalone Entry (DefKuratowskiPair) → · (3.52) · #DefKuratowskiPair