MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

2 Fixed a reference and a typo

While not the traditional Axiom of choice, Zorn's Lemma makes an appearance on the road to Mitchel's Theorem;

If X is an abelian category with the sup property(Grothendeick's AB5), then an object E is injective iff it does not have a non-trivial essential extension.

Mitchel's theorem is state stated in Rotman's Hom alg Homological Algebra(page 316) as;

If A is a small abelian category, then there is a covariant full faithful exact functor from A to abelian groups.

I believe(but do not have access to the appropriate materials to give details) that Zorn's lemma appears in homotopy limits also.