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. hbab1
   10. nfsab1
   11. nfsab1OLD
   12. hbab
   13. hbabg
   14. nfsab
   15. nfsabg
2. Class equality
   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. eqtrdi
   60. eqtr2di
   61. eqtr4di
   62. eqtr4id
   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
3. Class membership
   1. df-clel
   2. dfclel
   3. eleq1w
   4. eleq2w
   5. eleq1d
   6. eleq2d
   7. eleq2dALT
   8. eleq1
   9. eleq2
   10. eleq12
   11. eleq1i
   12. eleq2i
   13. eleq12i
   14. eqneltri
   15. eleq12d
   16. eleq1a
   17. eqeltri
   18. eqeltrri
   19. eleqtri
   20. eleqtrri
   21. eqeltrd
   22. eqeltrrd
   23. eleqtrd
   24. eleqtrrd
   25. eqeltrid
   26. eqeltrrid
   27. eleqtrid
   28. eleqtrrid
   29. eqeltrdi
   30. eqeltrrdi
   31. eleqtrdi
   32. eleqtrrdi
   33. 3eltr3i
   34. 3eltr4i
   35. 3eltr3d
   36. 3eltr4d
   37. 3eltr3g
   38. 3eltr4g
   39. eleq2s
   40. eqneltrd
   41. eqneltrrd
   42. neleqtrd
   43. neleqtrrd
   44. cleqh
   45. nelneq
   46. nelneq2
   47. eqsb3
   48. clelsb3
   49. clelsb3vOLD
   50. hbxfreq
   51. hblem
   52. 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. clabel
   14. sbab