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. hbab
   12. hbabg
   13. nfsab
   14. 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. eqeqan12dALT
   29. eqtr
   30. eqtr2
   31. eqtr3
   32. eqtri
   33. eqtr2i
   34. eqtr3i
   35. eqtr4i
   36. 3eqtri
   37. 3eqtrri
   38. 3eqtr2i
   39. 3eqtr2ri
   40. 3eqtr3i
   41. 3eqtr3ri
   42. 3eqtr4i
   43. 3eqtr4ri
   44. eqtrd
   45. eqtr2d
   46. eqtr3d
   47. eqtr4d
   48. 3eqtrd
   49. 3eqtrrd
   50. 3eqtr2d
   51. 3eqtr2rd
   52. 3eqtr3d
   53. 3eqtr3rd
   54. 3eqtr4d
   55. 3eqtr4rd
   56. eqtrid
   57. eqtr2id
   58. eqtr3id
   59. eqtr3di
   60. eqtrdi
   61. eqtr2di
   62. eqtr4di
   63. eqtr4id
   64. sylan9eq
   65. sylan9req
   66. sylan9eqr
   67. 3eqtr3g
   68. 3eqtr3a
   69. 3eqtr4g
   70. 3eqtr4a
   71. eq2tri
   72. iseqsetvlem
   73. iseqsetv-cleq
   74. abbi
   75. abbidv
   76. abbii
   77. abbid
   78. abbib
   79. cbvabv
   80. cbvabw
   81. cbvab
   82. eqabbw
3. Class membership
   1. df-clel
   2. dfclel
   3. elex2
   4. issettru
   5. iseqsetv-clel
   6. issetlem
   7. elissetv
   8. elisset
   9. eleq1w
   10. eleq2w
   11. eleq1d
   12. eleq2d
   13. eleq2dALT
   14. eleq1
   15. eleq2
   16. eleq12
   17. eleq1i
   18. eleq2i
   19. eleq12i
   20. eleq12d
   21. eleq1a
   22. eqeltri
   23. eqeltrri
   24. eleqtri
   25. eleqtrri
   26. eqeltrd
   27. eqeltrrd
   28. eleqtrd
   29. eleqtrrd
   30. eqeltrid
   31. eqeltrrid
   32. eleqtrid
   33. eleqtrrid
   34. eqeltrdi
   35. eqeltrrdi
   36. eleqtrdi
   37. eleqtrrdi
   38. 3eltr3i
   39. 3eltr4i
   40. 3eltr3d
   41. 3eltr4d
   42. 3eltr3g
   43. 3eltr4g
   44. eleq2s
   45. eqneltri
   46. eqneltrd
   47. eqneltrrd
   48. neleqtrd
   49. neleqtrrd
   50. nelneq
   51. nelneq2
   52. eqsb1
   53. clelsb1
   54. clelsb2
   55. cleqh
   56. hbxfreq
   57. hblem
   58. hblemg
4. Elementary properties of class abstractions
   1. eqabdv
   2. eqabcdv
   3. eqabi
   4. abid1
   5. abid2
   6. eqab
   7. eqabb
   8. eqabbOLD
   9. eqabcb
   10. eqabrd
   11. eqabri
   12. eqabcri
   13. clelab
   14. clabel
   15. sbab