Metamath Proof Explorer


Table of Contents - 2.1.2.2. Class equality

This section introduces class equality in df-cleq.

Note that apart from the local introduction of class variables to state the syntax axioms wceq and wcel, this section is the first to use class variables. Therefore, the file set.mm contains declarations of class variables at the beginning of this section (not visible on the webpages).

  1. df-cleq
  2. dfcleq
  3. cvjust
  4. ax9ALT
  5. eqriv
  6. eqrdv
  7. eqrdav
  8. eqid
  9. eqidd
  10. eqeq1d
  11. eqeq1dALT
  12. eqeq1
  13. eqeq1i
  14. eqcomd
  15. eqcom
  16. eqcoms
  17. eqcomi
  18. neqcomd
  19. eqeq2d
  20. eqeq2
  21. eqeq2i
  22. eqeq12
  23. eqeq12i
  24. eqeq12d
  25. eqeqan12d
  26. eqeqan12dALT
  27. eqeqan12rd
  28. eqtr
  29. eqtr2
  30. eqtr3
  31. eqtri
  32. eqtr2i
  33. eqtr3i
  34. eqtr4i
  35. 3eqtri
  36. 3eqtrri
  37. 3eqtr2i
  38. 3eqtr2ri
  39. 3eqtr3i
  40. 3eqtr3ri
  41. 3eqtr4i
  42. 3eqtr4ri
  43. eqtrd
  44. eqtr2d
  45. eqtr3d
  46. eqtr4d
  47. 3eqtrd
  48. 3eqtrrd
  49. 3eqtr2d
  50. 3eqtr2rd
  51. 3eqtr3d
  52. 3eqtr3rd
  53. 3eqtr4d
  54. 3eqtr4rd
  55. syl5eq
  56. syl5req
  57. syl5eqr
  58. syl5reqr
  59. syl6eq
  60. syl6req
  61. syl6eqr
  62. syl6reqr
  63. sylan9eq
  64. sylan9req
  65. sylan9eqr
  66. 3eqtr3g
  67. 3eqtr3a
  68. 3eqtr4g
  69. 3eqtr4a
  70. eq2tri
  71. abbi1
  72. abbidv
  73. abbii
  74. abbid
  75. abbi
  76. cbvabv
  77. cbvabw
  78. cbvabwOLD
  79. cbvab