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. axrep6g
   13. zfrepclf
   14. zfrep3cl
   15. 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. nalset
   2. vnex
   3. vprc
   4. nvel
   5. inex1
   6. inex2
   7. inex1g
   8. inex2g
   9. ssex
   10. ssexi
   11. ssexg
   12. ssexd
   13. abexd
   14. abex
   15. prcssprc
   16. sselpwd
   17. difexg
   18. difexi
   19. difexd
   20. zfausab
   21. elpw2g
   22. elpw2
   23. elpwi2
   24. rabelpw
   25. rabexg
   26. rabexgOLD
   27. rabex
   28. rabexd
   29. rabex2
   30. rab2ex
   31. elssabg
   32. intex
   33. intnex
   34. intexab
   35. intexrab
   36. iinexg
   37. intabs
   38. inuni
   39. axpweq
   40. pwnss
   41. pwne
   42. difelpw
5. Theorems requiring empty set existence
   1. class2set
   2. 0elpw
   3. pwne0
   4. 0nep0
   5. 0inp0
   6. unidif0
   7. eqsnuniex
   8. iin0
   9. notzfaus
   10. intv