Theorem fnfun 6636

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5659  Fun wfun 6531   Fn wfn 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6540

This theorem is used by:  fnfund  6637  fnrel  6638  funfni  6642  fncofn  6653  fnco  6654  fnssresb  6658  ffunOLD  6710  f1funOLD  6778  f1ofun  6823  fnbrfvb  6932  fvelima2  6934  fvelimad  6949  fvelimab  6954  fvun1  6973  elpreima  7054  respreima  7062  rescnvimafod  7069  fnsnr  7164  fnsnbg  7165  fnprb  7210  fntpb  7211  fconst3  7215  fnfvima  7235  ralima  7239  fnunirn  7253  nvof1o  7284  f1eqcocnv  7305  offun  7695  fnexALT  7951  curry1  8104  curry2  8107  fimaproj  8136  suppvalfng  8168  suppvalfn  8169  suppfnss  8190  fnsuppres  8192  frrlem2  8289  frrlem12  8299  tfrlem4  8370  tfrlem5  8371  tfrlem11  8380  tz7.48-2  8434  tz7.49  8437  naddcllem  8667  naddov2  8670  naddunif  8685  naddasslem1  8686  naddasslem2  8687  fndmeng  9045  fnfi  9175  fodomfi  9285  resfnfinfin  9307  tfsnfin2  9333  finnzfsuppd  9346  fczfsuppd  9359  marypha2lem4  9411  inf0  9603  r1elss  9791  dfac8alem  10035  alephfp  10114  dfac3  10127  dfac9  10142  dfac12lem1  10149  dfac12lem2  10150  r1om  10248  cfsmolem  10275  alephsing  10281  zorn2lem1  10501  zorn2lem5  10505  zorn2lem6  10506  zorn2lem7  10507  ttukeylem3  10516  ttukeylem6  10519  fnct  10547  fnctOLD  10548  smobeth  10598  fpwwe2lem8  10650  wunr1om  10731  tskr1om  10779  tskr1om2  10780  uzrdg0i  14025  uzrdgsuci  14026  seqexw  14083  hashkf  14398  cshimadifsn  14902  cshimadifsn0  14903  shftfn  15148  phimullem  16874  imasaddvallem  17619  imasvscaval  17628  dfrngc2  20794  dfringc2  20823  rngcresringcat  20835  lidlval  21401  rspval  21402  psgnghm  21797  iscldtop  23324  2ndcomap  23688  qtoptop  23930  basqtop  23941  qtoprest  23947  kqfvima  23960  isr0  23967  kqreglem1  23971  kqnrmlem1  23973  kqnrmlem2  23974  ustbas  24457  uniiccdif  25810  noextendseq  27904  madeval  28098  oldval  28100  addsval  28228  negsval  28291  negsproplem2  28295  negsunif  28321  mulsval  28375  zsex  28646  nowisdomv  30955  fcoinver  33079  fresunsn  33100  fnpreimac  33145  elrgspnlem2  33685  mdetpmtr1  34335  sseqf  34905  sseqfv2  34907  elorrvc  34977  bnj1371  35540  bnj1497  35571  fnrelpredd  35598  gblacfnacd  35701  onvf1odlem3  35704  onvf1odlem4  35705  onvf1od  35706  nmulprop  36772  filnetlem4  37002  heibor1lem  38561  diaf11N  41924  dibf11N  42036  dibclN  42037  dihintcl  42219  aks6d1c2lem4  42995  ismrc  43548  dnnumch1  43887  aomclem4  43900  aomclem6  43902  tfsconcatrev  44191  tfsnfin  44195  fnimafnex  44282  ntrclsfv1  44897  ntrneifv1  44921  climrescn  46578  icccncfext  46717  stoweidlem29  46859  stoweidlem59  46889  ovolval4lem1  47479  fnresfnco  47931  funcoressn  47932  fnfocofob  47969  fnbrafvb  48044  tz6.12-afv  48063  afvco2  48066  tz6.12-afv2  48130  fnbrafv2b  48138  imaelsetpreimafv  48297  imasetpreimafvbijlemfv  48304  imasetpreimafvbijlemfo  48307  plusfreseq  49081  ackvalsuc0val  49619