The power set $\mathcal{P}(x) = \{\, z : z \subseteq x \,\}$

Let $x$ be a set. By For every set $x$ there is exactly one set whose elements are precisely the subsets of $x$ there is exactly one set whose elements are precisely the subsets of $x$ (Subset $x \subseteq y$, proper subset $x \subsetneq y$, and the separation notation $\{\, z \in x : \varphi(z) \,\}$); it is the power set of $x$, written $\mathcal{P}(x)$. Thus $z \in \mathcal{P}(x)$ holds if and only if $z \subseteq x$, and in the class notation of the page,

$\mathcal{P}(x) = \{\, z : z \subseteq x \,\}.$

• Two axioms, not one. The elements of $\mathcal{P}(x)$ are pinned down by The Axiom of Power Set: $\forall x\,\exists y\,\forall z\,(\forall t\,(t \in z \to t \in x) \to z \in y)$ together with 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)))$, because the axiom is assumed here only in its implication form. The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes keeps that cost visible.

• The power set is never empty. $\varnothing \subseteq x$ always holds, so $\varnothing \in \mathcal{P}(x)$ for every $x$; in particular $\mathcal{P}(\varnothing) = \{\varnothing\}$ rather than $\varnothing$. That and the other basic identities are $\mathcal{P}(\varnothing) = \{\varnothing\}$; $\varnothing \in \mathcal{P}(a)$ and $a \in \mathcal{P}(a)$; $a \subseteq b$ if and only if $\mathcal{P}(a) \subseteq \mathcal{P}(b)$; $\bigcup \mathcal{P}(a) = a$; $\bigcap \mathcal{P}(a) = \varnothing$; and $\mathcal{P}(a \cap b) = \mathcal{P}(a) \cap \mathcal{P}(b)$ while only $\mathcal{P}(a) \cup \mathcal{P}(b) \subseteq \mathcal{P}(a \cup b)$ holds.