The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes

Each construction here is licensed by named axioms, and this is the account of which ones.

• The Axiom of Extensionality: $\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)$ is consumed by every construction on the page. An axiom that produces a set specifies its members with a biconditional; Extensionality is what turns "a set with these members" into "the set with these members", and so licenses each definite article and each piece of notation introduced below.

• The Axiom Schema of Separation: for each formula $\varphi$, $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p)))$ is consumed by There is exactly one set with no elements, written $\varnothing$, by the intersection of a nonempty set, by the trimming step that yields The power set $\mathcal{P}(x) = \{\, z : z \subseteq x \,\}$, by the difference of two sets, and by The Cartesian product $A \times B := \{\, z \in \mathcal{P}(\mathcal{P}(A \cup B)) : \exists a \in A\ \exists b \in B\ z = (a,b) \,\}$. It is also what There is no set $U$ with $y \in U$ for every set $y$ is proved from.

• The Axiom of Pairing: $\forall x\,\forall y\,\exists z\,\forall t\,(t \in z \leftrightarrow (t = x \vee t = y))$ is consumed by unordered pairs and singletons, hence by ordered pairs and by everything built from them.

• The Axiom of Union: $\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow \exists s\,(s \in x \wedge z \in s))$ is consumed by The union $\bigcup x$ of a set, and the binary union $a \cup b := \bigcup \{a,b\}$, and through the ambient double power set also by The Cartesian product $A \times B := \{\, z \in \mathcal{P}(\mathcal{P}(A \cup B)) : \exists a \in A\ \exists b \in B\ z = (a,b) \,\}$.

• The Axiom of Power Set: $\forall x\,\exists y\,\forall z\,(\forall t\,(t \in z \to t \in x) \to z \in y)$ is consumed by The power set $\mathcal{P}(x) = \{\, z : z \subseteq x \,\}$ and, through the same ambient set, by The Cartesian product $A \times B := \{\, z \in \mathcal{P}(\mathcal{P}(A \cup B)) : \exists a \in A\ \exists b \in B\ z = (a,b) \,\}$. It is assumed here in its implication form, so each of those two constructions consumes Separation as well.

• The Axiom of Foundation: $\forall S\,(\exists t\,(t \in S) \to \exists s\,(s \in S \wedge \neg\exists u\,(u \in s \wedge u \in S)))$ is consumed by Under Foundation, $x \notin x$ for every set $x$, there are no sets with $x \in y \in x$, and there are no sets with $x \in y \in z \in x$ and, through it, by the injectivity of the successor operation. No other result on this page uses it, and no definition does.

• The Axiom of Infinity: there is a set containing a set with no elements and closed under $y \mapsto y \cup \{y\}$ is consumed by nothing on this page. It is stated here because it belongs to the system, and it is what the construction of the natural numbers rests on.

• The Axiom Schema of Replacement: for each formula $\varphi$, if $\varphi$ defines a class function on $A$ then its image on $A$ is a set is consumed by nothing on this page either. Every set formed here is separated inside a set already in hand, which is exactly what Separation licenses.

• The Axiom of Choice is the one axiom of ZFC that is not stated on this page. This library states it at The Axiom of Choice ↗. No construction and no result on this page uses it.

Two redundancies in the list are worth recording, because they explain why the ledger above is not the shortest possible one. Separation is derivable from Replacement together with a set that has no elements, by a derivation that splits on whether the separating condition holds anywhere in the ambient set; The Axiom Schema of Replacement: for each formula $\varphi$, if $\varphi$ defines a class function on $A$ then its image on $A$ is a set carries it. Pairing is derivable from Replacement applied to a set with at least two elements, such as the double power set of the empty set. Both are nevertheless assumed here, because each is used constantly and deriving it every time would obscure what a construction actually costs.

The empty set runs the other way. It is often taken as an axiom, and here it is derived instead, from Separation together with the logical fact that the domain of discourse is nonempty; There is exactly one set with no elements, written $\varnothing$ carries the derivation.