The axiom of choice is *not* included in the ZF axioms; ZF+choice is usually abbreviated ZFC.

While all of mathematics is supposed to be embedded in ZFC (or just ZF), some mathematicians prefer to work outside it (or to *pretend* to work outside it, depending on whom you ask). Some logicians use other systems (which are essentially equivalent); some category theorists prefer to avoid using standard formulations of set theory, since they need to use many large categories. And Conway has advocated (in __On Numbers and Games__) ditching the entire fixation on axiom systems, and returning to a more relaxed view of the foundations of mathematics wherever possible (he also uses very large objects, such as a category which satisfies the field axioms, except for not being a set).