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. 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
  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