Theorem fnfun 6661

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5655  Fun wfun 6552   Fn wfn 6553

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 6561

This theorem is used by:  fnfund  6662  fnrel  6663  funfni  6667  fncofn  6678  fnco  6679  fnssresb  6683  ffunOLD  6735  f1funOLD  6803  f1ofun  6848  fnbrfvb  6958  fvelima2  6960  fvelimad  6975  fvelimab  6980  fvun1  6999  elpreimaOLD  7081  respreima  7089  rescnvimafod  7097  fnsnr  7192  fnsnbg  7193  fnprb  7237  fntpb  7238  fconst3  7242  fnfvima  7262  ralima  7266  fnunirn  7280  nvof1o  7311  f1eqcocnv  7332  offun  7731  fnexALT  7987  curry1  8142  curry2  8145  fimaproj  8179  suppvalfng  8212  suppvalfn  8213  suppfnss  8234  fnsuppres  8236  frrlem2  8333  frrlem12  8343  tfrlem4  8414  tfrlem5  8415  tfrlem11  8424  tz7.48-2  8480  tz7.49  8483  naddcllem  8713  naddov2  8716  naddunif  8731  naddasslem1  8732  naddasslem2  8733  fndmeng  9091  fnfi  9221  fodomfi  9332  resfnfinfin  9354  tfsnfin2  9380  finnzfsuppd  9392  fczfsuppd  9405  marypha2lem4  9457  inf0  9649  r1elss  9841  dfac8alem  10135  alephfp  10214  dfac3  10227  dfac9  10242  dfac12lem1  10249  dfac12lem2  10250  cfsmolem  10375  alephsing  10381  zorn2lem1  10601  zorn2lem5  10605  zorn2lem6  10606  zorn2lem7  10607  ttukeylem3  10616  ttukeylem6  10619  fnct  10647  fnctOLD  10648  smobeth  10698  fpwwe2lem8  10750  uzrdg0i  14129  uzrdgsuci  14130  seqexw  14187  hashkf  14503  cshimadifsn  15008  cshimadifsn0  15009  shftfn  15255  phimullem  16985  imasaddvallem  17730  imasvscaval  17739  dfrngc2  20910  dfringc2  20939  rngcresringcat  20951  lidlval  21518  rspval  21519  psgnghm  21916  iscldtop  23443  2ndcomap  23807  qtoptop  24049  basqtop  24060  qtoprest  24066  kqfvima  24079  isr0  24086  kqreglem1  24090  kqnrmlem1  24092  kqnrmlem2  24093  ustbas  24576  uniiccdif  25929  noextendseq  28054  madeval  28248  oldval  28250  addsval  28378  negsval  28441  negsproplem2  28445  negsunif  28471  mulsval  28525  zsex  28796  nowisdomv  31105  fcoinver  33270  fresunsn  33291  fnpreimac  33336  elrgspnlem2  33874  mdetpmtr1  34525  sseqf  35094  sseqfv2  35096  elorrvc  35166  bnj1371  35729  bnj1497  35760  fnrelpredd  35804  acwer1prc  35852  fnlfvk30  36027  fnlfvk3n0  36028  gblacfnacd  36029  onvf1odlem3  36033  onvf1odlem4  36034  onvf1od  36035  nmulprop  37117  filnetlem4  37347  heibor1lem  38935  diaf11N  42298  dibf11N  42410  dibclN  42411  dihintcl  42593  aks6d1c2lem4  43369  ismrc  43905  dnnumch1  44244  aomclem4  44252  aomclem6  44254  tfsconcatrev  44542  tfsnfin  44546  fnimafnex  44633  ntrclsfv1  45247  ntrneifv1  45271  climrescn  46963  icccncfext  47102  stoweidlem29  47244  stoweidlem59  47274  ovolval4lem1  47864  fnresfnco  48316  funcoressn  48317  fnfocofob  48354  fnbrafvb  48429  tz6.12-afv  48448  afvco2  48451  tz6.12-afv2  48515  fnbrafv2b  48523  imaelsetpreimafv  48682  imasetpreimafvbijlemfv  48689  imasetpreimafvbijlemfo  48692  plusfreseq  49466  ackvalsuc0val  50004