Union of Disjoint Singletons is Doubleton/Proof 2

Theorem

Let $\set a$ and $\set b$ be singletons such that $a \ne b$.

Then:

$\set a \cup \set b = \set {a, b}$

Proof

Straightforward from Union of Unordered Tuples.

$\blacksquare$

Sources

• Mizar article ENUMSET1:1