The other axioms of ZFC are not modified. This theory is not finitely axiomatized. ZFC's replacement schema has been replaced by a single axiom, but the axiom schema of class comprehension has been introduced. To produce a theory with finitely many axioms, the axiom schema of class comprehension is first replaced with finitely many class existence axioms. Then these axioms are used to prove the class existence theorem which implies every instance of the axiom schema. The proof of this theorem requires only seven class existence axioms, which are used to convert the construction of a formula into the construction of a class satisfying the formula. NBG has two types of objects: classes and sets. Intuitively, every set is also a class. There are two ways to axiomatize this. Bernays used many-sorted logic with two sorts: classes and sets. Gödel avoided sorts by introducing primitive predicates: formula_21 for "formula_19 is a class" and formula_23 for "formula_19 is a set" (in German, "set" is "Menge"). He also introduced axioms stating that every set is a class and that if class formula_19 is a member of a class, then formula_19 is a set. Using predicates is the standard way to eliminate sorts. Elliott Mendelson modified Gödel's approach by having everything be a class and defining the set predicate formula_27 as formula_28 This modification eliminates Gödel's class predicate and his two axioms. Bernays' two-sorted approach may appear more natural at first, but it creates a more complex theory. In Bernays' theory, every set has two representations: one as a set and the other as a class. Also, there are two membership relations: the first, denoted by "∈", is between two sets; the second, denoted by "η", is between a set and a class. This redundancy is required by many-sorted logic because variables of different sorts range over disjoint subdomains of the domain of discourse. The differences between these two approaches does not affect what can be proved, but it does affect how statements are written. In Gödel's approach, formula_29 where formula_19 and formula_31 are classes is a valid statement. In Bernays' approach this statement has no meaning. However, if formula_19 is a set, there is an equivalent statement: Define "set formula_33 represents class formula_19" if they have the same sets as members—that is, formula_35 The statement formula_36 where set formula_33 represents class formula_19 is equivalent to Gödel's formula_39  The approach adopted in this article is that of Gödel with Mendelson's modification.