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

Theorem fnfun 5341
Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fnfun  |-  ( F  Fn  A  ->  Fun  F )

Proof of Theorem fnfun
StepHypRef Expression
1 df-fn 5258 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simplbi 446 1  |-  ( F  Fn  A  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   dom cdm 4689   Fun wfun 5249    Fn wfn 5250
This theorem is referenced by:  fnrel  5342  funfni  5344  fnco  5352  fnssresb  5356  ffun  5391  f1fun  5439  f1ofun  5474  fnbrfvb  5563  fvelimab  5578  fvun1  5590  elpreima  5645  respreima  5654  fconst3  5735  fnexALT  5742  fnfvima  5756  fnunirn  5778  f1eqcocnv  5805  curry1  6210  curry2  6213  tfrlem2  6392  tfrlem4  6395  tfrlem11  6404  tz7.48-2  6454  tz7.49  6457  fndmeng  6937  fnfi  7134  fodomfi  7135  marypha2lem4  7191  inf0  7322  noinfepOLD  7361  r1elss  7478  dfac8alem  7656  alephfp  7735  dfac3  7748  dfac9  7762  dfac12lem1  7769  dfac12lem2  7770  r1om  7870  cfsmolem  7896  alephsing  7902  zorn2lem1  8123  zorn2lem5  8127  zorn2lem6  8128  zorn2lem7  8129  ttukeylem3  8138  ttukeylem6  8141  smobeth  8208  fpwwe2lem9  8260  wunr1om  8341  tskr1om  8389  tskr1om2  8390  uzrdg0i  11022  uzrdgsuci  11023  hashkf  11339  shftfn  11568  phimullem  12847  imasaddvallem  13431  imasvscaval  13440  frmdss2  14485  lidlval  15946  rspval  15947  iscldtop  16832  2ndcomap  17184  qtoptop  17391  basqtop  17402  qtoprest  17408  kqfvima  17421  isr0  17428  kqreglem1  17432  kqnrmlem1  17434  kqnrmlem2  17435  uniiccdif  18933  ipasslem8  21415  nvof1o  23036  fnct  23341  elorrvc  23664  eupap1  23900  wfrlem2  24257  wfrlem14  24269  frrlem2  24282  bpolylem  24783  npincppr  25159  repfuntw  25160  prl2  25169  cur1vald  25199  domrancur1b  25200  domrancur1c  25202  valcurfn1  25204  nsn  25530  tartarmap  25888  fnctartar  25907  fnctartar2  25908  fnckleb  26046  filnetlem4  26330  heibor1lem  26533  ismrc  26776  dnnumch1  27141  aomclem4  27154  aomclem6  27156  frlmsslsp  27248  psgnghm  27437  stoweidlem29  27778  stoweidlem59  27808  fnresfnco  27989  funcoressn  27990  fnbrafvb  28016  tz6.12-afv  28035  afvco2  28037  bnj142  28754  bnj930  28801  bnj1371  29059  bnj1497  29090  diaf11N  31239  dibf11N  31351  dibclN  31352  dihintcl  31534
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 5258
  Copyright terms: Public domain W3C validator