Metamath Proof Explorer

Table of Contents - 3.2.1. Introduce the Axiom of Choice

1. ax-ac
2. zfac
3. ac2
4. ac3
5. ax-ac2
6. axac3
7. ackm
8. axac2
9. axac
10. axaci
11. cardeqv
12. numth3
13. numth2
14. numth
15. ac7
16. ac7g
17. ac4
18. ac4c
19. ac5
20. ac5b
21. ac6num
22. ac6
23. ac6c4
24. ac6c5
25. ac9
26. ac6s
27. ac6n
28. ac6s2
29. ac6s3
30. ac6sg
31. ac6sf
32. ac6s4
33. ac6s5
34. ac8
35. ac9s