In set theory, a set is called hereditarily countable if it is a countable set of hereditarily countable sets. The inductive definition above is well-founded and can be expressed in the language of first-order set theory. A set is hereditarily countable if and only if it is countable, and every element of its transitive closure is countable. If the axiom of countable choice holds, then a set is hereditarily countable if and only if its transitive closure is countable. The class of all hereditarily countable sets can be proven to be a set from the axioms of Zermelo–Fraenkel set theory (ZF) and is set is designated . In particular, the existence does not require any form of the axiom of choice. Constructive Zermelo-Freankel (CZF) does not prove the class to be a set. This class is a model of Kripke–Platek set theory with the axiom of infinity (KPI), if the axiom of countable choice is assumed in the metatheory. If , then . More generally, a set is hereditarily of cardinality less than κ if it is of cardinality less than κ, and all its elements are hereditarily of cardinality less than κ; the class of all such sets can also be proven to be a set from the axioms of ZF, and is designated . If the axiom of choice holds and the cardinal κ is regular, then a set is hereditarily of cardinality less than κ if and only if its transitive closure is of cardinality less than κ.