Theorem fnfun 6625

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

Syntax hints:   → wi 4   = wceq 1563  dom cdm 5652  Fun wfun 6519   Fn wfn 6520

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 210  df-an 401  df-fn 6528

This theorem is referenced by:  fnfund  6626  fnrel  6627  funfni  6631  fncofn  6642  fnco  6643  fnssresb  6647  ffunOLD  6699  f1funOLD  6767  f1ofun  6812  fnbrfvb  6921  fvelima2  6923  fvelimad  6938  fvelimab  6943  fvun1  6962  elpreima  7043  respreima  7051  rescnvimafod  7058  fnsnr  7151  fnsnbg  7152  fnprb  7196  fntpb  7197  fconst3  7201  fnfvima  7221  ralima  7225  fnunirn  7241  nvof1o  7268  f1eqcocnv  7289  offun  7678  fnexALT  7936  curry1  8087  curry2  8090  fimaproj  8119  suppvalfng  8151  suppvalfn  8152  suppfnss  8173  fnsuppres  8175  frrlem2  8272  frrlem12  8282  tfrlem4  8353  tfrlem5  8354  tfrlem11  8363  tz7.48-2  8417  tz7.49  8420  naddcllem  8650  naddov2  8653  naddunif  8668  naddasslem1  8669  naddasslem2  8670  fndmeng  9020  fnfi  9150  fodomfi  9260  resfnfinfin  9282  tfsnfin2  9308  finnzfsuppd  9321  fczfsuppd  9334  marypha2lem4  9386  inf0  9578  r1elss  9766  dfac8alem  10001  alephfp  10080  dfac3  10093  dfac9  10108  dfac12lem1  10115  dfac12lem2  10116  r1om  10214  cfsmolem  10242  alephsing  10248  zorn2lem1  10468  zorn2lem5  10472  zorn2lem6  10473  zorn2lem7  10474  ttukeylem3  10483  ttukeylem6  10486  fnct  10509  smobeth  10559  fpwwe2lem8  10611  wunr1om  10692  tskr1om  10740  tskr1om2  10741  uzrdg0i  13986  uzrdgsuci  13987  seqexw  14044  hashkf  14359  cshimadifsn  14856  cshimadifsn0  14857  shftfn  15100  phimullem  16828  imasaddvallem  17573  imasvscaval  17582  dfrngc2  20704  dfringc2  20733  rngcresringcat  20745  lidlval  21303  rspval  21304  psgnghm  21690  iscldtop  23213  2ndcomap  23576  qtoptop  23818  basqtop  23829  qtoprest  23835  kqfvima  23848  isr0  23855  kqreglem1  23859  kqnrmlem1  23861  kqnrmlem2  23862  ustbas  24345  uniiccdif  25698  noextendseq  27789  madeval  27983  oldval  27985  addsval  28113  negsval  28176  negsproplem2  28180  negsunif  28206  mulsval  28260  zsex  28531  nowisdomv  30734  fcoinver  32859  fresunsn  32882  fnpreimac  32927  elrgspnlem2  33476  mdetpmtr1  34130  sseqf  34699  sseqfv2  34701  elorrvc  34771  bnj1371  35334  bnj1497  35365  fnrelpredd  35397  gblacfnacd  35457  onvf1odlem3  35460  onvf1odlem4  35461  onvf1od  35462  nmulprop  36553  filnetlem4  36754  heibor1lem  38320  diaf11N  41685  dibf11N  41797  dibclN  41798  dihintcl  41980  aks6d1c2lem4  42756  ismrc  43294  dnnumch1  43633  aomclem4  43646  aomclem6  43648  tfsconcatrev  43937  tfsnfin  43941  fnimafnex  44028  ntrclsfv1  44643  ntrneifv1  44667  climrescn  46320  icccncfext  46459  stoweidlem29  46601  stoweidlem59  46631  ovolval4lem1  47221  fnresfnco  47633  funcoressn  47634  fnfocofob  47671  fnbrafvb  47746  tz6.12-afv  47765  afvco2  47768  tz6.12-afv2  47832  fnbrafv2b  47840  imaelsetpreimafv  47999  imasetpreimafvbijlemfv  48006  imasetpreimafvbijlemfo  48009  plusfreseq  48784  ackvalsuc0val  49318