Metamath Proof Explorer

Table of Contents - 20.3.3. General Set Theory

1. Class abstractions (a.k.a. class builders)
   1. dmrab
   2. difrab2
   3. rabexgfGS
   4. rabsnel
   5. rabeqsnd
   6. eqrrabd
   7. foresf1o
   8. rabfodom
2. Image Sets
   1. abrexdomjm
   2. abrexdom2jm
   3. abrexexd
   4. elabreximd
   5. elabreximdv
   6. abrexss
3. Set relations and operations - misc additions
   1. elunsn
   2. nelun
   3. disjdifr
   4. snsssng
   5. rabss3d
   6. inin
   7. inindif
   8. difininv
   9. difeq
   10. eqdif
   11. undif5
   12. indifbi
   13. diffib
   14. difxp1ss
   15. difxp2ss
   16. undifr
   17. indifundif
   18. elpwincl1
   19. elpwdifcl
   20. elpwiuncl
4. Unordered pairs
   1. eqsnd
   2. elpreq
   3. nelpr
   4. inpr0
   5. neldifpr1
   6. neldifpr2
   7. unidifsnel
   8. unidifsnne
5. Conditional operator - misc additions
   1. ifeqeqx
   2. elimifd
   3. elim2if
   4. elim2ifim
   5. ifeq3da
6. Set union
   1. uniinn0
   2. uniin1
   3. uniin2
   4. difuncomp
   5. elpwunicl
7. Indexed union - misc additions
   1. cbviunf
   2. iuneq12daf
   3. iunin1f
   4. ssiun3
   5. ssiun2sf
   6. iuninc
   7. iundifdifd
   8. iundifdif
   9. iunrdx
   10. iunpreima
   11. iunrnmptss
   12. iunxunsn
   13. iunxunpr
8. Indexed intersection - misc additions
   1. iinabrex
9. Disjointness - misc additions
   1. disjnf
   2. cbvdisjf
   3. disjss1f
   4. disjeq1f
   5. disjxun0
   6. disjdifprg
   7. disjdifprg2
   8. disji2f
   9. disjif
   10. disjorf
   11. disjorsf
   12. disjif2
   13. disjabrex
   14. disjabrexf
   15. disjpreima
   16. disjrnmpt
   17. disjin
   18. disjin2
   19. disjxpin
   20. iundisjf
   21. iundisj2f
   22. disjrdx
   23. disjex
   24. disjexc
   25. disjunsn
   26. disjun0
   27. disjiunel
   28. disjuniel