Description: Axiom scheme of strong
collection. It is stated with all possible
disjoint variable conditions, to show that this weak form is sufficient.
The antecedent means that represents a multivalued function on
, or equivalently
a collection of nonempty classes indexed by
, and the axiom
asserts the existence of a set which
"collects" at least one element in the image of each and
which is made only of such elements. That second conjunct is what makes
it "strong", compared to the axiom scheme of collection ax-coll 4120.
(Contributed by BJ, 5-Oct-2019.) |