Description: Equivalent of Axiom of
Choice. We do not insist that be a
function. However, theorem ac58878, derived from this one, shows that
this form of the axiom does imply that at least one such set whose
existence we assert is in fact a function. Axiom of Choice of
[TakeutiZaring] p. 83.
Takeuti and Zaring call this "weak choice" in contrast to
choice" E.A.(=/=->(`)e.), which asserts
the existence of a universal choice function but requires second-order
quantification on (proper) class variable and thus cannot be
expressed in our first-order formalization. However, it has been shown
that ZF plus strong choice is a conservative extension of ZF plus weak
choice. See Ulrich Felgner, "Comparison of the axioms of local and
universal choice," Fundamenta Mathematica, 71, 43-62 (1971).
Weak choice can be strengthened in a different direction to choose from
a collection of proper classes; see ac6s58892. (Contributed by NM,