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

Definition df-f 5398
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5820, dff3 5821, and dff4 5822. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )

Detailed syntax breakdown of Definition df-f
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3wf 5390 . 2  wff  F : A
--> B
53, 1wfn 5389 . . 3  wff  F  Fn  A
63crn 4819 . . . 4  class  ran  F
76, 2wss 3263 . . 3  wff  ran  F  C_  B
85, 7wa 359 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 177 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff set class
This definition is referenced by:  feq1  5516  feq2  5517  feq3  5518  nff  5529  ffn  5531  dffn2  5532  frn  5537  dffn3  5538  fss  5539  fco  5540  funssxp  5544  fun  5547  fnfco  5549  fssres  5550  fcoi2  5558  fint  5562  fin  5563  f0  5567  fconst  5569  f1ssr  5585  fof  5593  dff1o2  5619  fun11iun  5635  ffoss  5647  dff2  5820  dff3  5821  fmpt  5829  ffnfv  5833  ffvresb  5839  fpr  5853  idref  5918  dff1o6  5952  fliftf  5976  1stcof  6313  2ndcof  6314  smores  6550  smores2  6552  iordsmo  6555  map0e  6987  sbthlem9  7161  sucdom2  7239  inf3lem6  7521  alephsmo  7916  alephsing  8089  axdc3lem2  8264  smobeth  8394  fpwwe2lem11  8448  gch3  8488  gruiun  8607  gruima  8610  nqerf  8740  om2uzf1oi  11220  fclim  12274  invf  13920  funcres2b  14021  funcres2c  14025  hofcllem  14282  hofcl  14283  resmhm2b  14688  gsumval2  14710  frmdss2  14735  gsumval3a  15439  subgdmdprd  15519  cnrest  17271  cnrest2  17272  lmss  17284  concn  17410  txflf  17959  cnextf  18018  clsnsg  18060  tgpconcomp  18063  causs  19122  ellimc2  19631  perfdvf  19657  c1lip2  19749  dvne0  19762  plyeq0  19997  plyreres  20067  aannenlem1  20112  taylf  20144  ulmss  20180  ausisusgra  21247  usgraedgrnv  21264  usgraexmpl  21286  cusgrarn  21334  hhssnv  22612  pjfi  23054  fdmrn  23882  measdivcstOLD  24372  cvmlift2lem9a  24769  elno2  25332  elno3  25333  nodenselem6  25364  mptelee  25548  isbnd3  26184  lsslindf  26969  indlcim  26979  dvsid  27217  stoweidlem27  27444  stoweidlem29  27446  stoweidlem31  27448  ffnafv  27704  dihf11lem  31381
  Copyright terms: Public domain W3C validator