DEF-U. Union.
The union of $X$, written as
\[\bigcup X,\]is the unique set $Y$ such that
\[\forall y :\enspace y\in Y \enspace\Leftrightarrow\enspace \exists x:x\in X\land y\in x.\]The existence of $Y$ is justified by Axiom of Union and the uniqueness is justified by Axiom of Extensionality.
For any $A$ and $B$, we define
\[A\cup B = \bigcup\{A,B\}.\]For any $A$, $B$ and $C$, we define
\[A\cup B\cup C = (A\cup B)\cup C,\]and so on.
PROP-U-EMP.
\[\bigcup\varnothing = \varnothing.\]
PROP-U-EMP2.
For any $X$,
\[X\cup\varnothing = X.\]
PROP-U-SLF.
For any $X$,
\[X\cup X = X.\]
PROP-U-COM. Commutativity.
For any $A$ and $B$,
\[A\cup B = B\cup A.\]
PROP-U-ASS. Associativity.
For any $A$, $B$ and $C$,
\[(A\cup B)\cup C = A\cup (B\cup C).\]