Class existence theorem

Statement

Let $\phi(x_1, \dots, x_n, Y_1, \dots, Y_m)$ be a formula that quantifies only over sets and contains no free variables other than $x_1, \dots, x_n, Y_1, \dots, Y_m$ (not necessarily all of these). Then for all $Y_1, \dots, Y_m$, there exists a unique class $A$ of $n$-tuples such that:

$$\forall x_1 \cdots \,\forall x_n [(x_1, \dots , x_n) \in A \iff \phi(x_1, \dots, x_n, Y_1, \dots, Y_m)].$$

The class $A$ is denoted by $\{(x_1, \dots , x_n): \phi(x_1, \dots, x_n, Y_1, \dots, Y_m)\}.$