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	|- E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z )

Proof

Step	Hyp	Ref	Expression
1		dfac3	|- ( CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
2	1	axaci	|- E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z )