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. 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. incom
   10. ineqcom
   11. ineqcomi
   12. ineqri
   13. ineq1
   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. 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