Theorem fnfun 5615

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 5528	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simplbi 460	1 |- ( F Fn A -> Fun F )

Syntax hints:   -> wi 4   = wceq 1370   dom cdm 4947   Fun wfun 5519   Fn wfn 5520

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 5528

This theorem is referenced by:  fnrel  5616  funfni  5618  fnco  5626  fnssresb  5630  ffun  5668  f1fun  5715  f1ofun  5750  fnbrfvb  5840  fvelimab  5855  fvun1  5870  elpreima  5931  respreima  5940  fnsnb  6006  fnprb  6044  fnprOLD  6045  fconst3  6049  fnfvima  6063  fnunirn  6078  nvof1o  6095  f1eqcocnv  6107  fnexALT  6652  curry1  6773  curry2  6776  suppvalfn  6806  suppfnss  6823  fnsuppres  6825  tfrlem4  6947  tfrlem5  6948  tfrlem11  6956  tz7.48-2  7006  tz7.49  7009  fndmeng  7495  fnfi  7699  fodomfi  7700  fczfsuppd  7748  marypha2lem4  7798  inf0  7937  noinfepOLD  7976  r1elss  8123  dfac8alem  8309  alephfp  8388  dfac3  8401  dfac9  8415  dfac12lem1  8422  dfac12lem2  8423  r1om  8523  cfsmolem  8549  alephsing  8555  zorn2lem1  8775  zorn2lem5  8779  zorn2lem6  8780  zorn2lem7  8781  ttukeylem3  8790  ttukeylem6  8793  smobeth  8860  fpwwe2lem9  8915  wunr1om  8996  tskr1om  9044  tskr1om2  9045  uzrdg0i  11898  uzrdgsuci  11899  hashkf  12221  shftfn  12679  phimullem  13971  imasaddvallem  14585  imasvscaval  14594  frmdss2  15659  dprdvalOLD  16608  lcomfsupp  17107  lidlval  17395  rspval  17396  psrbagev1  17717  psgnghm  18134  frlmsslsp  18347  frlmsslspOLD  18348  iscldtop  18830  2ndcomap  19193  qtoptop  19404  basqtop  19415  qtoprest  19421  kqfvima  19434  isr0  19441  kqreglem1  19445  kqnrmlem1  19447  kqnrmlem2  19448  elrnust  19930  ustbas  19933  uniiccdif  21190  eupap1  23748  fnct  26163  sseqf  26918  sseqfv2  26920  elorrvc  26989  wfrlem2  27868  wfrlem14  27880  frrlem2  27912  bpolylem  28334  filnetlem4  28749  heibor1lem  28855  ismrc  29184  dnnumch1  29544  aomclem4  29557  aomclem6  29559  stoweidlem29  29971  stoweidlem59  30001  fnresfnco  30179  funcoressn  30180  fnbrafvb  30207  tz6.12-afv  30226  afvco2  30229  resfnfinfin  30312  mndpsuppss  30931  mndpfsupp  30937  bnj142OLD  32034  bnj930  32080  bnj1371  32337  bnj1497  32368  diaf11N  35017  dibf11N  35129  dibclN  35130  dihintcl  35312