Axiom schema of collection
= 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.