Metamath Proof Explorer

Table of Contents - 3.1.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