Axiom of global choice

Informally it states that one can simultaneously choose an element from every non-empty set.

The axiom of global choice states that there is a global choice function τ, meaning a function such that for every non-empty set z, τ(z) is an element of z.

Alternatively, Gödel showed that given the axiom of constructibility one can write down an explicit (though somewhat complicated) choice function τ in the language of ZFC, so in some sense the axiom of constructibility implies global choice (in fact, [ZFC proves that] in the language extended by the unary function symbol τ, the axiom of constructibility implies that if τ is said explicitly definable function, then this τ is a global choice function.

In the language of von Neumann–Bernays–Gödel set theory (NBG) and Morse–Kelley set theory, the axiom of global choice can be stated directly (Fraenkel, Bar-Hillel & Levy 1973, p.133), and is equivalent to various other statements: In von Neumann–Bernays–Gödel set theory, global choice does not add any consequence about sets (not proper classes) beyond what could have been deduced from the ordinary axiom of choice.

Global choice is a consequence of the axiom of limitation of size.