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 | ||
Assertion | ac6s4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ac6s4.1 | ||
2 | n0 | ||
3 | 2 | ralbii | |
4 | eleq1 | ||
5 | 1 4 | ac6s2 | |
6 | 3 5 | sylbi |