The axiom system consisting of ZF (Zermelo-Fraenkel set theory) along with the axiom of choice ("C"). ZFC is consistent if ZF is (as is ZF + the negation of C). It is sometimes convenient to state that some proof occurs in ZF (i.e. does *not* require the axiom of choice). There are still some who do not accept C, or have some misgivings about it. And even if you accept C, actually using it in a proof immediately makes the result highly non-constructive. So a proof in ZF is more constructive.