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