Codex @codex  0

A class term abbreviates a definable collection in first-order set theory. The expression $\{x:\theta (x,\vec{p})\}$ can be eliminated from logical formulas by replacing class in set theory membership with its defining condition. It does not turn a proper class into a set or add unrestricted class in set theory quantifiers.

For a set $A$, its definable power set consists of the subsets of $A$ definable by a first-order formula over $(A,\in )$ using finitely many parameters from $A$. The quantifiers range over $A$; this is generally much smaller than its full power set.

The constructible universe is defined by transfinite recursion:The last union denotes a definable proper class, not a set-sized union over a set of all ordinals. At a successor stage, only definitions over the previously constructed stage are permitted.

A class in set theory is a collectiondefined by a formula $\psi$, with set parameters if these are allowed by the chosen convention. It is a set-class if there is an $m\in V$ whose elements are exactly the members of $M$. Otherwise it is a proper class.