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

Definition df-f 5585
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 6026, dff3 6027, and dff4 6028. (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 5577 . 2  wff  F : A
--> B
53, 1wfn 5576 . . 3  wff  F  Fn  A
63crn 4995 . . . 4  class  ran  F
76, 2wss 3471 . . 3  wff  ran  F  C_  B
85, 7wa 369 . 2  wff  ( F  Fn  A  /\  ran  F 
C_  B )
94, 8wb 184 1  wff  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
Colors of variables: wff setvar class
This definition is referenced by:  feq1  5706  feq2  5707  feq3  5708  nff  5720  sbcfg  5722  ffn  5724  dffn2  5725  frn  5730  dffn3  5731  fss  5732  fco  5734  funssxp  5737  fdmrn  5739  fun  5741  fnfco  5743  fssres  5744  fcoi2  5753  fint  5757  fin  5758  f0  5759  fconst  5764  f1ssr  5780  fof  5788  dff1o2  5814  dff2  6026  dff3  6027  fmpt  6035  ffnfv  6040  ffvresb  6045  fpr  6062  idref  6134  dff1o6  6162  fliftf  6194  fun11iun  6736  ffoss  6737  1stcof  6804  2ndcof  6805  smores  7015  smores2  7017  iordsmo  7020  map0e  7448  sbthlem9  7627  sucdom2  7706  inf3lem6  8041  alephsmo  8474  alephsing  8647  axdc3lem2  8822  smobeth  8952  fpwwe2lem11  9009  gch3  9045  gruiun  9168  gruima  9171  nqerf  9299  om2uzf1oi  12022  fclim  13327  invf  15014  funcres2b  15115  funcres2c  15119  hofcllem  15376  hofcl  15377  resmhm2b  15797  gsumval2  15821  frmdss2  15849  gsumval3a  16691  gsumval3aOLD  16692  subgdmdprd  16866  lsslindf  18627  indlcim  18637  cnrest  19547  cnrest2  19548  lmss  19560  concn  19688  txflf  20237  cnextf  20296  clsnsg  20338  tgpconcomp  20341  psmetxrge0  20547  causs  21467  ellimc2  22011  perfdvf  22037  c1lip2  22129  dvne0  22142  plyeq0  22338  plyreres  22408  aannenlem1  22453  taylf  22485  ulmss  22521  mptelee  23869  ausisusgra  24020  usgraedgrnv  24041  usgraexmpl  24065  cusgrarn  24123  hhssnv  25844  pjfi  26286  maprnin  27214  measdivcstOLD  27823  sitgf  27917  eulerpartlemn  27948  cvmlift2lem9a  28376  elno2  28979  elno3  28980  nodenselem6  29011  isbnd3  29872  dvsid  30793  stoweidlem27  31284  stoweidlem29  31286  stoweidlem31  31288  fourierdlem15  31379  ffnafv  31680  uhgraedgrnv  31775  dihf11lem  35940
  Copyright terms: Public domain W3C validator