Theorem fnfun 6643

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5659  Fun wfun 6530   Fn wfn 6531

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 6539

This theorem is referenced by:  fnfund  6644  fnrel  6645  funfni  6649  fncofn  6660  fnco  6661  fnssresb  6665  ffun  6714  f1fun  6781  f1ofun  6825  fnbrfvb  6934  fvelima2  6936  fvelimad  6951  fvelimab  6956  fvun1  6975  elpreima  7053  respreima  7061  rescnvimafod  7068  fnsnr  7160  fnsnbg  7161  fnprb  7205  fntpb  7206  fconst3  7210  fnfvima  7230  ralima  7234  fnunirn  7251  nvof1o  7278  f1eqcocnv  7299  offun  7690  fnexALT  7954  curry1  8108  curry2  8111  fimaproj  8139  suppvalfng  8171  suppvalfn  8172  suppfnss  8193  fnsuppres  8195  frrlem2  8291  frrlem12  8301  wfrlem2OLD  8328  wfrlem14OLD  8341  tfrlem4  8398  tfrlem5  8399  tfrlem11  8407  tz7.48-2  8461  tz7.49  8464  naddcllem  8693  naddov2  8696  naddunif  8710  naddasslem1  8711  naddasslem2  8712  fndmeng  9054  fnfi  9197  fodomfi  9327  fodomfiOLD  9347  resfnfinfin  9354  finnzfsuppd  9390  fczfsuppd  9403  marypha2lem4  9455  inf0  9640  r1elss  9825  dfac8alem  10048  alephfp  10127  dfac3  10140  dfac9  10156  dfac12lem1  10163  dfac12lem2  10164  r1om  10262  cfsmolem  10289  alephsing  10295  zorn2lem1  10515  zorn2lem5  10519  zorn2lem6  10520  zorn2lem7  10521  ttukeylem3  10530  ttukeylem6  10533  fnct  10556  smobeth  10605  fpwwe2lem8  10657  wunr1om  10738  tskr1om  10786  tskr1om2  10787  uzrdg0i  13982  uzrdgsuci  13983  seqexw  14040  hashkf  14355  cshimadifsn  14853  cshimadifsn0  14854  shftfn  15097  phimullem  16803  imasaddvallem  17548  imasvscaval  17557  dfrngc2  20593  dfringc2  20622  rngcresringcat  20634  lidlval  21176  rspval  21177  psgnghm  21545  iscldtop  23038  2ndcomap  23401  qtoptop  23643  basqtop  23654  qtoprest  23660  kqfvima  23673  isr0  23680  kqreglem1  23684  kqnrmlem1  23686  kqnrmlem2  23687  ustbas  24171  uniiccdif  25536  noextendseq  27636  madeval  27817  oldval  27819  addsval  27926  negsval  27988  negsproplem2  27992  negsunif  28018  mulsval  28069  zsex  28325  fcoinver  32590  fnpreimac  32654  elrgspnlem2  33243  mdetpmtr1  33859  sseqf  34429  sseqfv2  34431  elorrvc  34501  bnj1371  35065  bnj1497  35096  fnrelpredd  35125  gblacfnacd  35135  filnetlem4  36404  heibor1lem  37838  diaf11N  41073  dibf11N  41185  dibclN  41186  dihintcl  41368  aks6d1c2lem4  42145  ismrc  42691  dnnumch1  43035  aomclem4  43048  aomclem6  43050  tfsconcatrev  43339  tfsnfin  43343  fnimafnex  43431  ntrclsfv1  44046  ntrneifv1  44070  climrescn  45744  icccncfext  45883  stoweidlem29  46025  stoweidlem59  46055  ovolval4lem1  46645  fnresfnco  47037  funcoressn  47038  fnfocofob  47075  fnbrafvb  47150  tz6.12-afv  47169  afvco2  47172  tz6.12-afv2  47236  fnbrafv2b  47244  imaelsetpreimafv  47376  imasetpreimafvbijlemfv  47383  imasetpreimafvbijlemfo  47386  plusfreseq  48106  ackvalsuc0val  48634