Metamath Proof Explorer


Theorem ac6s4

Description: Generalization of the Axiom of Choice to proper classes. B is a collection B ( x ) of nonempty, possible proper classes. (Contributed by NM, 29-Sep-2006)

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

Proof

Step Hyp Ref Expression
1 ac6s4.1 A V
2 n0 B y y B
3 2 ralbii x A B x A y y B
4 eleq1 y = f x y B f x B
5 1 4 ac6s2 x A y y B f f Fn A x A f x B
6 3 5 sylbi x A B f f Fn A x A f x B