 The axiom scheme of class comprehension with quantification only over sets admits a finite axiomatization (a finite selection of formulas \(\phi\) (most with parameters) suffices) and was historically first presented in this way. It is an immediate consequence of class comprehension that the Russell class \(\{x \mid x \not\in x\}\) cannot be a set (so there is at least one proper class).