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

Definition df-f 5421
Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5844, dff3 5845, and dff4 5846. (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 5413 . 2  wff  F : A
--> B
53, 1wfn 5412 . . 3  wff  F  Fn  A
63crn 4842 . . . 4  class  ran  F
76, 2wss 3284 . . 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  5539  feq2  5540  feq3  5541  nff  5552  ffn  5554  dffn2  5555  frn  5560  dffn3  5561  fss  5562  fco  5563  funssxp  5567  fun  5570  fnfco  5572  fssres  5573  fcoi2  5581  fint  5585  fin  5586  f0  5590  fconst  5592  f1ssr  5608  fof  5616  dff1o2  5642  fun11iun  5658  ffoss  5670  dff2  5844  dff3  5845  fmpt  5853  ffnfv  5857  ffvresb  5863  fpr  5877  idref  5942  dff1o6  5976  fliftf  6000  1stcof  6337  2ndcof  6338  smores  6577  smores2  6579  iordsmo  6582  map0e  7014  sbthlem9  7188  sucdom2  7266  inf3lem6  7548  alephsmo  7943  alephsing  8116  axdc3lem2  8291  smobeth  8421  fpwwe2lem11  8475  gch3  8515  gruiun  8634  gruima  8637  nqerf  8767  om2uzf1oi  11252  fclim  12306  invf  13952  funcres2b  14053  funcres2c  14057  hofcllem  14314  hofcl  14315  resmhm2b  14720  gsumval2  14742  frmdss2  14767  gsumval3a  15471  subgdmdprd  15551  cnrest  17307  cnrest2  17308  lmss  17320  concn  17446  txflf  17995  cnextf  18054  clsnsg  18096  tgpconcomp  18099  psmetxrge0  18301  causs  19208  ellimc2  19721  perfdvf  19747  c1lip2  19839  dvne0  19852  plyeq0  20087  plyreres  20157  aannenlem1  20202  taylf  20234  ulmss  20270  ausisusgra  21337  usgraedgrnv  21354  usgraexmpl  21377  cusgrarn  21425  hhssnv  22721  pjfi  23163  fdmrn  23996  measdivcstOLD  24535  sitgf  24617  cvmlift2lem9a  24947  elno2  25526  elno3  25527  nodenselem6  25558  mptelee  25742  isbnd3  26387  lsslindf  27172  indlcim  27182  dvsid  27420  stoweidlem27  27647  stoweidlem29  27649  stoweidlem31  27651  ffnafv  27906  uhgraedgrnv  28036  dihf11lem  31753
  Copyright terms: Public domain W3C validator