Theorem fnfun 6660

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

Syntax hints:   → wi 4   = wceq 1534  dom cdm 5682  Fun wfun 6548   Fn wfn 6549

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 206  df-an 395  df-fn 6557

This theorem is referenced by:  fnfund  6661  fnrel  6662  funfni  6666  fncofn  6677  fnco  6678  fncoOLD  6679  fnssresb  6683  ffun  6731  f1fun  6800  f1ofun  6845  fnbrfvb  6954  fvelimad  6970  fvelimab  6975  fvun1  6993  elpreima  7071  respreima  7079  rescnvimafod  7087  fnsnr  7179  fnprb  7225  fntpb  7226  fconst3  7230  fnfvima  7250  fnunirn  7269  nvof1o  7294  f1eqcocnv  7315  offun  7704  fnexALT  7964  curry1  8118  curry2  8121  fimaproj  8149  suppvalfng  8181  suppvalfn  8182  suppfnss  8203  fnsuppres  8205  frrlem2  8302  frrlem12  8312  wfrlem2OLD  8339  wfrlem14OLD  8352  tfrlem4  8409  tfrlem5  8410  tfrlem11  8418  tz7.48-2  8472  tz7.49  8475  naddcllem  8706  naddov2  8709  naddunif  8723  naddasslem1  8724  naddasslem2  8725  fndmeng  9071  fnfi  9215  fodomfi  9352  fodomfiOLD  9372  resfnfinfin  9379  fczfsuppd  9429  marypha2lem4  9481  inf0  9664  r1elss  9849  dfac8alem  10072  alephfp  10151  dfac3  10164  dfac9  10179  dfac12lem1  10186  dfac12lem2  10187  r1om  10287  cfsmolem  10313  alephsing  10319  zorn2lem1  10539  zorn2lem5  10543  zorn2lem6  10544  zorn2lem7  10545  ttukeylem3  10554  ttukeylem6  10557  fnct  10580  smobeth  10629  fpwwe2lem8  10681  wunr1om  10762  tskr1om  10810  tskr1om2  10811  uzrdg0i  13979  uzrdgsuci  13980  seqexw  14037  hashkf  14349  cshimadifsn  14838  cshimadifsn0  14839  shftfn  15078  phimullem  16781  imasaddvallem  17544  imasvscaval  17553  dfrngc2  20606  dfringc2  20635  rngcresringcat  20647  lidlval  21199  rspval  21200  psgnghm  21576  iscldtop  23090  2ndcomap  23453  qtoptop  23695  basqtop  23706  qtoprest  23712  kqfvima  23725  isr0  23732  kqreglem1  23736  kqnrmlem1  23738  kqnrmlem2  23739  ustbas  24223  uniiccdif  25598  noextendseq  27697  madeval  27876  oldval  27878  addsval  27976  negsval  28035  negsproplem2  28038  negsunif  28064  mulsval  28110  zsex  28330  fcoinver  32524  fnpreimac  32588  mdetpmtr1  33638  sseqf  34226  sseqfv2  34228  elorrvc  34297  bnj1371  34874  bnj1497  34905  fnrelpredd  34926  gblacfnacd  34935  filnetlem4  36093  heibor1lem  37510  diaf11N  40748  dibf11N  40860  dibclN  40861  dihintcl  41043  aks6d1c2lem4  41825  fnsnbt  41954  ismrc  42358  dnnumch1  42705  aomclem4  42718  aomclem6  42720  tfsconcatrev  43014  tfsnfin  43018  fnimafnex  43107  ntrclsfv1  43722  ntrneifv1  43746  finnzfsuppd  43876  fvelima2  44869  climrescn  45369  icccncfext  45508  stoweidlem29  45650  stoweidlem59  45680  ovolval4lem1  46270  fnresfnco  46656  funcoressn  46657  fnfocofob  46692  fnbrafvb  46767  tz6.12-afv  46786  afvco2  46789  tz6.12-afv2  46853  fnbrafv2b  46861  imaelsetpreimafv  46967  imasetpreimafvbijlemfv  46974  imasetpreimafvbijlemfo  46977  plusfreseq  47541  ackvalsuc0val  48075