Symbol Reference: ∪ — Binary Class Union Functional Symbol (∪, AST Constructor: CpBinUnion)

∪ \(\cup\) — Binary Class Union Functional Symbol (∪, AST Constructor: CpBinUnion)

Binary class union functional symbol A ∪ B = {x | (x∈A) ∨ (x∈B)} (Entry DefBinaryUnion (3.53)).

Field	Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol	∪ \(\cup\)
Category	Functional Symbol (Binary Class Operator)
SML AST Constructor	`HC (CpBinUnion of ('Class_EXP * 'Class_EXP)) [in datatype Class_p, typetheory.ML:568]`
Constructor Arguments	1. Left class A : Class; 2. Right class B : Class
Metatype / Signature	`Class × Class → Class`
Binder Status	No — Binary Functional Symbol (Binary Union)
Defining Kernel Entries (ML Labels)	Definition DefBinaryUnion (3.53): Binary union (`#DefBinaryUnion` / `#label-binary-union`)
LaTeX Form	`\cup`
How to Understand It	SML AST Constructor: `HC (CpBinUnion of ('Class_EXP * 'Class_EXP))` in `Class_p` (`typetheory.ML:568`). Takes two class arguments `(A : Class, B : Class)`.
Canonical Law / Usage	`∀(A:Class)∀(B:Class)((A ∪ B) = {x \| (x ∈ A) ∨ (x ∈ B)})`
Related Symbols & Kernel Entries	Definition DefBinaryUnion (3.53): Binary union Binary Intersection ∩ (CpBinInter)

Defining Axioms, Rules & Formal Definitions (Rendered Directly from Kernel Entries)

Generated without code duplication by invoking render_entry_row_base "../manual.html" on the corresponding kernel Entry records.

# Formal Entity Specification

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`