Metamath Proof Explorer

Table of Contents - 3.1. ZFC Set Theory - add Countable Choice and Dependent Choice

1. Introduce the Axiom of Countable Choice
   1. ax-cc
   2. axcc2lem
   3. axcc2
   4. axcc3
   5. axcc4
   6. acncc
   7. axcc4dom
   8. domtriomlem
   9. domtriom
   10. fin41
   11. dominf
2. Introduce the Axiom of Dependent Choice
   1. ax-dc
   2. dcomex
   3. axdc2lem
   4. axdc2
   5. axdc3lem
   6. axdc3lem2
   7. axdc3lem3
   8. axdc3lem4
   9. axdc3
   10. axdc4lem
   11. axdc4
   12. axcclem
   13. axcc