Theorem fnfun 6668

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5685  Fun wfun 6555   Fn wfn 6556

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 6564

This theorem is referenced by:  fnfund  6669  fnrel  6670  funfni  6674  fncofn  6685  fnco  6686  fnssresb  6690  ffun  6739  f1fun  6806  f1ofun  6850  fnbrfvb  6959  fvelima2  6961  fvelimad  6976  fvelimab  6981  fvun1  7000  elpreima  7078  respreima  7086  rescnvimafod  7093  fnsnr  7185  fnprb  7228  fntpb  7229  fconst3  7233  fnfvima  7253  ralima  7257  fnunirn  7274  nvof1o  7300  f1eqcocnv  7321  offun  7711  fnexALT  7975  curry1  8129  curry2  8132  fimaproj  8160  suppvalfng  8192  suppvalfn  8193  suppfnss  8214  fnsuppres  8216  frrlem2  8312  frrlem12  8322  wfrlem2OLD  8349  wfrlem14OLD  8362  tfrlem4  8419  tfrlem5  8420  tfrlem11  8428  tz7.48-2  8482  tz7.49  8485  naddcllem  8714  naddov2  8717  naddunif  8731  naddasslem1  8732  naddasslem2  8733  fndmeng  9075  fnfi  9218  fodomfi  9350  fodomfiOLD  9370  resfnfinfin  9377  finnzfsuppd  9413  fczfsuppd  9426  marypha2lem4  9478  inf0  9661  r1elss  9846  dfac8alem  10069  alephfp  10148  dfac3  10161  dfac9  10177  dfac12lem1  10184  dfac12lem2  10185  r1om  10283  cfsmolem  10310  alephsing  10316  zorn2lem1  10536  zorn2lem5  10540  zorn2lem6  10541  zorn2lem7  10542  ttukeylem3  10551  ttukeylem6  10554  fnct  10577  smobeth  10626  fpwwe2lem8  10678  wunr1om  10759  tskr1om  10807  tskr1om2  10808  uzrdg0i  14000  uzrdgsuci  14001  seqexw  14058  hashkf  14371  cshimadifsn  14868  cshimadifsn0  14869  shftfn  15112  phimullem  16816  imasaddvallem  17574  imasvscaval  17583  dfrngc2  20628  dfringc2  20657  rngcresringcat  20669  lidlval  21220  rspval  21221  psgnghm  21598  iscldtop  23103  2ndcomap  23466  qtoptop  23708  basqtop  23719  qtoprest  23725  kqfvima  23738  isr0  23745  kqreglem1  23749  kqnrmlem1  23751  kqnrmlem2  23752  ustbas  24236  uniiccdif  25613  noextendseq  27712  madeval  27891  oldval  27893  addsval  27995  negsval  28057  negsproplem2  28061  negsunif  28087  mulsval  28135  zsex  28366  fcoinver  32617  fnpreimac  32681  elrgspnlem2  33247  mdetpmtr1  33822  sseqf  34394  sseqfv2  34396  elorrvc  34466  bnj1371  35043  bnj1497  35074  fnrelpredd  35103  gblacfnacd  35113  filnetlem4  36382  heibor1lem  37816  diaf11N  41051  dibf11N  41163  dibclN  41164  dihintcl  41346  aks6d1c2lem4  42128  fnsnbt  42271  ismrc  42712  dnnumch1  43056  aomclem4  43069  aomclem6  43071  tfsconcatrev  43361  tfsnfin  43365  fnimafnex  43453  ntrclsfv1  44068  ntrneifv1  44092  climrescn  45763  icccncfext  45902  stoweidlem29  46044  stoweidlem59  46074  ovolval4lem1  46664  fnresfnco  47053  funcoressn  47054  fnfocofob  47091  fnbrafvb  47166  tz6.12-afv  47185  afvco2  47188  tz6.12-afv2  47252  fnbrafv2b  47260  imaelsetpreimafv  47382  imasetpreimafvbijlemfv  47389  imasetpreimafvbijlemfo  47392  plusfreseq  48080  ackvalsuc0val  48608