The Axiom of Power Set: $\forall x\,\exists y\,\forall z\,(\forall t\,(t \in z \to t \in x) \to z \in y)$

The Axiom of Power Set is the sentence

$\forall x\,\exists y\,\forall z\,\bigl(\forall t\,(t \in z \to t \in x) \to z \in y\bigr)$

of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations): for every set $x$ there is a set $y$ that contains every $z$ all of whose elements belong to $x$.

The axiom is assumed here in this implication form. It says that some set collects all such $z$; it does not say that $y$ contains nothing else, and trimming $y$ down to exactly those $z$ is a separate step, carried out at For every set $x$ there is exactly one set whose elements are precisely the subsets of $x$ using 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)))$.

• Why the weak form. Some presentations assume the biconditional $\forall t\,(t \in z \to t \in x) \leftrightarrow z \in y$ outright. The implication form assumed here is the weaker assumption, and it keeps the Separation step visible: the ledger at The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes then records honestly that the power set costs Power Set and Separation.

• The axiom says nothing about size. It asserts that a set collecting the subsets of $x$ exists, and nothing about how many members that set has. How large the power set of an infinite set is, is exactly the question the continuum hypothesis asks, and that question is settled by neither ZF nor ZFC (The continuum hypothesis and its generalisation are independent of ZFC ‡).