Joel nicely answers Asaf's question. Here I just want to add some footnotes to his answer, and to also suggest an answer to the question that Joel poses at the end of his posting.
1. Joel' argument shows that $ZFC$ cannot even prove the definable class form of axiom of choice for pairs. Historically, this was first done by with a similar argument by Easton in his 1964-thesis (printed in the Annals of Mathematical Logic).
2. In the pre-forcing era, Mostowski had already shown that $ZFA$ + "the universe can be linearly ordered" does not imply "every set can be well-ordered" (see p.51 of Jech's book on the Axiom of Choice).
3. As shown in the proof of Theorem 5.21 (p.71) of Jech's text, Mostwoski's argument can be transplanted to the forcing context to show that indeed $V$ can be definably linearly ordered in Cohen's so-called basic model of the failure of the axiom of choice.
4 At the end of his posting, Joel asks:
The next question, I suppose, will be whether one can have a definable linear order of the universe, with ZFC, but no global choicefunction.
I suspect the model in Joel's answer already provides a positive answer to this question.
