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

Definition df-f 5500
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5945, dff3 5946, and dff4 5947. (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 5492 . 2  wff  F : A
--> B
53, 1wfn 5491 . . 3  wff  F  Fn  A
63crn 4914 . . . 4  class  ran  F
76, 2wss 3389 . . 3  wff  ran  F  C_  B
85, 7wa 367 . 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  5621  feq2  5622  feq3  5623  nff  5635  sbcfg  5637  ffn  5639  dffn2  5640  frn  5645  dffn3  5646  fss  5647  fco  5649  funssxp  5652  fdmrn  5654  fun  5656  fnfco  5658  fssres  5659  fcoi2  5668  fint  5672  fin  5673  f0  5674  fconst  5679  f1ssr  5695  fof  5703  dff1o2  5729  dff2  5945  dff3  5946  fmpt  5954  ffnfv  5959  ffvresb  5964  fpr  5981  idref  6054  dff1o6  6082  fliftf  6114  fun11iun  6659  ffoss  6660  1stcof  6727  2ndcof  6728  smores  6941  smores2  6943  iordsmo  6946  sbthlem9  7554  sucdom2  7632  inf3lem6  7964  alephsmo  8396  alephsing  8569  axdc3lem2  8744  smobeth  8874  fpwwe2lem11  8929  gch3  8965  gruiun  9088  gruima  9091  nqerf  9219  om2uzf1oi  11967  fclim  13378  invf  15174  funcres2b  15303  funcres2c  15307  hofcllem  15644  hofcl  15645  gsumval2  16024  resmhm2b  16109  frmdss2  16148  gsumval3a  17022  gsumval3aOLD  17023  subgdmdprd  17194  lsslindf  18950  indlcim  18960  cnrest2  19873  lmss  19885  concn  20012  txflf  20592  cnextf  20651  clsnsg  20693  tgpconcomp  20696  psmetxrge0  20902  causs  21822  ellimc2  22366  perfdvf  22392  c1lip2  22484  dvne0  22497  plyeq0  22693  plyreres  22764  aannenlem1  22809  taylf  22841  ulmss  22877  mptelee  24319  ausisusgra  24476  usgraedgrnv  24498  usgraexmpl  24522  cusgrarn  24580  hhssnv  26297  pjfi  26739  maprnin  27704  measdivcstOLD  28351  sitgf  28472  eulerpartlemn  28503  cvmlift2lem9a  28937  elno2  29579  elno3  29580  nodenselem6  29611  isbnd3  30446  dvsid  31404  stoweidlem27  31975  stoweidlem29  31977  stoweidlem31  31979  fourierdlem15  32070  ffnafv  32422  uhgraedgrnv  32667  resmgmhm2b  32806  dihf11lem  37406
  Copyright terms: Public domain W3C validator