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. dfdif3OLD
   3. difeq1
   4. difeq2
   5. difeq12
   6. difeq1i
   7. difeq2i
   8. difeq12i
   9. difeq1d
   10. difeq2d
   11. difeq12d
   12. difeqri
   13. nfdif
   14. eldifi
   15. eldifn
   16. elndif
   17. neldif
   18. difdif
   19. difss
   20. difssd
   21. difss2
   22. difss2d
   23. ssdifss
   24. ddif
   25. ssconb
   26. sscon
   27. ssdif
   28. ssdifd
   29. sscond
   30. ssdifssd
   31. ssdif2d
   32. raldifb
   33. rexdifi
   34. complss
   35. compleq
2. The union of two classes
   1. elun
   2. elunnel1
   3. elunnel2
   4. uneqri
   5. unidm
   6. uncom
   7. equncom
   8. equncomi
   9. uneq1
   10. uneq2
   11. uneq12
   12. uneq1i
   13. uneq2i
   14. uneq12i
   15. uneq1d
   16. uneq2d
   17. uneq12d
   18. nfun
   19. unass
   20. un12
   21. un23
   22. un4
   23. unundi
   24. unundir
   25. ssun1
   26. ssun2
   27. ssun3
   28. ssun4
   29. elun1
   30. elun2
   31. elunant
   32. unss1
   33. ssequn1
   34. unss2
   35. unss12
   36. ssequn2
   37. unss
   38. unssi
   39. unssd
   40. unssad
   41. unssbd
   42. ssun
   43. rexun
   44. ralunb
   45. ralun
3. The intersection of two classes
   1. elini
   2. elind
   3. elinel1
   4. elinel2
   5. elin2
   6. elin1d
   7. elin2d
   8. elin3
   9. nel1nelin
   10. nel2nelin
   11. incom
   12. ineqcom
   13. ineqcomi
   14. ineqri
   15. ineq1
   16. ineq2
   17. ineq12
   18. ineq1i
   19. ineq2i
   20. ineq12i
   21. ineq1d
   22. ineq2d
   23. ineq12d
   24. ineqan12d
   25. sseqin2
   26. nfin
   27. rabbi2dva
   28. inidm
   29. inass
   30. in12
   31. in32
   32. in13
   33. in31
   34. inrot
   35. in4
   36. inindi
   37. inindir
   38. inss1
   39. inss2
   40. ssin
   41. ssini
   42. ssind
   43. ssrin
   44. sslin
   45. ssrind
   46. ss2in
   47. ssinss1
   48. ssinss1d
   49. inss
   50. ralin
   51. rexin
   52. 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. difdif2
   33. undm
   34. indm
   35. difun1
   36. undif3
   37. difin2
   38. dif32
   39. difabs
   40. sscon34b
   41. rcompleq
   42. 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. rabdif
   16. notrab
   17. dfrab3ss
   18. 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