Metamath Proof Explorer


Table of Contents - 2.1.13. The difference, union, and intersection of two classes

  1. The difference of two classes
    1. dfdif3
    2. difeq1
    3. difeq2
    4. difeq12
    5. difeq1i
    6. difeq2i
    7. difeq12i
    8. difeq1d
    9. difeq2d
    10. difeq12d
    11. difeqri
    12. nfdif
    13. eldifi
    14. eldifn
    15. elndif
    16. neldif
    17. difdif
    18. difss
    19. difssd
    20. difss2
    21. difss2d
    22. ssdifss
    23. ddif
    24. ssconb
    25. sscon
    26. ssdif
    27. ssdifd
    28. sscond
    29. ssdifssd
    30. ssdif2d
    31. raldifb
    32. rexdifi
    33. complss
    34. compleq
  2. The union of two classes
    1. elun
    2. elunnel1
    3. uneqri
    4. unidm
    5. uncom
    6. equncom
    7. equncomi
    8. uneq1
    9. uneq2
    10. uneq12
    11. uneq1i
    12. uneq2i
    13. uneq12i
    14. uneq1d
    15. uneq2d
    16. uneq12d
    17. nfun
    18. unass
    19. un12
    20. un23
    21. un4
    22. unundi
    23. unundir
    24. ssun1
    25. ssun2
    26. ssun3
    27. ssun4
    28. elun1
    29. elun2
    30. elunant
    31. unss1
    32. ssequn1
    33. unss2
    34. unss12
    35. ssequn2
    36. unss
    37. unssi
    38. unssd
    39. unssad
    40. unssbd
    41. ssun
    42. rexun
    43. ralunb
    44. ralun
  3. The intersection of two classes
    1. elini
    2. elind
    3. elinel1
    4. elinel2
    5. elin2
    6. elin1d
    7. elin2d
    8. elin3
    9. incom
    10. incomOLD
    11. ineqri
    12. ineq1
    13. ineq1OLD
    14. ineq2
    15. ineq12
    16. ineq1i
    17. ineq2i
    18. ineq12i
    19. ineq1d
    20. ineq2d
    21. ineq12d
    22. ineqan12d
    23. sseqin2
    24. nfin
    25. rabbi2dva
    26. inidm
    27. inass
    28. in12
    29. in32
    30. in13
    31. in31
    32. inrot
    33. in4
    34. inindi
    35. inindir
    36. inss1
    37. inss2
    38. ssin
    39. ssini
    40. ssind
    41. ssrin
    42. sslin
    43. ssrind
    44. ss2in
    45. ssinss1
    46. inss
    47. rexin
    48. dfss7
  4. The symmetric difference of two classes
    1. csymdif
    2. df-symdif
    3. symdifcom
    4. symdifeq1
    5. symdifeq2
    6. nfsymdif
    7. elsymdif
    8. dfsymdif4
    9. elsymdifxor
    10. dfsymdif2
    11. symdifass
    12. difsssymdif
    13. difsymssdifssd
  5. Combinations of difference, union, and intersection of two classes
    1. unabs
    2. inabs
    3. nssinpss
    4. nsspssun
    5. dfss4
    6. dfun2
    7. dfin2
    8. difin
    9. ssdifim
    10. ssdifsym
    11. dfss5
    12. dfun3
    13. dfin3
    14. dfin4
    15. invdif
    16. indif
    17. indif2
    18. indif1
    19. indifcom
    20. indi
    21. undi
    22. indir
    23. undir
    24. unineq
    25. uneqin
    26. difundi
    27. difundir
    28. difindi
    29. difindir
    30. indifdir
    31. difdif2
    32. undm
    33. indm
    34. difun1
    35. undif3
    36. difin2
    37. dif32
    38. difabs
    39. dfsymdif3
  6. Class abstractions with difference, union, and intersection of two classes
    1. unab
    2. inab
    3. difab
    4. notab
    5. unrab
    6. inrab
    7. inrab2
    8. difrab
    9. dfrab3
    10. dfrab2
    11. notrab
    12. dfrab3ss
    13. rabun2
  7. Restricted uniqueness with difference, union, and intersection
    1. reuss2
    2. reuss
    3. reuun1
    4. reuun2
    5. reupick
    6. reupick3
    7. reupick2
    8. euelss