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. axrep4
   7. axrep5
   8. axrep6
   9. zfrepclf
   10. zfrep3cl
   11. zfrep4
2. Derive the Axiom of Separation
   1. axsepgfromrep
   2. axsep
   3. ax-sep
   4. axsepg
   5. zfauscl
   6. bm1.3ii
   7. 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. prcssprc
   14. sselpwd
   15. difexg
   16. difexi
   17. zfausab
   18. rabexg
   19. rabex
   20. rabexd
   21. rabex2
   22. rab2ex
   23. elssabg
   24. intex
   25. intnex
   26. intexab
   27. intexrab
   28. iinexg
   29. intabs
   30. inuni
   31. elpw2g
   32. elpw2
   33. elpwi2
   34. pwnss
   35. pwne
   36. difelpw
   37. rabelpw
5. Theorems requiring empty set existence
   1. class2set
   2. class2seteq
   3. 0elpw
   4. pwne0
   5. 0nep0
   6. 0inp0
   7. unidif0
   8. iin0
   9. notzfaus
   10. notzfausOLD
   11. intv
   12. axpweq