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. snsssng
   4. rabss3d
   5. inin
   6. inindif
   7. difininv
   8. difeq
   9. eqdif
   10. undif5
   11. indifbi
   12. diffib
   13. difxp1ss
   14. difxp2ss
   15. undifr
   16. indifundif
   17. elpwincl1
   18. elpwdifcl
   19. 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