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. axrep4OLD
   9. axrep5
   10. axrep6
   11. axrep6OLD
   12. replem
   13. zfrep6
   14. axrep6g
   15. zfrepclf
   16. zfrep3cl
   17. zfrep4
2. Derive the Axiom of Separation
   1. axsepgfromrep
   2. axsep
   3. ax-sep
   4. axsepg
   5. zfauscl
   6. sepexlem
   7. sepex
   8. sepexi
   9. bm1.3iiOLD
   10. 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. ssex
   16. ssexi
   17. ssexg
   18. ssexd
   19. abexd
   20. abex
   21. prcssprc
   22. sselpwd
   23. difexg
   24. difexi
   25. difexd
   26. zfausab
   27. elpw2g
   28. elpw2
   29. elpwi2
   30. rabelpw
   31. rabexg
   32. rabexgOLD
   33. rabex
   34. rabexd
   35. rabex2
   36. rab2ex
   37. elssabg
   38. intex
   39. intnex
   40. intexab
   41. intexrab
   42. iinexg
   43. intabs
   44. inuni
   45. axpweq
   46. pwnss
   47. pwne
   48. 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. notzfaus
   11. intv