Metamath Proof Explorer

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