Metamath Proof Explorer

Table of Contents - 21.3.4. Relations and Functions

1. Relations - misc additions
   1. xpdisjres
   2. opeldifid
   3. difres
   4. imadifxp
   5. relfi
   6. 0res
   7. fcoinver
   8. fcoinvbr
   9. brabgaf
   10. brelg
   11. br8d
   12. fnfvor
   13. ofrco
   14. opabdm
   15. opabrn
   16. opabssi
   17. opabid2ss
   18. ssrelf
   19. eqrelrd2
   20. erbr3b
   21. iunsnima
   22. iunsnima2
2. Functions - misc additions
   1. fconst7v
   2. constcof
   3. ac6sf2
   4. ac6mapd
   5. fnresin
   6. fresunsn
   7. f1o3d
   8. eldmne0
   9. f1rnen
   10. f1oeq3dd
   11. rinvf1o
   12. fresf1o
   13. nfpconfp
   14. fmptco1f1o
   15. cofmpt2
   16. f1mptrn
   17. dfimafnf
   18. funimass4f
   19. suppss2f
   20. ofrn
   21. ofrn2
   22. off2
   23. ofresid
   24. unipreima
   25. opfv
   26. xppreima
   27. 2ndimaxp
   28. dmdju
   29. djussxp2
   30. 2ndresdju
   31. 2ndresdjuf1o
   32. xppreima2
   33. abfmpunirn
   34. rabfmpunirn
   35. abfmpeld
   36. abfmpel
   37. fmptdf2
   38. fmptcof2
   39. fcomptf
   40. acunirnmpt
   41. acunirnmpt2
   42. acunirnmpt2f
   43. aciunf1lem
   44. aciunf1
   45. ofoprabco
   46. ofpreima
   47. ofpreima2
   48. funcnv5mpt
   49. funcnv4mpt
   50. preimane
   51. fnpreimac
   52. fgreu
   53. fcnvgreu
   54. rnmposs
   55. mptssALT
   56. dfcnv2
   57. partfun2
   58. rnressnsn
3. Operations - misc additions
   1. mpomptxf
   2. of0r
4. The mapping operation
   1. elmaprd
5. Support of a function
   1. suppovss
   2. elsuppfnd
   3. fisuppov1
   4. suppun2
   5. fdifsupp
   6. suppiniseg
   7. fsuppinisegfi
   8. fressupp
   9. fdifsuppconst
   10. ressupprn
   11. supppreima
   12. fsupprnfi
   13. mptiffisupp
6. Explicit Functions with one or two points as a domain
   1. cosnopne
   2. cosnop
   3. cnvprop
   4. brprop
   5. mptprop
   6. coprprop
   7. fmptunsnop
7. Isomorphisms - misc. additions
   1. gtiso
   2. isoun
8. Disjointness (additional proof requiring functions)
   1. disjdsct
9. First and second members of an ordered pair - misc additions
   1. df1stres
   2. df2ndres
   3. 1stpreimas
   4. 1stpreima
   5. 2ndpreima
   6. curry2ima
   7. preiman0
   8. intimafv
10. Countable Sets
    1. snct
    2. prct
    3. mpocti
    4. abrexct
    5. mptctf
    6. abrexctf
    7. padct
    8. f1od2
    9. fcobij
    10. fcobijfs
    11. fcobijfs2
    12. suppss3
    13. fsuppcurry1
    14. fsuppcurry2
    15. offinsupp1
    16. ffs2
    17. ffsrn
    18. cocnvf1o
    19. resf1o
    20. maprnin
    21. fpwrelmapffslem
    22. fpwrelmap
    23. fpwrelmapffs