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

The Axiom of Power Set is the sentence

$\mathrm{\forall }x\mathrm{\exists }y\mathrm{\forall }z(\mathrm{\forall }t(t\in z\to t\in x)\to z\in y)$

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

• Why the weak form. Some presentations assume the biconditional $\mathrm{\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 cardinal arithmetic. It asserts that a set collecting the subsets of $x$ exists. Questions comparing the size of an infinite set with intermediate sizes require later cardinal and model theory; no such result is a premise here.