NBG conservative extension of ZFC?

Question

Wikipedia (https://en.wikipedia.org/wiki/Conservative_extension) says:

Von Neumann–Bernays–Gödel set theory is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice (ZFC).

In which sense is NBG a conservative extension of ZFC? I think that in NBG one can prove the existence of a proper class (i.e. the class of all sets) whilst in ZFC one can't prove the existence of such an entity. So there are really statements in NBG that are not provable in ZFC. Why should it be conservative extension then?

Answer 1

What is meant by "conservative extension" in this case is:

Take any sentence in the language of ZFC and translate it into NBG by rewriting every quantifier to restrict its variable to range over sets only. Then the rewritten sentence is a theorem of NBG if and only if the original sentence is a theorem of ZFC.

There are sentences in NBG that don't correspond to a ZFC formula under this translation, and the "conservative extension" property doesn't say anything about those sentences at all. That's why it is an extension.

(To prove the property, assuming the metatheory is a set theory, note that any model of ZFC can become a model of NBG by adding to it every definable collection that is not already a set to the model as proper classes. This gives a model of NBG where the translation of a ZFC sentence is true in the extended model exactly if the original sentence was true in the original model. Conversely, given a model of NBG, removing the proper classes from it produces a model of ZFC).

Answer 2

The easiest way to think of this is probably to formulate NBG as a two-sorted theory, with lower-case variables $x, y, z, \dots$ varying over just sets, and upper-case variables $X, Y, Z, \dots$ varying over all classes. Then, for any formula $\varphi$ all of whose variables are set variables, $\varphi$ is provable in NBG iff $\varphi$ is provable in ZFC.