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

Definition df-f 5421
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5843, dff3 5844, and dff4 5845. (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 5413 . 2
53, 1wfn 5412 . . 3
63crn 4845 . . . 4
76, 2wss 3353 . . 3
85, 7wa 360 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  feq1  5539  feq2  5540  feq3  5541  nff  5552  sbcfg  5554  ffn  5556  dffn2  5557  frn  5562  dffn3  5563  fss  5564  fco  5565  funssxp  5568  fun  5571  fnfco  5573  fssres  5574  fcoi2  5582  fint  5586  fin  5587  f0  5588  fconst  5590  f1ssr  5606  fof  5614  dff1o2  5640  dff2  5843  dff3  5844  fmpt  5852  ffnfv  5856  ffvresb  5861  fpr  5876  idref  5936  dff1o6  5958  fliftf  5982  fun11iun  6499  ffoss  6500  1stcof  6565  2ndcof  6566  smores  6726  smores2  6728  iordsmo  6731  map0e  7163  sbthlem9  7337  sucdom2  7415  inf3lem6  7700  alephsmo  8097  alephsing  8270  axdc3lem2  8445  smobeth  8575  fpwwe2lem11  8629  gch3  8665  gruiun  8788  gruima  8791  nqerf  8921  om2uzf1oi  11568  fclim  12817  invf  14484  funcres2b  14585  funcres2c  14589  hofcllem  14846  hofcl  14847  resmhm2b  15264  gsumval2  15286  frmdss2  15311  gsumval3a  16015  subgdmdprd  16095  cnrest  17852  cnrest2  17853  lmss  17865  concn  17993  txflf  18542  cnextf  18601  clsnsg  18643  tgpconcomp  18646  psmetxrge0  18848  causs  19755  ellimc2  20268  perfdvf  20294  c1lip2  20386  dvne0  20399  plyeq0  20634  plyreres  20704  aannenlem1  20749  taylf  20781  ulmss  20817  ausisusgra  21889  usgraedgrnv  21906  usgraexmpl  21929  cusgrarn  21977  hhssnv  23275  pjfi  23717  fdmrn  24565  maprnin  24652  measdivcstOLD  25309  sitgf  25398  eulerpartlemn  25429  cvmlift2lem9a  25829  elno2  26439  elno3  26440  nodenselem6  26471  mptelee  26664  isbnd3  27356  lsslindf  28206  indlcim  28216  dvsid  28454  stoweidlem27  28676  stoweidlem29  28678  stoweidlem31  28680  ffnafv  28933  uhgraedgrnv  29132  dihf11lem  33337
  Copyright terms: Public domain W3C validator