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