Metamath Proof Explorer

Table of Contents - 2.6.12. Axiom of Choice equivalents

  1. wac
  2. df-ac
  3. aceq1
  4. aceq0
  5. aceq2
  6. aceq3lem
  7. dfac3
  8. dfac4
  9. dfac5lem1
  10. dfac5lem2
  11. dfac5lem3
  12. dfac5lem4
  13. dfac5lem5
  14. dfac5lem4OLD
  15. dfac5
  16. dfac2a
  17. dfac2b
  18. dfac2
  19. dfac7
  20. dfac0
  21. dfac1
  22. dfac8
  23. dfac9
  24. dfac10
  25. dfac10c
  26. dfac10b
  27. acacni
  28. dfacacn
  29. dfac13
  30. dfac12lem1
  31. dfac12lem2
  32. dfac12lem3
  33. dfac12r
  34. dfac12k
  35. dfac12a
  36. dfac12
  37. kmlem1
  38. kmlem2
  39. kmlem3
  40. kmlem4
  41. kmlem5
  42. kmlem6
  43. kmlem7
  44. kmlem8
  45. kmlem9
  46. kmlem10
  47. kmlem11
  48. kmlem12
  49. kmlem13
  50. kmlem14
  51. kmlem15
  52. kmlem16
  53. dfackm