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. ineqcom
    12. ineqcomi
    13. ineqri
    14. ineq1
    15. ineq2
    16. ineq12
    17. ineq1i
    18. ineq2i
    19. ineq12i
    20. ineq1d
    21. ineq2d
    22. ineq12d
    23. ineqan12d
    24. sseqin2
    25. nfin
    26. rabbi2dva
    27. inidm
    28. inass
    29. in12
    30. in32
    31. in13
    32. in31
    33. inrot
    34. in4
    35. inindi
    36. inindir
    37. inss1
    38. inss2
    39. ssin
    40. ssini
    41. ssind
    42. ssrin
    43. sslin
    44. ssrind
    45. ss2in
    46. ssinss1
    47. inss
    48. rexin
    49. 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. indifdi
    31. indifdir
    32. indifdirOLD
    33. difdif2
    34. undm
    35. indm
    36. difun1
    37. undif3
    38. difin2
    39. dif32
    40. difabs
    41. sscon34b
    42. rcompleq
    43. dfsymdif3
  6. Class abstractions with difference, union, and intersection of two classes
    1. unabw
    2. unab
    3. inab
    4. difab
    5. abanssl
    6. abanssr
    7. notabw
    8. notab
    9. unrab
    10. inrab
    11. inrab2
    12. difrab
    13. dfrab3
    14. dfrab2
    15. notrab
    16. dfrab3ss
    17. rabun2
  7. Restricted uniqueness with difference, union, and intersection
    1. reuun2
    2. reuss2
    3. reuss
    4. reuun1
    5. reupick
    6. reupick3
    7. reupick2
    8. euelss