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

Definition df-f 5417
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5840, dff3 5841, and dff4 5842. (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 5409 . 2  wff  F : A
--> B
53, 1wfn 5408 . . 3  wff  F  Fn  A
63crn 4838 . . . 4  class  ran  F
76, 2wss 3280 . . 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  5535  feq2  5536  feq3  5537  nff  5548  ffn  5550  dffn2  5551  frn  5556  dffn3  5557  fss  5558  fco  5559  funssxp  5563  fun  5566  fnfco  5568  fssres  5569  fcoi2  5577  fint  5581  fin  5582  f0  5586  fconst  5588  f1ssr  5604  fof  5612  dff1o2  5638  fun11iun  5654  ffoss  5666  dff2  5840  dff3  5841  fmpt  5849  ffnfv  5853  ffvresb  5859  fpr  5873  idref  5938  dff1o6  5972  fliftf  5996  1stcof  6333  2ndcof  6334  smores  6573  smores2  6575  iordsmo  6578  map0e  7010  sbthlem9  7184  sucdom2  7262  inf3lem6  7544  alephsmo  7939  alephsing  8112  axdc3lem2  8287  smobeth  8417  fpwwe2lem11  8471  gch3  8511  gruiun  8630  gruima  8633  nqerf  8763  om2uzf1oi  11248  fclim  12302  invf  13948  funcres2b  14049  funcres2c  14053  hofcllem  14310  hofcl  14311  resmhm2b  14716  gsumval2  14738  frmdss2  14763  gsumval3a  15467  subgdmdprd  15547  cnrest  17303  cnrest2  17304  lmss  17316  concn  17442  txflf  17991  cnextf  18050  clsnsg  18092  tgpconcomp  18095  psmetxrge0  18297  causs  19204  ellimc2  19717  perfdvf  19743  c1lip2  19835  dvne0  19848  plyeq0  20083  plyreres  20153  aannenlem1  20198  taylf  20230  ulmss  20266  ausisusgra  21333  usgraedgrnv  21350  usgraexmpl  21373  cusgrarn  21421  hhssnv  22717  pjfi  23159  fdmrn  23992  measdivcstOLD  24531  sitgf  24613  cvmlift2lem9a  24943  elno2  25522  elno3  25523  nodenselem6  25554  mptelee  25738  isbnd3  26383  lsslindf  27168  indlcim  27178  dvsid  27416  stoweidlem27  27643  stoweidlem29  27645  stoweidlem31  27647  ffnafv  27902  uhgraedgrnv  28032  dihf11lem  31749
  Copyright terms: Public domain W3C validator