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.