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

Let $\phi (z,\bar{p})$ be a formula of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations) in which the variable $y$ does not occur free. The Separation instance for $\phi$ is the sentence

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

The Axiom Schema of Separation is the collection of all these sentences, one for each such $\phi$. In words: for any parameters $\bar{p}$ and any set $x$, there is a set $y$ whose elements are exactly the elements $z$ of $x$ for which $\phi (z,\bar{p})$ holds.

It is a schema and not a single axiom because $\phi$ ranges over the formulas of the language, of which there are infinitely many, and the language provides no way to quantify over them.

• The side condition is not decoration. If $y$ were allowed to occur free in $\phi$, the instance $\phi (z,\bar{p}):=z\mathrm{\notin }y$ would assert that some $y$ satisfies $z\in y\leftrightarrow (z\in x\wedge z\mathrm{\notin }y)$ for every $z$, which is contradictory as soon as $x$ has a member. Requiring $y$ to be fresh is what keeps the schema consistent.

• One parameter or a list. Some presentations state the schema with a single parameter $p$ rather than a list $\bar{p}$; the two forms prove the same theorems, since a finite list can be coded once ordered pairs are available. The list form is used here because the instances below quantify over several sets at once.

• A separated set is unique. The instance is stated with $\leftrightarrow$, so any two sets it produces have the same elements and are equal by The Axiom of Extensionality: $\mathrm{\forall }x\mathrm{\forall }y(\mathrm{\forall }z(z\in x\leftrightarrow z\in y)\to x=y)$. That is what licenses the notation $\{z\in x:\phi (z,\bar{p})\}$ introduced at Subset $x\subseteq y$, proper subset $x⊊y$, and the separation notation $\{z\in x:\phi (z)\}$.