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

Theorem fnfun 5357
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 5274 . 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 1632   dom cdm 4705   Fun wfun 5265    Fn wfn 5266
This theorem is referenced by:  fnrel  5358  funfni  5360  fnco  5368  fnssresb  5372  ffun  5407  f1fun  5455  f1ofun  5490  fnbrfvb  5579  fvelimab  5594  fvun1  5606  elpreima  5661  respreima  5670  fconst3  5751  fnexALT  5758  fnfvima  5772  fnunirn  5794  f1eqcocnv  5821  curry1  6226  curry2  6229  tfrlem2  6408  tfrlem4  6411  tfrlem11  6420  tz7.48-2  6470  tz7.49  6473  fndmeng  6953  fnfi  7150  fodomfi  7151  marypha2lem4  7207  inf0  7338  noinfepOLD  7377  r1elss  7494  dfac8alem  7672  alephfp  7751  dfac3  7764  dfac9  7778  dfac12lem1  7785  dfac12lem2  7786  r1om  7886  cfsmolem  7912  alephsing  7918  zorn2lem1  8139  zorn2lem5  8143  zorn2lem6  8144  zorn2lem7  8145  ttukeylem3  8154  ttukeylem6  8157  smobeth  8224  fpwwe2lem9  8276  wunr1om  8357  tskr1om  8405  tskr1om2  8406  uzrdg0i  11038  uzrdgsuci  11039  hashkf  11355  shftfn  11584  phimullem  12863  imasaddvallem  13447  imasvscaval  13456  frmdss2  14501  lidlval  15962  rspval  15963  iscldtop  16848  2ndcomap  17200  qtoptop  17407  basqtop  17418  qtoprest  17424  kqfvima  17437  isr0  17444  kqreglem1  17448  kqnrmlem1  17450  kqnrmlem2  17451  uniiccdif  18949  ipasslem8  21431  nvof1o  23052  fnct  23356  elorrvc  23679  eupap1  23915  wfrlem2  24328  wfrlem14  24340  frrlem2  24353  bpolylem  24855  npincppr  25262  repfuntw  25263  prl2  25272  cur1vald  25302  domrancur1b  25303  domrancur1c  25305  valcurfn1  25307  nsn  25633  tartarmap  25991  fnctartar  26010  fnctartar2  26011  fnckleb  26149  filnetlem4  26433  heibor1lem  26636  ismrc  26879  dnnumch1  27244  aomclem4  27257  aomclem6  27259  frlmsslsp  27351  psgnghm  27540  stoweidlem29  27881  stoweidlem59  27911  fnresfnco  28094  funcoressn  28095  fnbrafvb  28122  tz6.12-afv  28141  afvco2  28144  bnj142  29070  bnj930  29117  bnj1371  29375  bnj1497  29406  diaf11N  31861  dibf11N  31973  dibclN  31974  dihintcl  32156
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 5274
  Copyright terms: Public domain W3C validator