|Description: Axiom of Union. An axiom
of Intuitionistic Zermelo-Fraenkel set
theory. It states that a set y exists that includes the union of a
given set x
i.e. the collection of all members of the members of
variant axun2 4095 states that the union itself exists. A
version with the standard abbreviation for union is uniex2 4096. A
version using class notation is uniex 4097.
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 3830),
and (c) the order of the conjuncts is swapped (which is equivalent by
The union of a class df-uni 3533 should not be confused with the union of
two classes df-un 2900. Their relationship is shown in unipr 3546.
(Contributed by NM, 23-Dec-1993.)