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

Definition df-f 5259
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5672, dff3 5673, and dff4 5674. (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 5251 . 2  wff  F : A
--> B
53, 1wfn 5250 . . 3  wff  F  Fn  A
63crn 4690 . . . 4  class  ran  F
76, 2wss 3152 . . 3  wff  ran  F  C_  B
85, 7wa 358 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 176 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff set class
This definition is referenced by:  feq1  5375  feq2  5376  feq3  5377  nff  5387  ffn  5389  dffn2  5390  frn  5395  dffn3  5396  fss  5397  fco  5398  funssxp  5402  fun  5405  fnfco  5407  fssres  5408  fcoi2  5416  fint  5420  fin  5421  f0  5425  fconst  5427  f1ssr  5443  fof  5451  dff1o2  5477  fun11iun  5493  ffoss  5505  dff2  5672  dff3  5673  fmpt  5681  ffnfv  5685  ffvresb  5690  fpr  5704  idref  5759  dff1o6  5791  fliftf  5814  1stcof  6147  2ndcof  6148  smores  6369  smores2  6371  iordsmo  6374  map0e  6805  sbthlem9  6979  sucdom2  7057  inf3lem6  7334  alephsmo  7729  alephsing  7902  axdc3lem2  8077  smobeth  8208  fpwwe2lem11  8262  gch3  8302  gruiun  8421  gruima  8424  nqerf  8554  om2uzf1oi  11016  fclim  12027  invf  13670  funcres2b  13771  funcres2c  13775  hofcllem  14032  hofcl  14033  resmhm2b  14438  gsumval2  14460  frmdss2  14485  gsumval3a  15189  subgdmdprd  15269  cnrest  17013  cnrest2  17014  lmss  17026  concn  17152  txflf  17701  clsnsg  17792  tgpconcomp  17795  causs  18724  ellimc2  19227  perfdvf  19253  c1lip2  19345  dvne0  19358  plyeq0  19593  plyreres  19663  aannenlem1  19708  taylf  19740  ulmss  19774  hhssnv  21841  pjfi  22283  fdmrn  23035  measdivcstOLD  23551  measdivcst  23552  cvmlift2lem9a  23834  elno2  24308  elno3  24309  nodenselem6  24340  mptelee  24523  domrancur1b  25200  trnij  25615  fnckleb  26046  isbnd3  26508  lsslindf  27300  indlcim  27310  dvsid  27548  fnvinran  27685  cncmpmax  27703  stoweidlem27  27776  stoweidlem29  27778  stoweidlem31  27780  ffnafv  28033  usgraedgrnv  28123  usgraexmpl  28133  dihf11lem  31456
  Copyright terms: Public domain W3C validator