Metamath Proof Explorer

Table of Contents - 21.18. Mathbox for Matthew House

  1. Relations on well-ordered indexed unions
    1. weiunval
    2. weiunlem
    3. weiunfrlem
    4. weiunpo
    5. weiunso
    6. weiunfr
    7. weiunse
    8. weiunwe
    9. numiunnum
  2. Axiom of Transitive Containment
    1. axtco
    2. ax-tco
    3. axtco1
    4. axtco2
    5. axtco1from2
    6. axtco1g
    7. axtco2g
    8. axtcond
    9. axuntco
    10. axnulregtco
    11. elALTtco
    12. tz9.1ctco
    13. tz9.1tco
  3. Transitive closure of a class
    1. tr0elw
    2. tr0el
    3. cttc
    4. df-ttc
    5. ttceq
    6. ttceqi
    7. ttceqd
    8. nfttc
    9. ttcid
    10. ttctr
    11. ttctr2
    12. ttctr3
    13. ttcmin
    14. ttcexrg
    15. ttcss
    16. ttcss2
    17. ttcel
    18. ttcel2
    19. ttctrid
    20. ttcidm
    21. ssttctr
    22. elttctr
    23. dfttc2g
    24. ttc0
    25. ttc00
    26. csbttc
    27. ttcuniun
    28. ttciunun
    29. ttcun
    30. ttcuni
    31. ttciun
    32. ttcpwss
    33. ttcsnssg
    34. ttcsnidg
    35. ttcsnmin
    36. ttcsng
    37. ttcsnexg
    38. ttcsnexbig
    39. ttcsntrsucg
    40. dfttc3gw
    41. ttcwf
    42. ttcwf2
    43. ttcwf3
    44. ttc0elw
    45. dfttc4lem1
    46. dfttc4lem2
    47. dfttc4
    48. elttcirr
    49. ttcexg
    50. ttcexbi
    51. dfttc3g
    52. ttc0el
  4. Stronger axioms of regularity
    1. mh-setind
    2. mh-setindnd
    3. regsfromregtco
    4. regsfromsetind
    5. regsfromunir1
  5. Short axioms written in primitive symbols
    1. mh-inf3f1
    2. mh-inf3sn
    3. mh-prprimbi
    4. mh-unprimbi
    5. mh-regprimbi
    6. mh-infprim1bi
    7. mh-infprim2bi
    8. mh-infprim3bi