Theorem fnfun 5496

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

Step	Hyp	Ref	Expression
1		df-fn 5409	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simplbi 457	1 |- ( F Fn A -> Fun F )

Syntax hints:   -> wi 4   = wceq 1362   dom cdm 4827   Fun wfun 5400   Fn wfn 5401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-fn 5409

This theorem is referenced by:  fnrel  5497  funfni  5499  fnco  5507  fnssresb  5511  ffun  5549  f1fun  5596  f1ofun  5631  fnbrfvb  5720  fvelimab  5735  fvun1  5750  elpreima  5811  respreima  5820  fnsnb  5885  fnprb  5923  fnprOLD  5924  fconst3  5928  fnfvima  5942  fnunirn  5956  nvof1o  5974  f1eqcocnv  5986  fnexALT  6532  curry1  6653  curry2  6656  suppvalfn  6686  suppfnss  6703  fnsuppres  6705  tfrlem4  6824  tfrlem5  6825  tfrlem11  6833  tz7.48-2  6883  tz7.49  6886  fndmeng  7374  fnfi  7577  fodomfi  7578  fczfsuppd  7626  marypha2lem4  7676  inf0  7815  noinfepOLD  7854  r1elss  8001  dfac8alem  8187  alephfp  8266  dfac3  8279  dfac9  8293  dfac12lem1  8300  dfac12lem2  8301  r1om  8401  cfsmolem  8427  alephsing  8433  zorn2lem1  8653  zorn2lem5  8657  zorn2lem6  8658  zorn2lem7  8659  ttukeylem3  8668  ttukeylem6  8671  smobeth  8738  fpwwe2lem9  8793  wunr1om  8874  tskr1om  8922  tskr1om2  8923  uzrdg0i  11766  uzrdgsuci  11767  hashkf  12089  shftfn  12546  phimullem  13837  imasaddvallem  14450  imasvscaval  14459  frmdss2  15521  dprdvalOLD  16461  lcomfsupp  16909  lidlval  17195  rspval  17196  psrbagev1  17522  psgnghm  17852  frlmsslsp  18065  frlmsslspOLD  18066  iscldtop  18541  2ndcomap  18904  qtoptop  19115  basqtop  19126  qtoprest  19132  kqfvima  19145  isr0  19152  kqreglem1  19156  kqnrmlem1  19158  kqnrmlem2  19159  elrnust  19641  ustbas  19644  uniiccdif  20900  eupap1  23420  fnct  25837  sseqf  26623  sseqfv2  26625  elorrvc  26694  wfrlem2  27572  wfrlem14  27584  frrlem2  27616  bpolylem  28038  filnetlem4  28446  heibor1lem  28552  ismrc  28882  dnnumch1  29242  aomclem4  29255  aomclem6  29257  stoweidlem29  29670  stoweidlem59  29700  fnresfnco  29878  funcoressn  29879  fnbrafvb  29906  tz6.12-afv  29925  afvco2  29928  resfnfinfin  30011  mndpsuppss  30616  mndpfsupp  30621  bnj142OLD  31440  bnj930  31486  bnj1371  31743  bnj1497  31774  diaf11N  34288  dibf11N  34400  dibclN  34401  dihintcl  34583