User:Dfeuer/Axiom Schema of Separation

Axiom

Let $\varphi (A_1, A_2, \dots, A_n, x)$ be a first-order formula whose class variables are $A_1, A_2, \dots, A_n$ and whose only set variable is $x$.

Note that $n$ may be $0$. That is, there may not be any class variables in the formula aside from the set variable $x$.

Then:

$\forall A_1: \forall A_2: \dots: \forall A_n: \exists B: \forall x: x \in B \iff \varphi(A_1, A_2, \dots, A_n, x)$

That is, given any subclasses $A_1, A_2, \dots, A_n$ of the universe $\mathbb U$, there is a class $B$ consisting precisely of the elements of $\mathbb U$ that satisfy $\phi(A_1, A_2, \dots, A_n, x)$.

Note that this axiom schema produces a separate axiom for each first-order formula $\phi$.