The Cartesian product $A\times B:=\{z\in \mathcal{P}(\mathcal{P}(A\cup B)):\mathrm{\exists }a\in A\mathrm{\exists }b\in Bz=(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 $\phi$, $\mathrm{\forall }\bar{p}\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(z\in y\leftrightarrow (z\in x\wedge \phi (z,\bar{p})))$ applied inside that set produces the Cartesian product

$A\times B:=\{z\in \mathcal{P}(\mathcal{P}(A\cup B)):\mathrm{\exists }a\in A\mathrm{\exists }b\in Bz=(a,b)\}\mathrm{.}$

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$.

If $a\in A$ and $b\in B$ then $(a,b)\in \mathcal{P}(\mathcal{P}(A\cup B))$

The Axiom Schema of Separation: for each formula $\phi$, $\mathrm{\forall }\bar{p}\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(z\in y\leftrightarrow (z\in x\wedge \phi (z,\bar{p})))$

The Kuratowski ordered pair $(a,b):=\{\{a\},\{a,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: $\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(\mathrm{\forall }t(t\in z\to t\in x)\to z\in y)$ and The Axiom of Union: $\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(z\in y\leftrightarrow \mathrm{\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=\mathrm{\varnothing }$ if and only if $A=\mathrm{\varnothing }$ or $B=\mathrm{\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 ↗.