Metamath Proof Explorer


Theorem ac6s5

Description: Generalization of the Axiom of Choice to proper classes. B is a collection B ( x ) of nonempty, possible proper classes. Remark after Theorem 10.46 of TakeutiZaring p. 98. (Contributed by NM, 27-Mar-2006)

Ref Expression
Hypothesis ac6s4.1 A V
Assertion ac6s5 x A B f x A f x B

Proof

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