Axiom schema of collection
ID: axiom-schema-of-collection
For each formula, if every member of a domain set has a witness, a set contains witnesses for all those members. It permits extra members and does not require unique witnesses. For hereditarily countable sets, use ambient axiom of choice to select one internal witness for each member of the countable domain, and use countable-subset closure to keep the resulting witness set internal.
New to topics? Read the docs here!