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) \,\}$

Let $A$ and $B$ be sets. By If $a \in A$ and $b \in B$ then $(a,b) \in \mathcal{P}(\mathcal{P}(A \cup B))$ every ordered pair $(a,b)$ with $a \in A$ and $b \in B$ is an element of $\mathcal{P}(\mathcal{P}(A \cup B))$, so 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)))$ applied inside that set produces 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) \,\}.$

Its elements are exactly the ordered pairs $(a,b)$ (The Kuratowski ordered pair $(a,b) := \{\{a\},\{a,b\}\}$) with $a \in A$ and $b \in B$: no such pair is lost, because each such pair lies in the ambient set being separated. Thus $z \in A \times B$ holds if and only if $z = (a,b)$ for some $a \in A$ and some $b \in B$.

• Why the ambient set is needed. "The set of all ordered pairs with first coordinate in $A$ and second in $B$" is a class abbreviation, and no axiom turns a class abbreviation into a set on its own. The double power set is what supplies a set to separate inside, so the product costs The Axiom of Power Set: $\forall x\,\exists y\,\forall z\,(\forall t\,(t \in z \to t \in x) \to z \in y)$ and The Axiom of Union: $\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow \exists s\,(s \in x \wedge z \in s))$ as well as Separation; The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes keeps the account.

• Products of nonempty sets. Whether a product of two nonempty sets is nonempty is settled here, by exhibiting the pair ($A \times (B \cup C) = (A \times B) \cup (A \times C)$, $A \times (B \cap C) = (A \times B) \cap (A \times C)$, $A \times (B \setminus C) = (A \times B) \setminus (A \times C)$, $(A \cap B) \times (C \cap D) = (A \times C) \cap (B \times D)$; $A \times B = \varnothing$ if and only if $A = \varnothing$ or $B = \varnothing$; and for nonempty $A$ and $B$, $A \times B \subseteq C \times D$ if and only if $A \subseteq C$ and $B \subseteq D$). The corresponding question for a product of an arbitrary indexed family of nonempty sets is not settled by the axioms on this page: it is one formulation of the Axiom of Choice, stated at The Axiom of Choice ↗.