Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Collection of sets
Set union
Formulation 0
Let $E_j$ be a D11: Set for every $j \in J$.
The union of $E = \{ E_j \}_{j \in J}$ is the D11: Set \begin{equation} \bigcup_{j \in J} E_j : = \{ x \mid \exists \, j \in J : x \in E_j \} \end{equation}
Formulation 1
Let $x$ be a D11: Set.
The union of $x$ is the D11: Set \begin{equation} \cup x : = \{ z \mid \exists \, y \in x : z \in y \} \end{equation}
Dual definition
» Set intersection
Child definitions
» D157: Disjoint union
» D74: Set cover
» D589: Successor set
Results
» R4152:
» R4268: Finite set union with empty set
» R4269: Countable set union with empty set
» R4270: Set union with empty set
» R2224: Set union is associative
» R2080: Union is upper bound for intersection
» R292: Union is smallest upper bound
» R4142: Union is an upper bound to each set in the union
» R4144: Finite union is an upper bound to each set in the union
» R4143: Countable union is an upper bound to each set in the union
» R4145: Binary union is an upper bound to both sets in the union
» R2071: Isotonicity of set union
» R4164: Superset of union iff superset of every set in the union
» R4165: Superset of countable union iff superset of every set in the union
» R4166: Superset of finite union iff superset of every set in the union
» R4167: Superset of binary union iff superset of both sets in the union
» R2082: Binary set union with empty set
» R4213: Countable set union is invariant under bijective shifting of indices
» R2222: Set union is invariant under bijective shifting of indices
» R4214: Finite set union is invariant under bijective shifting of indices
» R2223: Binary set union is commutative
» R977: Ambient set is union of subset and complement of subset
» R4580: Empty set union equals the empty set