ThmDunaevSecondProjection (3.78, Theorem): Second projection of Dunaev's tagged ordered pair

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

Formula Display:
Proof Trees:

ThmDunaevSecondProjection (3.78) — Second projection of Dunaev's tagged ordered pair

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.78
Title Second projection of Dunaev's tagged ordered pair #ThmDunaevSecondProjection #label-second-projection-of-dunaev-s-tagged-ordered-pair
Classification Theorem
Formula
0(∀(A:Class)∀(B:Class)({b|{{{{b}}},{∅,{∅}}}∈(A,B)}=B))
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/class-comprehension.html}{\{} \href{../symbols/variables.html}{b} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/upair-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{b} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/singleton-op.html}{\}} \href{../symbols/comma-delim.html}{,} \href{../symbols/upair-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/comma-delim.html}{,} \href{../symbols/singleton-op.html}{\{} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/singleton-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/upair-op.html}{\}} \href{../symbols/in-pred.html}{\in} \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/class-comprehension.html}{\}} \href{../symbols/eq-pred.html}{=} \href{../symbols/variables.html}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST CpPr2
Scheme of Types 0(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])({[b@Class.Expression]|{{{{[b@Class.Expression]}}},{∅,{∅}}}∈([A@Class.Expression],[B@Class.Expression])}=[B@Class.Expression]))
Kernel Note Recovers B from (A,B) via tag 2 without requiring A or B to be sets.
Verification Verified (Kernel) · Standalone Entry (ThmDunaevSecondProjection) → · (3.78) · #ThmDunaevSecondProjection