Metamath Proof Explorer


Theorem ac6c5

Description: Equivalent of Axiom of Choice. B is a collection B ( x ) of nonempty sets. Remark after Theorem 10.46 of TakeutiZaring p. 98. (Contributed by Mario Carneiro, 22-Mar-2013)

Ref Expression
Hypotheses ac6c4.1 A V
ac6c4.2 B V
Assertion ac6c5 x A B f x A f x B

Proof

Step Hyp Ref Expression
1 ac6c4.1 A V
2 ac6c4.2 B V
3 1 2 ac6c4 x A B f f Fn A x A f x B
4 exsimpr f f Fn A x A f x B f x A f x B
5 3 4 syl x A B f x A f x B