Theorem fnfun 6586

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 6489	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simplbi 497	1 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5623  Fun wfun 6480   Fn wfn 6481

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 6489

This theorem is referenced by:  fnfund  6587  fnrel  6588  funfni  6592  fncofn  6603  fnco  6604  fnssresb  6608  ffun  6659  f1fun  6726  f1ofun  6770  fnbrfvb  6877  fvelima2  6879  fvelimad  6894  fvelimab  6899  fvun1  6918  elpreima  6996  respreima  7004  rescnvimafod  7011  fnsnr  7103  fnsnbg  7104  fnprb  7148  fntpb  7149  fconst3  7153  fnfvima  7173  ralima  7177  fnunirn  7194  nvof1o  7221  f1eqcocnv  7242  offun  7631  fnexALT  7893  curry1  8044  curry2  8047  fimaproj  8075  suppvalfng  8107  suppvalfn  8108  suppfnss  8129  fnsuppres  8131  frrlem2  8227  frrlem12  8237  tfrlem4  8308  tfrlem5  8309  tfrlem11  8317  tz7.48-2  8371  tz7.49  8374  naddcllem  8601  naddov2  8604  naddunif  8618  naddasslem1  8619  naddasslem2  8620  fndmeng  8967  fnfi  9102  fodomfi  9219  fodomfiOLD  9239  resfnfinfin  9246  finnzfsuppd  9282  fczfsuppd  9295  marypha2lem4  9347  inf0  9536  r1elss  9721  dfac8alem  9942  alephfp  10021  dfac3  10034  dfac9  10050  dfac12lem1  10057  dfac12lem2  10058  r1om  10156  cfsmolem  10183  alephsing  10189  zorn2lem1  10409  zorn2lem5  10413  zorn2lem6  10414  zorn2lem7  10415  ttukeylem3  10424  ttukeylem6  10427  fnct  10450  smobeth  10499  fpwwe2lem8  10551  wunr1om  10632  tskr1om  10680  tskr1om2  10681  uzrdg0i  13884  uzrdgsuci  13885  seqexw  13942  hashkf  14257  cshimadifsn  14754  cshimadifsn0  14755  shftfn  14998  phimullem  16708  imasaddvallem  17451  imasvscaval  17460  dfrngc2  20531  dfringc2  20560  rngcresringcat  20572  lidlval  21135  rspval  21136  psgnghm  21505  iscldtop  22998  2ndcomap  23361  qtoptop  23603  basqtop  23614  qtoprest  23620  kqfvima  23633  isr0  23640  kqreglem1  23644  kqnrmlem1  23646  kqnrmlem2  23647  ustbas  24131  uniiccdif  25495  noextendseq  27595  madeval  27780  oldval  27782  addsval  27892  negsval  27954  negsproplem2  27958  negsunif  27984  mulsval  28035  zsex  28291  fcoinver  32566  fnpreimac  32628  elrgspnlem2  33193  mdetpmtr1  33789  sseqf  34359  sseqfv2  34361  elorrvc  34431  bnj1371  34995  bnj1497  35026  fnrelpredd  35055  gblacfnacd  35074  onvf1odlem3  35077  onvf1odlem4  35078  onvf1od  35079  filnetlem4  36354  heibor1lem  37788  diaf11N  41028  dibf11N  41140  dibclN  41141  dihintcl  41323  aks6d1c2lem4  42100  ismrc  42674  dnnumch1  43017  aomclem4  43030  aomclem6  43032  tfsconcatrev  43321  tfsnfin  43325  fnimafnex  43413  ntrclsfv1  44028  ntrneifv1  44052  climrescn  45730  icccncfext  45869  stoweidlem29  46011  stoweidlem59  46041  ovolval4lem1  46631  fnresfnco  47026  funcoressn  47027  fnfocofob  47064  fnbrafvb  47139  tz6.12-afv  47158  afvco2  47161  tz6.12-afv2  47225  fnbrafv2b  47233  imaelsetpreimafv  47380  imasetpreimafvbijlemfv  47387  imasetpreimafvbijlemfo  47390  plusfreseq  48149  ackvalsuc0val  48673