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

Definition df-f 5442
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5871, dff3 5872, and dff4 5873. (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 5434 . 2
53, 1wfn 5433 . . 3
63crn 4863 . . . 4
76, 2wss 3365 . . 3
85, 7wa 360 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  feq1  5560  feq2  5561  feq3  5562  nff  5573  sbcfg  5575  ffn  5577  dffn2  5578  frn  5583  dffn3  5584  fss  5585  fco  5586  funssxp  5589  fun  5592  fnfco  5594  fssres  5595  fcoi2  5603  fint  5607  fin  5608  f0  5609  fconst  5613  f1ssr  5629  fof  5637  dff1o2  5663  dff2  5871  dff3  5872  fmpt  5880  ffnfv  5884  ffvresb  5889  fpr  5905  idref  5972  dff1o6  5994  fliftf  6018  fun11iun  6544  ffoss  6545  1stcof  6610  2ndcof  6611  smores  6776  smores2  6778  iordsmo  6781  map0e  7214  sbthlem9  7390  sucdom2  7468  inf3lem6  7755  alephsmo  8154  alephsing  8327  axdc3lem2  8502  smobeth  8632  fpwwe2lem11  8686  gch3  8722  gruiun  8845  gruima  8848  nqerf  8978  om2uzf1oi  11625  fclim  12878  invf  14547  funcres2b  14648  funcres2c  14652  hofcllem  14909  hofcl  14910  resmhm2b  15328  gsumval2  15351  frmdss2  15379  gsumval3a  16122  subgdmdprd  16207  cnrest  18363  cnrest2  18364  lmss  18376  concn  18504  txflf  19053  cnextf  19112  clsnsg  19154  tgpconcomp  19157  psmetxrge0  19359  causs  20266  ellimc2  20779  perfdvf  20805  c1lip2  20897  dvne0  20910  plyeq0  21145  plyreres  21215  aannenlem1  21260  taylf  21292  ulmss  21328  ausisusgra  22401  usgraedgrnv  22418  usgraexmpl  22441  cusgrarn  22489  hhssnv  23787  pjfi  24229  fdmrn  25074  maprnin  25161  measdivcstOLD  25818  sitgf  25907  eulerpartlemn  25938  cvmlift2lem9a  26338  elno2  26948  elno3  26949  nodenselem6  26980  mptelee  27173  isbnd3  27865  lsslindf  28640  indlcim  28650  dvsid  28779  stoweidlem27  29001  stoweidlem29  29003  stoweidlem31  29005  ffnafv  29256  uhgraedgrnv  29454  dihf11lem  33614
  Copyright terms: Public domain W3C validator