MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-f Unicode version

Definition df-f 5505
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5929, dff3 5930, and dff4 5931. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cF . . 3
41, 2, 3wf 5497 . 2
53, 1wfn 5496 . . 3
63crn 4920 . . . 4
76, 2wss 3309 . . 3
85, 7wa 360 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  feq1  5623  feq2  5624  feq3  5625  nff  5636  ffn  5638  dffn2  5639  frn  5644  dffn3  5645  fss  5646  fco  5647  funssxp  5651  fun  5654  fnfco  5656  fssres  5657  fcoi2  5665  fint  5669  fin  5670  f0  5674  fconst  5676  f1ssr  5692  fof  5700  dff1o2  5726  fun11iun  5742  ffoss  5754  dff2  5929  dff3  5930  fmpt  5938  ffnfv  5942  ffvresb  5948  fpr  5962  idref  6027  dff1o6  6061  fliftf  6085  1stcof  6424  2ndcof  6425  smores  6663  smores2  6665  iordsmo  6668  map0e  7100  sbthlem9  7274  sucdom2  7352  inf3lem6  7637  alephsmo  8034  alephsing  8207  axdc3lem2  8382  smobeth  8512  fpwwe2lem11  8566  gch3  8602  gruiun  8725  gruima  8728  nqerf  8858  om2uzf1oi  11344  fclim  12398  invf  14044  funcres2b  14145  funcres2c  14149  hofcllem  14406  hofcl  14407  resmhm2b  14812  gsumval2  14834  frmdss2  14859  gsumval3a  15563  subgdmdprd  15643  cnrest  17400  cnrest2  17401  lmss  17413  concn  17540  txflf  18089  cnextf  18148  clsnsg  18190  tgpconcomp  18193  psmetxrge0  18395  causs  19302  ellimc2  19815  perfdvf  19841  c1lip2  19933  dvne0  19946  plyeq0  20181  plyreres  20251  aannenlem1  20296  taylf  20328  ulmss  20364  ausisusgra  21431  usgraedgrnv  21448  usgraexmpl  21471  cusgrarn  21519  hhssnv  22815  pjfi  23257  fdmrn  24087  measdivcstOLD  24627  sitgf  24709  maprnin  24735  eulerpartlemn  24767  cvmlift2lem9a  25094  elno2  25713  elno3  25714  nodenselem6  25745  mptelee  25938  isbnd3  26604  lsslindf  27456  indlcim  27466  dvsid  27704  stoweidlem27  27930  stoweidlem29  27932  stoweidlem31  27934  ffnafv  28190  sbcfg  28255  uhgraedgrnv  28490  dihf11lem  32304
  Copyright terms: Public domain W3C validator