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. nfdifOLD
   15. eldifi
   16. eldifn
   17. elndif
   18. neldif
   19. difdif
   20. difss
   21. difssd
   22. difss2
   23. difss2d
   24. ssdifss
   25. ddif
   26. ssconb
   27. sscon
   28. ssdif
   29. ssdifd
   30. sscond
   31. ssdifssd
   32. ssdif2d
   33. raldifb
   34. rexdifi
   35. complss
   36. 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. nfunOLD
   20. unass
   21. un12
   22. un23
   23. un4
   24. unundi
   25. unundir
   26. ssun1
   27. ssun2
   28. ssun3
   29. ssun4
   30. elun1
   31. elun2
   32. elunant
   33. unss1
   34. ssequn1
   35. unss2
   36. unss12
   37. ssequn2
   38. unss
   39. unssi
   40. unssd
   41. unssad
   42. unssbd
   43. ssun
   44. rexun
   45. ralunb
   46. 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. nfinOLD
   28. rabbi2dva
   29. inidm
   30. inass
   31. in12
   32. in32
   33. in13
   34. in31
   35. inrot
   36. in4
   37. inindi
   38. inindir
   39. inss1
   40. inss2
   41. ssin
   42. ssini
   43. ssind
   44. ssrin
   45. sslin
   46. ssrind
   47. ss2in
   48. ssinss1
   49. ssinss1d
   50. inss
   51. ralin
   52. rexin
   53. 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