I don't know the proof either. The other weird thing to note is that even though NBG is a conservative extension of ZFC, some proofs in NBG are much shorter than proofs in ZFC. So in some sense it is only weakly conservative. I don't know if that notion can be made at all more precise.

Edit: Followup thought, most interesting conservative extensions are only weakly conservative in some sense. Consider for example finite degree field extensions of Q. If axiomatized these become conservative extensions of Z. (That's essentially why for example we can prove something in the Gaussian integers and know there's a proof in Z).