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

Theorem fnfun 5483
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 5398 . 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 1649   dom cdm 4819   Fun wfun 5389    Fn wfn 5390
This theorem is referenced by:  fnrel  5484  funfni  5486  fnco  5494  fnssresb  5498  ffun  5534  f1fun  5582  f1ofun  5617  fnbrfvb  5707  fvelimab  5722  fvun1  5734  elpreima  5790  respreima  5799  fnpr  5890  fnprOLD  5891  fconst3  5895  fnexALT  5902  fnfvima  5916  fnunirn  5939  f1eqcocnv  5968  curry1  6378  curry2  6381  tfrlem2  6574  tfrlem4  6577  tfrlem11  6586  tz7.48-2  6636  tz7.49  6639  fndmeng  7120  fnfi  7321  fodomfi  7322  marypha2lem4  7379  inf0  7510  noinfepOLD  7549  r1elss  7666  dfac8alem  7844  alephfp  7923  dfac3  7936  dfac9  7950  dfac12lem1  7957  dfac12lem2  7958  r1om  8058  cfsmolem  8084  alephsing  8090  zorn2lem1  8310  zorn2lem5  8314  zorn2lem6  8315  zorn2lem7  8316  ttukeylem3  8325  ttukeylem6  8328  smobeth  8395  fpwwe2lem9  8447  wunr1om  8528  tskr1om  8576  tskr1om2  8577  uzrdg0i  11227  uzrdgsuci  11228  hashkf  11548  shftfn  11816  phimullem  13096  imasaddvallem  13682  imasvscaval  13691  frmdss2  14736  lidlval  16193  rspval  16194  iscldtop  17083  2ndcomap  17443  qtoptop  17654  basqtop  17665  qtoprest  17671  kqfvima  17684  isr0  17691  kqreglem1  17695  kqnrmlem1  17697  kqnrmlem2  17698  elrnust  18176  ustbas  18179  uniiccdif  19338  eupap1  21547  nvof1o  23884  fnct  23947  elorrvc  24501  wfrlem2  25282  wfrlem14  25294  frrlem2  25307  bpolylem  25809  filnetlem4  26102  heibor1lem  26210  ismrc  26447  dnnumch1  26811  aomclem4  26824  aomclem6  26826  frlmsslsp  26918  psgnghm  27107  stoweidlem29  27447  stoweidlem59  27477  fnresfnco  27660  funcoressn  27661  fnbrafvb  27688  tz6.12-afv  27707  afvco2  27710  bnj142  28432  bnj930  28479  bnj1371  28737  bnj1497  28768  diaf11N  31165  dibf11N  31277  dibclN  31278  dihintcl  31460
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 5398
  Copyright terms: Public domain W3C validator