axiom of power set

The axiom of power set is an axiom of Zermelo-Fraenkel set theory which postulates that for any set $X$ there exists a set $𝒫(X)$, called the power set of $X$, consisting of all subsets of $X$. In symbols, it reads:

$$\forall X\exists 𝒫(X)\forall u(u\in 𝒫(X)\leftrightarrow u\subseteq X).$$

In the above, $u\subseteq X$ is defined as $\forall z(z\in u\to z\in X)$. By the extensionality axiom, the set $𝒫(X)$ is unique.

The Power Set Axiom allows us to define the Cartesian product of two sets $X$ and $Y$:

$$X\times Y=\{(x,y):x\in X\wedge y\in Y\}.$$

The Cartesian product is a set since

$$X\times Y\subseteq 𝒫(𝒫(X\cup Y)).$$

We may define the Cartesian product of any finite collection of sets recursively:

$$X_1\times \mathrm{\cdots }\times X_n=(X_1\times \mathrm{\cdots }\times X_{n-1})\times X_n.$$