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

Definition df-f 5597
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 6043, dff3 6044, and dff4 6045. (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 5589 . 2
53, 1wfn 5588 . . 3
63crn 5005 . . . 4
76, 2wss 3475 . . 3
85, 7wa 369 . 2
94, 8wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  feq1  5718  feq2  5719  feq3  5720  nff  5732  sbcfg  5734  ffn  5736  dffn2  5737  frn  5742  dffn3  5743  fss  5744  fco  5746  funssxp  5749  fdmrn  5751  fun  5753  fnfco  5755  fssres  5756  fcoi2  5765  fint  5769  fin  5770  f0  5771  fconst  5776  f1ssr  5792  fof  5800  dff1o2  5826  dff2  6043  dff3  6044  fmpt  6052  ffnfv  6057  ffvresb  6062  fpr  6079  idref  6153  dff1o6  6181  fliftf  6213  fun11iun  6760  ffoss  6761  1stcof  6828  2ndcof  6829  smores  7042  smores2  7044  iordsmo  7047  sbthlem9  7655  sucdom2  7734  inf3lem6  8071  alephsmo  8504  alephsing  8677  axdc3lem2  8852  smobeth  8982  fpwwe2lem11  9039  gch3  9075  gruiun  9198  gruima  9201  nqerf  9329  om2uzf1oi  12064  fclim  13376  invf  15162  funcres2b  15266  funcres2c  15270  hofcllem  15527  hofcl  15528  gsumval2  15907  resmhm2b  15992  frmdss2  16031  gsumval3a  16905  gsumval3aOLD  16906  subgdmdprd  17081  lsslindf  18865  indlcim  18875  cnrest2  19787  lmss  19799  concn  19927  txflf  20507  cnextf  20566  clsnsg  20608  tgpconcomp  20611  psmetxrge0  20817  causs  21737  ellimc2  22281  perfdvf  22307  c1lip2  22399  dvne0  22412  plyeq0  22608  plyreres  22679  aannenlem1  22724  taylf  22756  ulmss  22792  mptelee  24198  ausisusgra  24355  usgraedgrnv  24377  usgraexmpl  24401  cusgrarn  24459  hhssnv  26180  pjfi  26622  maprnin  27554  measdivcstOLD  28195  sitgf  28289  eulerpartlemn  28320  cvmlift2lem9a  28748  elno2  29414  elno3  29415  nodenselem6  29446  isbnd3  30280  dvsid  31236  stoweidlem27  31809  stoweidlem29  31811  stoweidlem31  31813  fourierdlem15  31904  ffnafv  32256  uhgraedgrnv  32349  resmgmhm2b  32488  dihf11lem  36993
  Copyright terms: Public domain W3C validator