|Description: Axiom of Union. An axiom
of Intuitionistic Zermelo-Fraenkel set theory.
It states that a set 𝑦 exists that includes the union of a
𝑥 i.e. the collection of all members of
the members of 𝑥. The
variant axun2 4172 states that the union itself exists. A
version with the
standard abbreviation for union is uniex2 4173. A version using class
notation is uniex 4174.
This is Axiom 3 of [Crosilla] p.
"Axioms of CZF and IZF", except (a)
unnecessary quantifiers are removed, (b) Crosilla has a biconditional
rather than an implication (but the two are equivalent by bm1.3ii 3878),
and (c) the order of the conjuncts is swapped (which is equivalent by
The union of a class df-uni 3581 should not be confused with the union of
two classes df-un 2922. Their relationship is shown in unipr 3594.
(Contributed by NM, 23-Dec-1993.)