This is more of an extended comment, but given the fact that there seems to be an incorrect statement on Wikipedia, I felt like it might be good to write some of these observations out more fully.
As per Joel David Hamkins' comments, we need to be a bit careful about what we mean by classes and quantifying over classes and such. Since you want to focus on $\mathsf{ZFC}$, the only reasonable notion of class is that of definable classes (i.e., classes of elements selected by some formula possibly with parameters). I'm going to think about for-all-exists statements regarding classes in a relatively constructive way as in if I say 'for all classes $X$, there is a class $Y$ such that...', what I mean is that there's an explicit procedure for producing a formula defining the class $Y$ given a formula for the class $X$ which works in any model of $\mathsf{ZFC}$ (although this procedure may in general involve finding new parameters). In particular, statements of this form can also be taken as an assumption, rather than a conclusion, and this assumption may only hold over certain models of $\mathsf{ZFC}$. As Joel also pointed out, in principle things might get a bit hairy if there's no uniform bound on the complexity of the formula for $Y$ in terms of the formula for $X$, but I don't think that's really an issue here. I think these arguments would actually go through in $\mathsf{GBC}$, but I'm not sure.
I need a notion of equivalence of categories that is sensible without choice. I suspect the 'correct' notion involves anafunctors, but I don't actually know enough category theory to be able to work with those. All I really want to say is that equivalence of categories is an equivalence relation (again, this is a relation we're defining on formulas over some fixed model of $\mathsf{ZFC}$) and if I have a functor $F : C \to D$ that is fully faithful and essentially surjective, then $C$ and $D$ are equivalent.
First, we have the fact that if you have skeletons for too many kinds of categories, you definitely get global choice. (Thanks to Asaf Karagila for pointing out how to finish this argument.) Here's a reasonably general form of the statement:
We'll say that a category $C$ has a spine if there is a definable sequence $(A_\alpha)_{\alpha \in \mathrm{Ord}}$ of pairwise distinct isomorphism classes of $C$. (Note that we don't really need to worry about the $A_\alpha$'s being proper classes by Scott's trick.)
Proposition 1. If there is a category $C$ that has a spine such that any category $D$ equivalent to $C$ has a skeleton, then global choice holds.
Proof. Let $(A_\alpha)_{\alpha \in \mathrm{Ord}}$ be a spine of $C$. For each $\alpha \in \mathrm{Ord}$, let $X_\alpha$ be the set of all well-orderings of $V_\alpha$ (which is non-empty by set choice). Define a new category $D$ whose objects are either
- $\langle B,0\rangle$ for some object $B \in C$ not in the given spine of $C$ or
- $\langle A_\alpha,1,x\rangle$ for $\alpha \in \mathrm{Ord}$ and $x \in X_\alpha$.
The morphisms are defined from the morphisms of $C$ in the obvious way (e.g., the morphisms from $\langle A_\alpha,1,x\rangle$ to $\langle A_\alpha,1,x'\rangle$ for $x\neq x'$ are just the morphisms of $A_\alpha$ into itself. Note that the obvious map from $D$ to $C$ is a fully faithful epimorphism of categories, so $D$ and $C$ are equivalent.
Let $S$ be a skeleton of $D$. Evidently we now have a choice function for the family $(X_\alpha)$ (by asking which elements of the form $\langle A_\alpha,1,x\rangle$ are in $S$). Finally, by Asaf's argument we can piece these together to get a global well-ordering and therefore global choice. $\square$
We get an immediate corollary which is that if any category equivalent to $\mathrm{Set}$ has a skeleton, then global choice holds. In particular, this makes me question the statement on Wikipedia that in $\mathsf{ZFC}$ any accessible category has a skeleton.
I actually cannot come up with an example of a large category that does not have a spine, so Proposition 1 already covers most of the categories one would probably want to think about.
Okay but what about spineless categories? Is there any hope that they might have skeletons (which I guess would necessarily be exoskeletons)? In order for a result like this to be relatively natural, one would hope that it would be preserved under passing to equivalent categories. My intuition, however, is that skeletons are just far too evil for any kind of general (purely categorical) statement to not imply global choice. I don't have a proof of this yet, but I have a partial result, which I'll give here. Perhaps someone else can come in and complete the argument.
First we'll need the following fact.
Fact. ($\mathsf{ZFC}$) There is a linearly ordered proper class $W$ with a definable surjection $f : W \to V$.
Proof. Let $W$ be the class of sets of ordinals that code a structure isomorphic to the $\in$-diagram of the transitive closure of some set (via the Gödel pairing function). The lexicographic ordering on sets of ordinals gives a definable linear order. For any $x \in W$, let $f(x)$ be the set coded by $x$. $\square$
Proposition 2. Suppose that there is a large category $C$ such that any category equivalent to $C$ has a skeleton. Then there is a proper class $P$ with a definable linear order such that any $P$-indexed family of sets has a definable choice function.
Proof. Let $C'$ be the category whose objects are of the form $\langle B, x \rangle$ where $B$ is an object of $C$, $x \in W$, and $f(x) = B$. Define automorphisms in $C'$ in the same way as before. $C'$ clearly has a fully faithful epimorphism onto $C$ and so they are equivalent as categories. Let $S$ be a skeleton of $C'$. The definable linear order on $W$ now gives a definable linear order on the objects of $S$.
Now, let $\mathrm{ob}(S)$ be the class of objects of $S$. Let $(X_B)_{B \in \mathrm{ob}(S)}$ be an $\mathrm{ob}(S)$-indexed family of non-empty sets. We can now play the same game and define a category whose objects are of the form $\langle B,x\rangle$, where $B \in \mathrm{ob}(S)$ and $x \in X_B$. Taking a skeleton of this category gives the required choice function. $\square$
With a little bit of fiddling we can also make sure that the linear order is '$\mathrm{Ord}$-like' (i.e., has that each initial segment is a set), but I don't see what that buys us at the moment.
