Metamath Proof Explorer

Table of Contents - 20.6.15. Metamath formal systems

This is a formalization of Appendix C of the Metamath book, which describes the mathematical representation of a formal system, of which set.mm (this file) is one.

  1. cmcn
  2. cmvar
  3. cmty
  4. cmvt
  5. cmtc
  6. cmax
  7. cmrex
  8. cmex
  9. cmdv
  10. cmvrs
  11. cmrsub
  12. cmsub
  13. cmvh
  14. cmpst
  15. cmsr
  16. cmsta
  17. cmfs
  18. cmcls
  19. cmpps
  20. cmthm
  21. df-mcn
  22. df-mvar
  23. df-mty
  24. df-mtc
  25. df-mmax
  26. df-mvt
  27. df-mrex
  28. df-mex
  29. df-mdv
  30. df-mvrs
  31. df-mrsub
  32. df-msub
  33. df-mvh
  34. df-mpst
  35. df-msr
  36. df-msta
  37. df-mfs
  38. df-mcls
  39. df-mpps
  40. df-mthm
  41. mvtval
  42. mrexval
  43. mexval
  44. mexval2
  45. mdvval
  46. mvrsval
  47. mvrsfpw
  48. mrsubffval
  49. mrsubfval
  50. mrsubval
  51. mrsubcv
  52. mrsubvr
  53. mrsubff
  54. mrsubrn
  55. mrsubff1
  56. mrsubff1o
  57. mrsub0
  58. mrsubf
  59. mrsubccat
  60. mrsubcn
  61. elmrsubrn
  62. mrsubco
  63. mrsubvrs
  64. msubffval
  65. msubfval
  66. msubval
  67. msubrsub
  68. msubty
  69. elmsubrn
  70. msubrn
  71. msubff
  72. msubco
  73. msubf
  74. mvhfval
  75. mvhval
  76. mpstval
  77. elmpst
  78. msrfval
  79. msrval
  80. mpstssv
  81. mpst123
  82. mpstrcl
  83. msrf
  84. msrrcl
  85. mstaval
  86. msrid
  87. msrfo
  88. mstapst
  89. elmsta
  90. ismfs
  91. mfsdisj
  92. mtyf2
  93. mtyf
  94. mvtss
  95. maxsta
  96. mvtinf
  97. msubff1
  98. msubff1o
  99. mvhf
  100. mvhf1
  101. msubvrs
  102. mclsrcl
  103. mclsssvlem
  104. mclsval
  105. mclsssv
  106. ssmclslem
  107. vhmcls
  108. ssmcls
  109. ss2mcls
  110. mclsax
  111. mclsind
  112. mppspstlem
  113. mppsval
  114. elmpps
  115. mppspst
  116. mthmval
  117. elmthm
  118. mthmi
  119. mthmsta
  120. mppsthm
  121. mthmblem
  122. mthmb
  123. mthmpps
  124. mclsppslem
  125. mclspps