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. difexd
   18. zfausab
   19. rabexg
   20. rabex
   21. rabexd
   22. rabex2
   23. rab2ex
   24. elssabg
   25. intex
   26. intnex
   27. intexab
   28. intexrab
   29. iinexg
   30. intabs
   31. inuni
   32. elpw2g
   33. elpw2
   34. elpwi2
   35. elpwi2OLD
   36. pwnss
   37. pwne
   38. difelpw
   39. rabelpw
5. Theorems requiring empty set existence
   1. class2set
   2. class2seteq
   3. 0elpw
   4. pwne0
   5. 0nep0
   6. 0inp0
   7. unidif0
   8. eqsnuniex
   9. iin0
   10. notzfaus
   11. intv
   12. axpweq