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. elpwi2OLD
    35. pwnss
    36. pwne
    37. difelpw
    38. 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