DefBinaryUnion (3.53, Definition): Binary union

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

Formula Display:
Proof Trees:

DefBinaryUnion (3.53) — Binary union

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.53
Title Binary union #DefBinaryUnion #label-binary-union
Classification Definition
Formula
0(∀(A:Class)∀(B:Class)((A∪B)={x|(x∈A)∨(x∈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/delimiters-brackets.html}{(} \href{../symbols/variables.html}{A} \href{../symbols/binunion-op.html}{\cup} \href{../symbols/variables.html}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/eq-pred.html}{=} \href{../symbols/class-comprehension.html}{\{} \href{../symbols/variables.html}{x} \href{../symbols/class-comprehension.html}{ \mid } \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{A} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/or-conn.html}{\lor} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{x} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{B} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/class-comprehension.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
SML Kernel AST CpBinUnion
Scheme of Types 0(∀([A@Variable]:[Class@Type])∀([B@Variable]:[Class@Type])(([A@Class.Expression]∪[B@Class.Expression])={[x@Class.Expression]|([x@Class.Expression]∈[A@Class.Expression])∨([x@Class.Expression]∈[B@Class.Expression])}))
Kernel Note Special Def.: (x ∪ y) = ⋃{x,y} (set-restricted); General Def.: (A ∪ B) = {z | (z ∈ A) ∨ (z ∈ B)} (general class definition).
Verification Definitional (Kernel AST) · Standalone Entry (DefBinaryUnion) → · (3.53) · #DefBinaryUnion