Metamath Proof Explorer


Theorem ac4

Description: Equivalent of Axiom of Choice. We do not insist that f be a function. However, Theorem ac5 , derived from this one, shows that this form of the axiom does imply that at least one such set f 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 "strong choice" E. F A. z ( z =/= (/) -> ( Fz ) e. z ) , which asserts the existence of a universal choice function but requires second-order quantification on (proper) class variable F 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 ac6s5 . (Contributed by NM, 21-Jul-1996)

Ref Expression
Assertion ac4 f z x z f z z

Proof

Step Hyp Ref Expression
1 dfac3 CHOICE x f z x z f z z
2 1 axaci f z x z f z z