Theorem fnfun 6642

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5666  Fun wfun 6537   Fn wfn 6538

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 6546

This theorem is used by:  fnfund  6643  fnrel  6644  funfni  6648  fncofn  6659  fnco  6660  fnssresb  6664  ffunOLD  6716  f1funOLD  6784  f1ofun  6829  fnbrfvb  6938  fvelima2  6940  fvelimad  6955  fvelimab  6960  fvun1  6979  elpreima  7060  respreima  7068  rescnvimafod  7075  fnsnr  7168  fnsnbg  7169  fnprb  7213  fntpb  7214  fconst3  7218  fnfvima  7238  ralima  7242  fnunirn  7258  nvof1o  7289  f1eqcocnv  7310  offun  7701  fnexALT  7957  curry1  8108  curry2  8111  fimaproj  8140  suppvalfng  8172  suppvalfn  8173  suppfnss  8194  fnsuppres  8196  frrlem2  8293  frrlem12  8303  tfrlem4  8374  tfrlem5  8375  tfrlem11  8384  tz7.48-2  8438  tz7.49  8441  naddcllem  8671  naddov2  8674  naddunif  8689  naddasslem1  8690  naddasslem2  8691  fndmeng  9042  fnfi  9172  fodomfi  9282  resfnfinfin  9304  tfsnfin2  9330  finnzfsuppd  9343  fczfsuppd  9356  marypha2lem4  9408  inf0  9600  r1elss  9788  dfac8alem  10032  alephfp  10111  dfac3  10124  dfac9  10139  dfac12lem1  10146  dfac12lem2  10147  r1om  10245  cfsmolem  10272  alephsing  10278  zorn2lem1  10498  zorn2lem5  10502  zorn2lem6  10503  zorn2lem7  10504  ttukeylem3  10513  ttukeylem6  10516  fnct  10539  smobeth  10589  fpwwe2lem8  10641  wunr1om  10722  tskr1om  10770  tskr1om2  10771  uzrdg0i  14015  uzrdgsuci  14016  seqexw  14073  hashkf  14388  cshimadifsn  14892  cshimadifsn0  14893  shftfn  15136  phimullem  16863  imasaddvallem  17608  imasvscaval  17617  dfrngc2  20764  dfringc2  20793  rngcresringcat  20805  lidlval  21371  rspval  21372  psgnghm  21767  iscldtop  23289  2ndcomap  23652  qtoptop  23894  basqtop  23905  qtoprest  23911  kqfvima  23924  isr0  23931  kqreglem1  23935  kqnrmlem1  23937  kqnrmlem2  23938  ustbas  24421  uniiccdif  25774  noextendseq  27868  madeval  28062  oldval  28064  addsval  28192  negsval  28255  negsproplem2  28259  negsunif  28285  mulsval  28339  zsex  28610  nowisdomv  30862  fcoinver  32986  fresunsn  33007  fnpreimac  33052  elrgspnlem2  33594  mdetpmtr1  34244  sseqf  34814  sseqfv2  34816  elorrvc  34886  bnj1371  35449  bnj1497  35480  fnrelpredd  35507  gblacfnacd  35610  onvf1odlem3  35613  onvf1odlem4  35614  onvf1od  35615  nmulprop  36703  filnetlem4  36933  heibor1lem  38501  diaf11N  41864  dibf11N  41976  dibclN  41977  dihintcl  42159  aks6d1c2lem4  42935  ismrc  43473  dnnumch1  43812  aomclem4  43825  aomclem6  43827  tfsconcatrev  44116  tfsnfin  44120  fnimafnex  44207  ntrclsfv1  44822  ntrneifv1  44846  climrescn  46503  icccncfext  46642  stoweidlem29  46784  stoweidlem59  46814  ovolval4lem1  47404  fnresfnco  47819  funcoressn  47820  fnfocofob  47857  fnbrafvb  47932  tz6.12-afv  47951  afvco2  47954  tz6.12-afv2  48018  fnbrafv2b  48026  imaelsetpreimafv  48185  imasetpreimafvbijlemfv  48192  imasetpreimafvbijlemfo  48195  plusfreseq  48970  ackvalsuc0val  49508