A global choice function is a function formula_1 defined on the class of all nonempty sets such that formula_2 for every nonempty set formula_3 The axiom of global choice states that there exists a global choice function.