Theorem fnfun 6581

Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fnfun	⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Proof of Theorem fnfun

Step	Hyp	Ref	Expression
1		df-fn 6484	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simplbi 497	1 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5616  Fun wfun 6475   Fn wfn 6476

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 207  df-an 396  df-fn 6484

This theorem is referenced by:  fnfund  6582  fnrel  6583  funfni  6587  fncofn  6598  fnco  6599  fnssresb  6603  ffun  6654  f1fun  6721  f1ofun  6765  fnbrfvb  6872  fvelima2  6874  fvelimad  6889  fvelimab  6894  fvun1  6913  elpreima  6991  respreima  6999  rescnvimafod  7006  fnsnr  7097  fnsnbg  7098  fnprb  7142  fntpb  7143  fconst3  7147  fnfvima  7167  ralima  7171  fnunirn  7187  nvof1o  7214  f1eqcocnv  7235  offun  7624  fnexALT  7883  curry1  8034  curry2  8037  fimaproj  8065  suppvalfng  8097  suppvalfn  8098  suppfnss  8119  fnsuppres  8121  frrlem2  8217  frrlem12  8227  tfrlem4  8298  tfrlem5  8299  tfrlem11  8307  tz7.48-2  8361  tz7.49  8364  naddcllem  8591  naddov2  8594  naddunif  8608  naddasslem1  8609  naddasslem2  8610  fndmeng  8957  fnfi  9087  fodomfi  9196  fodomfiOLD  9214  resfnfinfin  9221  finnzfsuppd  9257  fczfsuppd  9270  marypha2lem4  9322  inf0  9511  r1elss  9699  dfac8alem  9920  alephfp  9999  dfac3  10012  dfac9  10028  dfac12lem1  10035  dfac12lem2  10036  r1om  10134  cfsmolem  10161  alephsing  10167  zorn2lem1  10387  zorn2lem5  10391  zorn2lem6  10392  zorn2lem7  10393  ttukeylem3  10402  ttukeylem6  10405  fnct  10428  smobeth  10477  fpwwe2lem8  10529  wunr1om  10610  tskr1om  10658  tskr1om2  10659  uzrdg0i  13866  uzrdgsuci  13867  seqexw  13924  hashkf  14239  cshimadifsn  14736  cshimadifsn0  14737  shftfn  14980  phimullem  16690  imasaddvallem  17433  imasvscaval  17442  dfrngc2  20544  dfringc2  20573  rngcresringcat  20585  lidlval  21148  rspval  21149  psgnghm  21518  iscldtop  23011  2ndcomap  23374  qtoptop  23616  basqtop  23627  qtoprest  23633  kqfvima  23646  isr0  23653  kqreglem1  23657  kqnrmlem1  23659  kqnrmlem2  23660  ustbas  24143  uniiccdif  25507  noextendseq  27607  madeval  27794  oldval  27796  addsval  27906  negsval  27968  negsproplem2  27972  negsunif  27998  mulsval  28049  zsex  28305  fcoinver  32582  fnpreimac  32651  elrgspnlem2  33208  mdetpmtr1  33834  sseqf  34403  sseqfv2  34405  elorrvc  34475  bnj1371  35039  bnj1497  35070  fnrelpredd  35100  gblacfnacd  35144  onvf1odlem3  35147  onvf1odlem4  35148  onvf1od  35149  filnetlem4  36421  heibor1lem  37855  diaf11N  41094  dibf11N  41206  dibclN  41207  dihintcl  41389  aks6d1c2lem4  42166  ismrc  42740  dnnumch1  43083  aomclem4  43096  aomclem6  43098  tfsconcatrev  43387  tfsnfin  43391  fnimafnex  43479  ntrclsfv1  44094  ntrneifv1  44118  climrescn  45792  icccncfext  45931  stoweidlem29  46073  stoweidlem59  46103  ovolval4lem1  46693  fnresfnco  47078  funcoressn  47079  fnfocofob  47116  fnbrafvb  47191  tz6.12-afv  47210  afvco2  47213  tz6.12-afv2  47277  fnbrafv2b  47285  imaelsetpreimafv  47432  imasetpreimafvbijlemfv  47439  imasetpreimafvbijlemfo  47442  plusfreseq  48201  ackvalsuc0val  48725