Theorem fnfun 5660

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

Syntax hints:   -> wi 4   = wceq 1398   dom cdm 4988   Fun wfun 5564   Fn wfn 5565

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 369  df-fn 5573

This theorem is referenced by:  fnrel  5661  funfni  5663  fnco  5671  fnssresb  5675  ffun  5715  f1fun  5765  f1ofun  5800  fnbrfvb  5888  fvelimab  5904  fvun1  5919  elpreima  5983  respreima  5992  fnsnb  6066  fnprb  6106  fconst3  6110  fnfvima  6125  fnunirn  6140  nvof1o  6161  f1eqcocnv  6179  fnexALT  6739  curry1  6865  curry2  6868  suppvalfn  6898  suppfnss  6917  fnsuppres  6919  tfrlem4  7040  tfrlem5  7041  tfrlem11  7049  tz7.48-2  7099  tz7.49  7102  fndmeng  7585  fnfi  7790  fodomfi  7791  fczfsuppd  7839  marypha2lem4  7890  inf0  8029  noinfepOLD  8068  r1elss  8215  dfac8alem  8401  alephfp  8480  dfac3  8493  dfac9  8507  dfac12lem1  8514  dfac12lem2  8515  r1om  8615  cfsmolem  8641  alephsing  8647  zorn2lem1  8867  zorn2lem5  8871  zorn2lem6  8872  zorn2lem7  8873  ttukeylem3  8882  ttukeylem6  8885  smobeth  8952  fpwwe2lem9  9005  wunr1om  9086  tskr1om  9134  tskr1om2  9135  uzrdg0i  12052  uzrdgsuci  12053  hashkf  12389  shftfn  12988  phimullem  14393  imasaddvallem  15018  imasvscaval  15027  frmdss2  16230  dprdvalOLD  17231  lcomfsupp  17745  lidlval  18033  rspval  18034  psrbagev1  18372  psgnghm  18789  frlmsslsp  18998  iscldtop  19763  2ndcomap  20125  qtoptop  20367  basqtop  20378  qtoprest  20384  kqfvima  20397  isr0  20404  kqreglem1  20408  kqnrmlem1  20410  kqnrmlem2  20411  elrnust  20893  ustbas  20896  uniiccdif  22153  eupap1  25178  fcoinver  27674  fnct  27766  fimaproj  28071  sseqf  28595  sseqfv2  28597  elorrvc  28666  wfrlem2  29584  wfrlem14  29596  frrlem2  29628  filnetlem4  30439  heibor1lem  30545  ismrc  30873  dnnumch1  31229  aomclem4  31242  aomclem6  31244  icccncfext  31929  stoweidlem29  32050  stoweidlem59  32080  fnresfnco  32450  funcoressn  32451  fnbrafvb  32478  tz6.12-afv  32497  afvco2  32500  resfnfinfin  32684  plusfreseq  32832  dfrngc2  33034  dfringc2  33080  rngcresringcat  33092  mndpsuppss  33218  mndpfsupp  33223  bnj142OLD  34182  bnj930  34229  bnj1371  34486  bnj1497  34517  diaf11N  37173  dibf11N  37285  dibclN  37286  dihintcl  37468