# Source for NBG+Equipollence conservative over ZFC?

The "conservative" class theory, NBG, proves no new theorems about sets (with respect to ZFC). The choice function used here is set choice, and it's not too hard to prove (if M is a ctm for ZFC, then D(M) is a ctm for NBG and has the same set universe).

However, if we add the axiom that there is a bijection (in the class universe) between $\mathbf{V}$ and $\mathbf{ON}$, the classes of sets and ordinals, respectively, this is apparently still conservative over ZFC (with a much stronger class choice axiom). However, I can't find a reference for this.

Apparently this fact is credited to Easton and Solovay, published by Easton in 1964, and apparently it uses class forcing, but I can't find any more specific information on this topic, or the paper itself. Does anyone have more specific information on this, or better search skills than I do?

-
I don't have the reference handy, but the forcing consists of all set-sized partial injections from $\mathbf{ON}$ to $\mathbf{V}$, ordered by extension. Since this is $\kappa$-closed for all $\kappa$, no new sets are added in the forcing extension, and the generic is a bijection from $\mathbf{ON}$ to $\mathbf{V}$. –  François G. Dorais Apr 6 '12 at 15:50
This is the forcing I wanted to do, but unfortunately I lacked the background to prove (to my own satisfaction) that it actually works. –  Richard Rast Apr 6 '12 at 16:12

As an aside: In the last chapter of my master thesis, which unfortunately only exists in Czech, I prove a generalization of the result to set theory without foundation ($\mathrm{ZFC}\_-$). It turns out that in the absence of foundation, global choice has nontrivial consequences even for sets. $\mathrm{ZFC}\_-$ (or $\mathrm{NBG}\_-$) + global choice is a conservative extension of $\mathrm{ZF}\_-$ extended by the following schema: $$\forall x\\,\exists y\\,\phi(x,y)\to\forall\alpha\in\mathrm{On}\\,\exists f\colon\alpha\to\mathrm{V}\\,\forall\beta< \alpha\\,\phi(f\restriction\beta,f(\beta))$$ (a sort of class version of $\mathrm{DC}\_\alpha$; an equivalent formulation: any class tree whose height is bounded by an ordinal has a maximal path).