Consider NBG without choice. Denote this theory NBG'. It is fairly easy once one knows a bit of model theory to demonstrate that this theory is a conservative extension of ZF.
An outline of the traditional proof goes as follows:
Consider some sentence $\phi$ in the language of set theory, and suppose that NBG' $\vdash \phi$ (of course relativising everything to quantify over sets).
I claim that ZF $\vdash \phi$.
For consider some model $(M, \in_M)$ of ZF. We can construct the "model of classes" $(M', \in_{M'})$ as follows:
First, we define $M'$ to be the collection of all sets of the form $\{x \in M \mid M \models \psi(w_1, \ldots, w_n, x)\}$, where $\psi(w_1, \ldots, w_n, x)$ is some formula in the language of ZF and $w_1, \ldots, w_n$ are some elements of $M$.
We then define $S_1 \in_{M'} S_2$ to mean $\exists x \in S_2 (\{y \in M \mid y \in_M x\} = x)$.
It is easy to verify that $M'$ models all axioms of NBG'. Therefore, $M' \models \phi$ by the soundness theorem. We can verify from this statement that $M \models \phi$.
Since all models of ZF are models of $\phi$, we can conclude by the completeness theorem that ZF $\models \phi$.
Conversely, it can be easily shown that NBG' proves all axioms of ZF. So if ZF $\vdash \phi$, then NGB' $\vdash \phi$. $\square$
Of course, we see immediately from this statement that NBG + local choice is a conservative extension of ZFC. This is because $\phi$ is a theorem of NBG + local choice $\iff$ $choice \to \phi$ is a theorem of NBG' $\iff$ $choice \to \phi$ is a theorem of ZF $\iff$ $\phi$ is a theorem of ZFC.
Note that this proof relied on two facts: the soundness theorem for countable vocabularies, and the completeness theorem for countable vocabularies. Because both of these theorems can be formalised in second-order arithmetic, it is possible to formalise the above proof in second-order arithmetic (which is, of course, considerably weaker than ZF).
The question is: can we take the above proof and formalise it in first-order arithmetic?
It seems unlikely, since we cannot use a recursive notion of truth in first-order Peano arithmetic. I don't know how one could even formulate questions about "models" within Peano arithmetic.
If we cannot take the above proof and formalise it in first-order arithmetic, is there some other proof which is available to us? I attempted to proceed with the proof using Boolean categories as models instead of more traditional set-theoretic models, but I did not get anywhere and ran into pretty much the same issues.
Best Answer
$\mathsf{PA}$, and indeed much less, can prove this. Here is one way to do it (not necessarily the only one):
We can define in $\mathsf{PA}$ the notion of a "syntactic $\mathsf{ZFC}$ model;" this will be a $\Sigma^0_{17}$ (say) theory $T$ in the language of set theory + countably many new constant symbols $c_i$ ($i\in\mathbb{N}$) which is complete, contains $\mathsf{ZFC}$, and has the property that for every formula $\varphi(x)$ we have some $i$ such that $T\vdash\exists x\varphi(x)\rightarrow\varphi(c_i)$. $\mathsf{PA}$ can prove that $\mathsf{ZFC}$ is consistent iff there is a syntactic $\mathsf{ZFC}$ model, with the interesting direction amounting to your favorite basis theorem. Similarly we can define the notion of "syntactic $\mathsf{NBG}$ model," and prove the relevant result. The usual semantic relative consistency proof translates easily to a $\mathsf{PA}$-argument that if there exists a syntactic $\mathsf{ZFC}$ model then there exists a syntactic $\mathsf{NBG}$ model.
This is more-or-less a special case of the arithmetized completeness theorem, if memory serves.
EDIT: Here's another argument, which is less direct but perhaps more intuitive:
As you observe, the usual argument can be appropriately formalized in second-order arithmetic. In fact, the fragment $\mathsf{ACA_0}$ suffices for this (although some care is advisable since some seemingly-obvious statements about model theory go beyond $\mathsf{ACA_0}$, see here). But $\mathsf{ACA_0}$ is easily seen to be a conservative extension of $\mathsf{PA}$, in the strong model-theoretic sense, via basically the same argument as the one showing that $\mathsf{NBG}$ is a conservative extension of $\mathsf{PA}$! So - implicitly applying the completeness theorem - we're done.
The downside of this approach, of course, is that unlike the above argument it doesn't indicate a proof strategy inside $\mathsf{ACA_0}$ (and also doesn't help getting below $\mathsf{ACA}_0$, which the above argument does - at a glance, the above argument should work even down to the level of $\mathsf{I\Sigma_1}$). But it's still neat!