Theorem fnfun 6621

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5641  Fun wfun 6508   Fn wfn 6509

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 6517

This theorem is referenced by:  fnfund  6622  fnrel  6623  funfni  6627  fncofn  6638  fnco  6639  fnssresb  6643  ffun  6694  f1fun  6761  f1ofun  6805  fnbrfvb  6914  fvelima2  6916  fvelimad  6931  fvelimab  6936  fvun1  6955  elpreima  7033  respreima  7041  rescnvimafod  7048  fnsnr  7140  fnsnbg  7141  fnprb  7185  fntpb  7186  fconst3  7190  fnfvima  7210  ralima  7214  fnunirn  7231  nvof1o  7258  f1eqcocnv  7279  offun  7670  fnexALT  7932  curry1  8086  curry2  8089  fimaproj  8117  suppvalfng  8149  suppvalfn  8150  suppfnss  8171  fnsuppres  8173  frrlem2  8269  frrlem12  8279  tfrlem4  8350  tfrlem5  8351  tfrlem11  8359  tz7.48-2  8413  tz7.49  8416  naddcllem  8643  naddov2  8646  naddunif  8660  naddasslem1  8661  naddasslem2  8662  fndmeng  9009  fnfi  9148  fodomfi  9268  fodomfiOLD  9288  resfnfinfin  9295  finnzfsuppd  9331  fczfsuppd  9344  marypha2lem4  9396  inf0  9581  r1elss  9766  dfac8alem  9989  alephfp  10068  dfac3  10081  dfac9  10097  dfac12lem1  10104  dfac12lem2  10105  r1om  10203  cfsmolem  10230  alephsing  10236  zorn2lem1  10456  zorn2lem5  10460  zorn2lem6  10461  zorn2lem7  10462  ttukeylem3  10471  ttukeylem6  10474  fnct  10497  smobeth  10546  fpwwe2lem8  10598  wunr1om  10679  tskr1om  10727  tskr1om2  10728  uzrdg0i  13931  uzrdgsuci  13932  seqexw  13989  hashkf  14304  cshimadifsn  14802  cshimadifsn0  14803  shftfn  15046  phimullem  16756  imasaddvallem  17499  imasvscaval  17508  dfrngc2  20544  dfringc2  20573  rngcresringcat  20585  lidlval  21127  rspval  21128  psgnghm  21496  iscldtop  22989  2ndcomap  23352  qtoptop  23594  basqtop  23605  qtoprest  23611  kqfvima  23624  isr0  23631  kqreglem1  23635  kqnrmlem1  23637  kqnrmlem2  23638  ustbas  24122  uniiccdif  25486  noextendseq  27586  madeval  27767  oldval  27769  addsval  27876  negsval  27938  negsproplem2  27942  negsunif  27968  mulsval  28019  zsex  28275  fcoinver  32540  fnpreimac  32602  elrgspnlem2  33201  mdetpmtr1  33820  sseqf  34390  sseqfv2  34392  elorrvc  34462  bnj1371  35026  bnj1497  35057  fnrelpredd  35086  gblacfnacd  35096  onvf1odlem3  35099  onvf1odlem4  35100  onvf1od  35101  filnetlem4  36376  heibor1lem  37810  diaf11N  41050  dibf11N  41162  dibclN  41163  dihintcl  41345  aks6d1c2lem4  42122  ismrc  42696  dnnumch1  43040  aomclem4  43053  aomclem6  43055  tfsconcatrev  43344  tfsnfin  43348  fnimafnex  43436  ntrclsfv1  44051  ntrneifv1  44075  climrescn  45753  icccncfext  45892  stoweidlem29  46034  stoweidlem59  46064  ovolval4lem1  46654  fnresfnco  47046  funcoressn  47047  fnfocofob  47084  fnbrafvb  47159  tz6.12-afv  47178  afvco2  47181  tz6.12-afv2  47245  fnbrafv2b  47253  imaelsetpreimafv  47400  imasetpreimafvbijlemfv  47407  imasetpreimafvbijlemfo  47410  plusfreseq  48156  ackvalsuc0val  48680