Countable-subset closure
ID: countable-subset-closure
A set has countable-subset closure when every countable subset of it is one of its elements, including the empty subset. In ZFC, the hereditarily countable sets form the least such set. First realize them as the separated subset of with countable transitive closure. Countable unions show closure; well-founded induction proves leastness because each of these sets is a countable collection of earlier members.
New to topics? Read the docs here!