Metamath Proof Explorer

Table of Contents - 2.1.2. Classes

1. Class abstractions
   1. cab
   2. df-clab
   3. eleq1ab
   4. cleljustab
   5. abid
   6. vexwt
   7. vexw
   8. vextru
   9. nfsab1
   10. hbab1
   11. hbab1OLD
   12. hbab
   13. hbabg
   14. nfsab
   15. nfsabg
2. Class equality
   1. df-cleq
   2. dfcleq
   3. cvjust
   4. ax9ALT
   5. eleq2w2
   6. eqriv
   7. eqrdv
   8. eqrdav
   9. eqid
   10. eqidd
   11. eqeq1d
   12. eqeq1dALT
   13. eqeq1
   14. eqeq1i
   15. eqcomd
   16. eqcom
   17. eqcoms
   18. eqcomi
   19. neqcomd
   20. eqeq2d
   21. eqeq2
   22. eqeq2i
   23. eqeqan12d
   24. eqeqan12rd
   25. eqeq12d
   26. eqeq12
   27. eqeq12i
   28. eqeq12OLD
   29. eqeq12dOLD
   30. eqeqan12dOLD
   31. eqeqan12dALT
   32. eqtr
   33. eqtr2
   34. eqtr2OLD
   35. eqtr3
   36. eqtr3OLD
   37. eqtri
   38. eqtr2i
   39. eqtr3i
   40. eqtr4i
   41. 3eqtri
   42. 3eqtrri
   43. 3eqtr2i
   44. 3eqtr2ri
   45. 3eqtr3i
   46. 3eqtr3ri
   47. 3eqtr4i
   48. 3eqtr4ri
   49. eqtrd
   50. eqtr2d
   51. eqtr3d
   52. eqtr4d
   53. 3eqtrd
   54. 3eqtrrd
   55. 3eqtr2d
   56. 3eqtr2rd
   57. 3eqtr3d
   58. 3eqtr3rd
   59. 3eqtr4d
   60. 3eqtr4rd
   61. eqtrid
   62. eqtr2id
   63. eqtr3id
   64. eqtr3di
   65. eqtrdi
   66. eqtr2di
   67. eqtr4di
   68. eqtr4id
   69. sylan9eq
   70. sylan9req
   71. sylan9eqr
   72. 3eqtr3g
   73. 3eqtr3a
   74. 3eqtr4g
   75. 3eqtr4a
   76. eq2tri
   77. abbi1
   78. abbidv
   79. abbii
   80. abbid
   81. abbi
   82. cbvabv
   83. cbvabw
   84. cbvabwOLD
   85. cbvab
   86. abeq2w
3. Class membership
   1. df-clel
   2. dfclel
   3. elex2
   4. elissetv
   5. elisset
   6. eleq1w
   7. eleq2w
   8. eleq1d
   9. eleq2d
   10. eleq2dALT
   11. eleq1
   12. eleq2
   13. eleq12
   14. eleq1i
   15. eleq2i
   16. eleq12i
   17. eqneltri
   18. eleq12d
   19. eleq1a
   20. eqeltri
   21. eqeltrri
   22. eleqtri
   23. eleqtrri
   24. eqeltrd
   25. eqeltrrd
   26. eleqtrd
   27. eleqtrrd
   28. eqeltrid
   29. eqeltrrid
   30. eleqtrid
   31. eleqtrrid
   32. eqeltrdi
   33. eqeltrrdi
   34. eleqtrdi
   35. eleqtrrdi
   36. 3eltr3i
   37. 3eltr4i
   38. 3eltr3d
   39. 3eltr4d
   40. 3eltr3g
   41. 3eltr4g
   42. eleq2s
   43. eqneltrd
   44. eqneltrrd
   45. neleqtrd
   46. neleqtrrd
   47. cleqh
   48. nelneq
   49. nelneq2
   50. eqsb1
   51. clelsb1
   52. clelsb2
   53. clelsb2OLD
   54. hbxfreq
   55. hblem
   56. hblemg
4. Elementary properties of class abstractions
   1. abeq2
   2. abeq1
   3. abeq2d
   4. abeq2i
   5. abeq1i
   6. abbi2dv
   7. abbi1dv
   8. abbi2i
   9. abbiOLD
   10. abid1
   11. abid2
   12. clelab
   13. clelabOLD
   14. clabel
   15. sbab