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 5614  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  20543  dfringc2  20572  rngcresringcat  20584  lidlval  21147  rspval  21148  psgnghm  21517  iscldtop  23010  2ndcomap  23373  qtoptop  23615  basqtop  23626  qtoprest  23632  kqfvima  23645  isr0  23652  kqreglem1  23656  kqnrmlem1  23658  kqnrmlem2  23659  ustbas  24142  uniiccdif  25506  noextendseq  27606  madeval  27793  oldval  27795  addsval  27905  negsval  27967  negsproplem2  27971  negsunif  27997  mulsval  28048  zsex  28304  fcoinver  32584  fnpreimac  32653  elrgspnlem2  33210  mdetpmtr1  33836  sseqf  34405  sseqfv2  34407  elorrvc  34477  bnj1371  35041  bnj1497  35072  fnrelpredd  35102  gblacfnacd  35146  onvf1odlem3  35149  onvf1odlem4  35150  onvf1od  35151  filnetlem4  36425  heibor1lem  37848  diaf11N  41147  dibf11N  41259  dibclN  41260  dihintcl  41442  aks6d1c2lem4  42219  ismrc  42793  dnnumch1  43136  aomclem4  43149  aomclem6  43151  tfsconcatrev  43440  tfsnfin  43444  fnimafnex  43532  ntrclsfv1  44147  ntrneifv1  44171  climrescn  45845  icccncfext  45984  stoweidlem29  46126  stoweidlem59  46156  ovolval4lem1  46746  fnresfnco  47140  funcoressn  47141  fnfocofob  47178  fnbrafvb  47253  tz6.12-afv  47272  afvco2  47275  tz6.12-afv2  47339  fnbrafv2b  47347  imaelsetpreimafv  47494  imasetpreimafvbijlemfv  47501  imasetpreimafvbijlemfo  47504  plusfreseq  48263  ackvalsuc0val  48787