Class existence theorem schema

Let be a predicative formula. Then #m/thm/set/nbg

for any classes .

All of the Axioms of Class Existence are derivable from this theorem.

#state/develop | #lang/en | #SemBr