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

Theorem fnfun 5534
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 5449 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simplbi 447 1  |-  ( F  Fn  A  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   dom cdm 4870   Fun wfun 5440    Fn wfn 5441
This theorem is referenced by:  fnrel  5535  funfni  5537  fnco  5545  fnssresb  5549  ffun  5585  f1fun  5633  f1ofun  5668  fnbrfvb  5759  fvelimab  5774  fvun1  5786  elpreima  5842  respreima  5851  fnpr  5942  fnprOLD  5943  fconst3  5947  fnexALT  5954  fnfvima  5968  fnunirn  5991  f1eqcocnv  6020  curry1  6430  curry2  6433  tfrlem2  6629  tfrlem4  6632  tfrlem11  6641  tz7.48-2  6691  tz7.49  6694  fndmeng  7175  fnfi  7376  fodomfi  7377  marypha2lem4  7435  inf0  7568  noinfepOLD  7607  r1elss  7724  dfac8alem  7902  alephfp  7981  dfac3  7994  dfac9  8008  dfac12lem1  8015  dfac12lem2  8016  r1om  8116  cfsmolem  8142  alephsing  8148  zorn2lem1  8368  zorn2lem5  8372  zorn2lem6  8373  zorn2lem7  8374  ttukeylem3  8383  ttukeylem6  8386  smobeth  8453  fpwwe2lem9  8505  wunr1om  8586  tskr1om  8634  tskr1om2  8635  uzrdg0i  11291  uzrdgsuci  11292  hashkf  11612  shftfn  11880  phimullem  13160  imasaddvallem  13746  imasvscaval  13755  frmdss2  14800  lidlval  16257  rspval  16258  iscldtop  17151  2ndcomap  17513  qtoptop  17724  basqtop  17735  qtoprest  17741  kqfvima  17754  isr0  17761  kqreglem1  17765  kqnrmlem1  17767  kqnrmlem2  17768  elrnust  18246  ustbas  18249  uniiccdif  19462  eupap1  21690  nvof1o  24032  fnct  24097  elorrvc  24713  wfrlem2  25531  wfrlem14  25543  frrlem2  25575  bpolylem  26086  filnetlem4  26401  heibor1lem  26509  ismrc  26746  dnnumch1  27110  aomclem4  27123  aomclem6  27125  frlmsslsp  27216  psgnghm  27405  stoweidlem29  27745  stoweidlem59  27775  fnresfnco  27957  funcoressn  27958  fnbrafvb  27985  tz6.12-afv  28004  afvco2  28007  resfnfinfin  28071  bnj142  29030  bnj930  29077  bnj1371  29335  bnj1497  29366  diaf11N  31784  dibf11N  31896  dibclN  31897  dihintcl  32079
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 178  df-an 361  df-fn 5449
  Copyright terms: Public domain W3C validator