First-order NBG set theory is finitely axiomatizable. The proof of this basically shows that the axiom schemas, in the presence of the other axioms, can be reduced to a finite set of cases, and are hence equivalent to a finite set of axioms.
Is this equivalence also valid in second-order NBG? Or does the reduction to a finite number of cases only work for definable predicates (e.g. the first order axiom schema)?