Metamath Proof Explorer

Table of Contents - 2.5. ZF Set Theory - add the Axiom of Regularity

1. Introduce the Axiom of Regularity
   1. ax-reg
   2. axreg2
   3. zfregcl
   4. zfreg
   5. elirrv
   6. elirr
   7. elneq
   8. nelaneq
   9. epinid0
   10. sucprcreg
   11. ruv
   12. ruALT
   13. zfregfr
   14. en2lp
   15. elnanel
   16. cnvepnep
   17. epnsym
   18. elnotel
   19. elnel
   20. en3lplem1
   21. en3lplem2
   22. en3lp
   23. preleqg
   24. preleq
   25. preleqALT
   26. opthreg
   27. suc11reg
   28. dford2
2. Axiom of Infinity equivalents
   1. inf0
   2. inf1
   3. inf2
   4. inf3lema
   5. inf3lemb
   6. inf3lemc
   7. inf3lemd
   8. inf3lem1
   9. inf3lem2
   10. inf3lem3
   11. inf3lem4
   12. inf3lem5
   13. inf3lem6
   14. inf3lem7
   15. inf3
   16. infeq5i
   17. infeq5