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	$$⊢\exists f\forall z\in x\left(z\ne \varnothing \to f\left(z\right)\in z\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfac3	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\exists f\forall z\in x\left(z\ne \varnothing \to f\left(z\right)\in z\right)$$
2	1	axaci	$$⊢\exists f\forall z\in x\left(z\ne \varnothing \to f\left(z\right)\in z\right)$$