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

Definition df-f 5582
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 6028, dff3 6029, and dff4 6030. (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 5574 . 2  wff  F : A
--> B
53, 1wfn 5573 . . 3  wff  F  Fn  A
63crn 4990 . . . 4  class  ran  F
76, 2wss 3461 . . 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  5703  feq2  5704  feq3  5705  nff  5717  sbcfg  5719  ffn  5721  dffn2  5722  frn  5727  dffn3  5728  fss  5729  fco  5731  funssxp  5734  fdmrn  5736  fun  5738  fnfco  5740  fssres  5741  fcoi2  5750  fint  5754  fin  5755  f0  5756  fconst  5761  f1ssr  5777  fof  5785  dff1o2  5811  dff2  6028  dff3  6029  fmpt  6037  ffnfv  6042  ffvresb  6047  fpr  6064  idref  6138  dff1o6  6166  fliftf  6198  fun11iun  6745  ffoss  6746  1stcof  6813  2ndcof  6814  smores  7025  smores2  7027  iordsmo  7030  sbthlem9  7637  sucdom2  7716  inf3lem6  8053  alephsmo  8486  alephsing  8659  axdc3lem2  8834  smobeth  8964  fpwwe2lem11  9021  gch3  9057  gruiun  9180  gruima  9183  nqerf  9311  om2uzf1oi  12046  fclim  13358  invf  15144  funcres2b  15245  funcres2c  15249  hofcllem  15506  hofcl  15507  gsumval2  15886  resmhm2b  15971  frmdss2  16010  gsumval3a  16884  gsumval3aOLD  16885  subgdmdprd  17060  lsslindf  18843  indlcim  18853  cnrest2  19765  lmss  19777  concn  19905  txflf  20485  cnextf  20544  clsnsg  20586  tgpconcomp  20589  psmetxrge0  20795  causs  21715  ellimc2  22259  perfdvf  22285  c1lip2  22377  dvne0  22390  plyeq0  22586  plyreres  22657  aannenlem1  22702  taylf  22734  ulmss  22770  mptelee  24176  ausisusgra  24333  usgraedgrnv  24355  usgraexmpl  24379  cusgrarn  24437  hhssnv  26158  pjfi  26600  maprnin  27532  measdivcstOLD  28173  sitgf  28267  eulerpartlemn  28298  cvmlift2lem9a  28726  elno2  29390  elno3  29391  nodenselem6  29422  isbnd3  30256  dvsid  31212  stoweidlem27  31763  stoweidlem29  31765  stoweidlem31  31767  fourierdlem15  31858  ffnafv  32210  uhgraedgrnv  32303  resmgmhm2b  32442  dihf11lem  36868
  Copyright terms: Public domain W3C validator