Definition. Union_eq
⋃M = {x | ∃A. A ∈ M ∧ x ∈ A}