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

Let $\varphi(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 $\varphi$ is the sentence

$\forall \bar p\,\forall x\,\exists y\,\forall z\,\bigl(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p))\bigr).$

The Axiom Schema of Separation is the collection of all these sentences, one for each such $\varphi$. 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 $\varphi(z,\bar p)$ holds.

It is a schema and not a single axiom because $\varphi$ 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 $\varphi$, the instance $\varphi(z,\bar p) := z \notin y$ would assert that some $y$ satisfies $z \in y \leftrightarrow (z \in x \wedge z \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: $\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)$. That is what licenses the notation $\{\, z \in x : \varphi(z,\bar p) \,\}$ introduced at Subset $x \subseteq y$, proper subset $x \subsetneq y$, and the separation notation $\{\, z \in x : \varphi(z) \,\}$.