Infinitely many axioms of ZFC vs. finitely many axioms of NBG It is known that ZFC needs infinitely many axioms, but NBG (Neuman-Bernays-Gödel set theory) is finitely axiomatizable (as first-order theories of course). But both theories agree completely on the set part of their universe (as far as I have read).
How could this be? How can describing even more objects (proper classes in NBG) while keeping the complexity of some part can reduce the effort to describe this structure? Is there some plausible and evident explanation of this observation? Maybe some philosophical insight from someone who knows the proofs of these statements?
Maybe, is it because the proper classes allow NBG to quantify over predicates in some sense? Something for which ZFC usually needs axiom schemas? If so, why isn't NBG absolutely favorable to ZFC as foundation of math? I mean we also prefer set theory to Peano arithmetic because the latter one allows us to quantify over subsets (in some sense) despite it is a first-order theory (I know we prefer ZFC over PA for tons of other reasons too).

Note: 
I know of this and this question, but I ask specifically why the finite axiom system is not a convincing reason for NBG.
However,the question on which to prefer, ZFC or NBG is secondary. Please concentrate on the finitely vs. infinitely many axioms part and how this can be.
 A: This is because the framework described by the NBG axioms is strictly richer than that which the ZFC axioms describe. This is not an isolated phenomenon. Let me show you diffrent, perhaps a bit less abstract examples.

First example.
It is a well-known consequence of compactness that there is no first-order axiom in the language with just equality whose models are exactly the infinite sets. We need infinitely many axioms saying that there are at least $n$ elements, for arbitrarily large $n$.
On the other hand, if we add a linear ordering, we can consider the theory of dense linear orderings (with at least two points), which is finitely axiomatisable and has no finite models.
Every infinite set can be expanded to a dense linear ordering. Thus, the pure sets underlying dense linear orderings are exactly all infinite sets.

Second example.
For a field $F=(F,+,\cdot,0,1)$, the following are equivalent:

*

*$F$ is formally real, i.e. whenever a sum of squares is zero, all of them have to be zero.

*There is a linear ordering $\leq$ on $F$ which is compatible with the field operations (making $(F,+,\cdot,0,1,\leq)$ an ordered field).

Now, the first order of formally real fields is not finitely axiomatisable: for any $n$, there is a field which is not formally real, but such that the sum of at most $n$ squares, not all zero, is necessarily nonzero. The conclusion follows by compactness.
On the other hand, the theory of ordered fields is obviously finitely axiomatisable.
In this case, the pure fields described by the (finitely axiomatisable) theory of ordered fields are exactly the same as the pure fields described by the (not finitely axiomatisable) theory of formally real fields.

In both examples, the extra structure provided by the linear ordering allows us to force infinitely many axioms to hold simultaneously. Similarly, for NBG, the extra structure provided by the addition of proper classes as elements allows us to force infinitely many axioms to hold simultaneously.
In all cases, the cost is that we need to choose this extra structure: there are many ways to choose a dense linear ordering of an infinite sets, there are (typically) many ways to choose a compatible linear ordering for a formally real field, and there are also (typically?) many ways to expand a model of ZFC to a model of NBG - a pure set does not know its dense linear orderings, a formally real field (usually) does not know any particular compatible ordering, and there is no reason for a model of ZFC to know what classes you should endow it with to get a model of NBG.
A: I will discuss this in two parts:


*

*Why is ZFC finitely axiomatizable in NBG.

*Why is class comprehension finitely axiomatizable.
The first part is simply because, by class comprehensions, every first order predicate is some class. The axioms of ZFC is restricted to first order predicates, and therefore definable in NBG.
As for part 2. NBG allows as to quantify over first order predicates. It is a second order language, applied to discuss first order objects. Just as separation and replacement are restricted to first order object, is is class comprehension, and it is therefore definable with a second order formula.
As for why NBG is not favored. In a sense it is. Many statements in Set Theory discuss proper classes. However the basis of Set Theory is sets, and ZFC is more intuitive in this aspect. And as many classes can be described in terms of sets or formulas, many results in NBG are derivable from ZFC plus the intuitive assumption "There is such thing as a class." The two theories are indeed equiconsistent.
