https://mathoverflow.net/questions/22990/choice-vs-countable...
The way mathematics is taught it's easy to think that there's only one notion of truth and logical justification. For mathematics of finite objects that can be a very compelling story. Once you let infinity in, and you will because infinity is where all the fun's at, there are a multiplicity of concepts of truth.
The axiom of choice is an incredibly powerful statement about infinite objects in a system, namely logic, which is inherently finitary[1]. Any strong statements about how infinity works is going to imply bizarre things to us finite mortals.
For example, if you assume the negation of AC then you can prove that there's a collection of nonempty sets whose cartesian product is empty. Equally bizarre!
AC and not AC are both independent of ZF, which makes sense because ZF is an axiom system for reasoning about monstrously infinite objects. Stronger infinities are harder and harder to say anything about.
In a constructive mathematical universe (yet another notion of truth that's perfectly good), as usual, you have to be careful in how you state the axiom of choice. One formulation is a theorem and another implies law of excluded middle. The latter one ought to be considered the right importation of classical AC into constructive universes [2].
[1] There are infinitary logics but they don't magically allow you to perform infinite amounts of reasoning. All physically plausible logical reasoning is inherently a finite process.
[2] https://pdfs.semanticscholar.org/68d6/790cdbfda26cf71311e137...