The Class Comprehension Theorem for Predicative Formulas

This is a theorem scheme of the metatheory: it asserts one theorem for each formula as below.

¶ Let $n\ge1$ and $m\ge0$ be metatheoretic numbers, let $x_{1},\dots,x_{n}$ be distinct set variables and $Y_{1},\dots,Y_{m}$ distinct variables of either kind, different from $x_{1},\dots,x_{n}$ (the parameters), and let $\varphi(x_{1},\dots,x_{n},Y_{1},\dots,Y_{m})$ be a predicative formula whose free variables are among them. Then for all classes $Y_{1},\dots,Y_{m}$, with a set assigned to each parameter that is a set variable as in the reading of formulas, there is a class $Z$ such that, for all sets $x_{1},\dots,x_{n}$, the tuple satisfies

$$\langle x_{1},\dots,x_{n}\rangle\in Z\quad\text{if and only if}\quad \varphi(x_{1},\dots,x_{n},Y_{1},\dots,Y_{m}).$$

¶ When $n=1$, the class $Z$ above is unique: any two classes $Z$ and $Z'$ such that, for every set $x_{1}$, each of $x_{1}\in Z$ and $x_{1}\in Z'$ holds if and only if $\varphi(x_{1},Y_{1},\dots,Y_{m})$, are equal.