The result Steve sketched a proof of (and my query which provoked this) concerned the conservativeness of ZFC over "ZF + Real Choice" for sentences of second-order arithmetic, not (as you state) the conservativeness of "ZF+RC" over ZF for sentences of second-order arithmetic.