Metamath Proof Explorer

Table of Contents - 20.10.35. Quantifier-free definitions

  1. ctxp
  2. cpprod
  3. csset
  4. ctrans
  5. cbigcup
  6. cfix
  7. climits
  8. cfuns
  9. csingle
  10. csingles
  11. cimage
  12. ccart
  13. cimg
  14. cdomain
  15. crange
  16. capply
  17. ccup
  18. ccap
  19. csuccf
  20. cfunpart
  21. cfullfn
  22. crestrict
  23. cub
  24. clb
  25. df-txp
  26. df-pprod
  27. df-sset
  28. df-trans
  29. df-bigcup
  30. df-fix
  31. df-limits
  32. df-funs
  33. df-singleton
  34. df-singles
  35. df-image
  36. df-cart
  37. df-img
  38. df-domain
  39. df-range
  40. df-cup
  41. df-cap
  42. df-restrict
  43. df-succf
  44. df-apply
  45. df-funpart
  46. df-fullfun
  47. df-ub
  48. df-lb
  49. txpss3v
  50. txprel
  51. brtxp
  52. brtxp2
  53. dfpprod2
  54. pprodcnveq
  55. pprodss4v
  56. brpprod
  57. brpprod3a
  58. brpprod3b
  59. relsset
  60. brsset
  61. idsset
  62. eltrans
  63. dfon3
  64. dfon4
  65. brtxpsd
  66. brtxpsd2
  67. brtxpsd3
  68. relbigcup
  69. brbigcup
  70. dfbigcup2
  71. fobigcup
  72. fnbigcup
  73. fvbigcup
  74. elfix
  75. elfix2
  76. dffix2
  77. fixssdm
  78. fixssrn
  79. fixcnv
  80. fixun
  81. ellimits
  82. limitssson
  83. dfom5b
  84. sscoid
  85. dffun10
  86. elfuns
  87. elfunsg
  88. brsingle
  89. elsingles
  90. fnsingle
  91. fvsingle
  92. dfsingles2
  93. snelsingles
  94. dfiota3
  95. dffv5
  96. unisnif
  97. brimage
  98. brimageg
  99. funimage
  100. fnimage
  101. imageval
  102. fvimage
  103. brcart
  104. brdomain
  105. brrange
  106. brdomaing
  107. brrangeg
  108. brimg
  109. brapply
  110. brcup
  111. brcap
  112. brsuccf
  113. funpartlem
  114. funpartfun
  115. funpartss
  116. funpartfv
  117. fullfunfnv
  118. fullfunfv
  119. brfullfun
  120. brrestrict
  121. dfrecs2
  122. dfrdg4
  123. dfint3
  124. imagesset
  125. brub
  126. brlb