Theorem fnfun 6639

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

Syntax hints:   → wi 4   = wceq 1533  dom cdm 5666  Fun wfun 6527   Fn wfn 6528

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 6536

This theorem is referenced by:  fnfund  6640  fnrel  6641  funfni  6645  fncofn  6656  fnco  6657  fncoOLD  6658  fnssresb  6662  ffun  6710  f1fun  6779  f1ofun  6825  fnbrfvb  6934  fvelimad  6949  fvelimab  6954  fvun1  6972  elpreima  7049  respreima  7057  rescnvimafod  7065  fnsnr  7155  fnprb  7201  fntpb  7202  fconst3  7206  fnfvima  7226  fnunirn  7245  nvof1o  7270  f1eqcocnv  7291  f1eqcocnvOLD  7292  offun  7677  fnexALT  7930  curry1  8084  curry2  8087  fimaproj  8115  suppvalfng  8147  suppvalfn  8148  suppfnss  8168  fnsuppres  8170  frrlem2  8267  frrlem12  8277  wfrlem2OLD  8304  wfrlem14OLD  8317  tfrlem4  8374  tfrlem5  8375  tfrlem11  8383  tz7.48-2  8437  tz7.49  8440  naddcllem  8671  naddov2  8674  naddunif  8688  naddasslem1  8689  naddasslem2  8690  fndmeng  9031  fnfi  9177  fodomfi  9321  resfnfinfin  9328  fczfsuppd  9377  marypha2lem4  9429  inf0  9612  r1elss  9797  dfac8alem  10020  alephfp  10099  dfac3  10112  dfac9  10127  dfac12lem1  10134  dfac12lem2  10135  r1om  10235  cfsmolem  10261  alephsing  10267  zorn2lem1  10487  zorn2lem5  10491  zorn2lem6  10492  zorn2lem7  10493  ttukeylem3  10502  ttukeylem6  10505  fnct  10528  smobeth  10577  fpwwe2lem8  10629  wunr1om  10710  tskr1om  10758  tskr1om2  10759  uzrdg0i  13921  uzrdgsuci  13922  seqexw  13979  hashkf  14289  cshimadifsn  14777  cshimadifsn0  14778  shftfn  15017  phimullem  16711  imasaddvallem  17474  imasvscaval  17483  dfrngc2  20514  dfringc2  20543  rngcresringcat  20555  lidlval  21059  rspval  21060  psgnghm  21441  iscldtop  22921  2ndcomap  23284  qtoptop  23526  basqtop  23537  qtoprest  23543  kqfvima  23556  isr0  23563  kqreglem1  23567  kqnrmlem1  23569  kqnrmlem2  23570  ustbas  24054  uniiccdif  25429  noextendseq  27516  madeval  27695  oldval  27697  addsval  27795  negsval  27854  negsproplem2  27857  negsunif  27883  mulsval  27925  fcoinver  32304  fnpreimac  32365  mdetpmtr1  33292  sseqf  33880  sseqfv2  33882  elorrvc  33951  bnj1371  34529  bnj1497  34560  fnrelpredd  34581  filnetlem4  35756  heibor1lem  37167  diaf11N  40410  dibf11N  40522  dibclN  40523  dihintcl  40705  fnsnbt  41544  ismrc  41928  dnnumch1  42275  aomclem4  42288  aomclem6  42290  tfsconcatrev  42587  tfsnfin  42591  fnimafnex  42680  ntrclsfv1  43295  ntrneifv1  43319  finnzfsuppd  43450  fvelima2  44449  climrescn  44949  icccncfext  45088  stoweidlem29  45230  stoweidlem59  45260  ovolval4lem1  45850  fnresfnco  46236  funcoressn  46237  fnfocofob  46272  fnbrafvb  46347  tz6.12-afv  46366  afvco2  46369  tz6.12-afv2  46433  fnbrafv2b  46441  imaelsetpreimafv  46548  imasetpreimafvbijlemfv  46555  imasetpreimafvbijlemfo  46558  plusfreseq  47027  ackvalsuc0val  47561