Gödel pointed out that the class existence theorem "is a metatheorem, that is, a theorem about the system [NBG], not in the system …" It is a theorem about NBG because it is proved in the metatheory by induction on NBG formulas.