Metamath Proof Explorer

Table of Contents - 2.2. ZF Set Theory - add the Axiom of Replacement

1. Introduce the Axiom of Replacement
   1. ax-rep
   2. axrep1
   3. axreplem
   4. axrep2
   5. axrep3
   6. axrep4v
   7. axrep4
   8. axrep5
   9. axrep6
   10. replem
   11. zfrep6
   12. axrep6g
   13. zfrepclf
   14. zfrep3cl
   15. zfrep4
2. Derive the Axiom of Separation
   1. axsepgfromrep
   2. axsep
   3. ax-sep
   4. axsepg
   5. sepg
   6. sepgi
   7. zfausclOLD
   8. sepexlem
   9. sepex
   10. sepexi
   11. ax6vsep
3. Derive the Null Set Axiom
   1. axnulALT
   2. axnul
   3. ax-nul
   4. 0ex
   5. al0ssb
   6. sseliALT
   7. csbexg
   8. csbex
   9. unisn2
4. Theorems requiring subset and intersection existence
   1. exnelv
   2. nalset
   3. nalsetOLD
   4. vneqv
   5. vnex
   6. vnexOLD
   7. nvel
   8. vprc
   9. vprcOLD
   10. nvelOLD
   11. inex1
   12. inex2
   13. inex1g
   14. inex2g
   15. ssexg
   16. ssex
   17. ssexOLD
   18. ssexi
   19. ssexgOLD
   20. ssexd
   21. abexd
   22. abex
   23. prcssprc
   24. sselpwd
   25. difexg
   26. difexi
   27. difexd
   28. sepab
   29. elpw2g
   30. elpw2
   31. elpwi2
   32. rabelpw
   33. rabexg
   34. rabex
   35. rabexd
   36. rabex2
   37. rab2ex
   38. elssabg
   39. intex
   40. intnex
   41. intexab
   42. intexrab
   43. iinexg
   44. intabs
   45. inuni
   46. axpweq
   47. pwnss
   48. pwne
   49. difelpw
5. Theorems requiring empty set existence
   1. class2set
   2. 0elpw
   3. pwne0
   4. 0nep0
   5. 0inp0
   6. unidif0
   7. unidif0OLD
   8. eqsnuniex
   9. iin0
   10. notsep
   11. intv