Class Abstraction: the Class of All Sets Satisfying a Predicative Formula

Let $m\ge0$ be a metatheoretic number, let $\varphi(x,Y_{1},\dots,Y_{m})$ be a predicative formula with $x$ a set variable and parameters $Y_{1},\dots,Y_{m}$ variables of either kind different from $x$, and let $Y_{1},\dots,Y_{m}$ be classes, those standing for set variables being sets.

¶ The class

$$\{x:\varphi(x,Y_{1},\dots,Y_{m})\}$$

is the unique class $Z$ such that, for every set $x$, $x\in Z$ if and only if $\varphi(x,Y_{1},\dots,Y_{m})$; it exists by The Class Comprehension Theorem for Predicative Formulas §comprehension with $n=1$ and is unique by The Class Comprehension Theorem for Predicative Formulas §unique. It is a class term with membership formula $\varphi(w,Y_{1},\dots,Y_{m})$; in particular, for a set $u$, the expression $u\in\{x:\varphi(x,Y_{1},\dots,Y_{m})\}$ stands for $\varphi(u,Y_{1},\dots,Y_{m})$.

¶ For a class $A$, taken as an additional parameter different from $x$, $\{x\in A:\varphi(x,Y_{1},\dots,Y_{m})\}$ denotes $\{x:x\in A\wedge\varphi(x,Y_{1},\dots,Y_{m})\}$, the formula $x\in A\wedge\varphi$ being predicative.