Theorem fnfun 6517

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5580  Fun wfun 6412   Fn wfn 6413

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 396  df-fn 6421

This theorem is referenced by:  fnfund  6518  fnrel  6519  funfni  6523  fncofn  6532  fnco  6533  fncoOLD  6534  fnssresb  6538  ffun  6587  f1fun  6656  f1ofun  6702  fnbrfvb  6804  fvelimad  6818  fvelimab  6823  fvun1  6841  elpreima  6917  respreima  6925  rescnvimafod  6933  fnsnr  7019  fnprb  7066  fntpb  7067  fconst3  7071  fnfvima  7091  fnunirn  7108  nvof1o  7133  f1eqcocnv  7153  f1eqcocnvOLD  7154  offun  7525  fnexALT  7767  curry1  7915  curry2  7918  fimaproj  7947  suppvalfng  7955  suppvalfn  7956  suppfnss  7976  fnsuppres  7978  frrlem2  8074  frrlem12  8084  wfrlem2OLD  8111  wfrlem14OLD  8124  tfrlem4  8181  tfrlem5  8182  tfrlem11  8190  tz7.48-2  8243  tz7.49  8246  fndmeng  8779  fnfi  8925  fodomfi  9022  resfnfinfin  9029  fczfsuppd  9076  marypha2lem4  9127  inf0  9309  r1elss  9495  dfac8alem  9716  alephfp  9795  dfac3  9808  dfac9  9823  dfac12lem1  9830  dfac12lem2  9831  r1om  9931  cfsmolem  9957  alephsing  9963  zorn2lem1  10183  zorn2lem5  10187  zorn2lem6  10188  zorn2lem7  10189  ttukeylem3  10198  ttukeylem6  10201  fnct  10224  smobeth  10273  fpwwe2lem8  10325  wunr1om  10406  tskr1om  10454  tskr1om2  10455  uzrdg0i  13607  uzrdgsuci  13608  seqexw  13665  hashkf  13974  cshimadifsn  14470  cshimadifsn0  14471  shftfn  14712  phimullem  16408  imasaddvallem  17157  imasvscaval  17166  lidlval  20375  rspval  20376  psgnghm  20697  iscldtop  22154  2ndcomap  22517  qtoptop  22759  basqtop  22770  qtoprest  22776  kqfvima  22789  isr0  22796  kqreglem1  22800  kqnrmlem1  22802  kqnrmlem2  22803  elrnust  23284  ustbas  23287  uniiccdif  24647  fcoinver  30847  fnpreimac  30910  mdetpmtr1  31675  sseqf  32259  sseqfv2  32261  elorrvc  32330  bnj1371  32909  bnj1497  32940  fnrelpredd  32961  naddcllem  33758  naddov2  33761  noextendseq  33797  madeval  33963  oldval  33965  negsval  34050  addsval  34053  filnetlem4  34497  heibor1lem  35894  diaf11N  38990  dibf11N  39102  dibclN  39103  dihintcl  39285  fnsnbt  40134  ismrc  40439  dnnumch1  40785  aomclem4  40798  aomclem6  40800  ntrclsfv1  41554  ntrneifv1  41578  finnzfsuppd  41709  fvelima2  42695  climrescn  43179  icccncfext  43318  stoweidlem29  43460  stoweidlem59  43490  ovolval4lem1  44077  fnresfnco  44422  funcoressn  44423  fnfocofob  44458  fnbrafvb  44533  tz6.12-afv  44552  afvco2  44555  tz6.12-afv2  44619  fnbrafv2b  44627  imaelsetpreimafv  44735  imasetpreimafvbijlemfv  44742  imasetpreimafvbijlemfo  44745  plusfreseq  45214  dfrngc2  45418  dfringc2  45464  rngcresringcat  45476  ackvalsuc0val  45921