Theorem fnfun 6637

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

Syntax hints:   → wi 4   = wceq 1570  dom cdm 5663  Fun wfun 6532   Fn wfn 6533

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 6541

This theorem is referenced by:  fnfund  6638  fnrel  6639  funfni  6643  fncofn  6654  fnco  6655  fnssresb  6659  ffunOLD  6711  f1funOLD  6779  f1ofun  6824  fnbrfvb  6933  fvelima2  6935  fvelimad  6950  fvelimab  6955  fvun1  6974  elpreima  7055  respreima  7063  rescnvimafod  7070  fnsnr  7163  fnsnbg  7164  fnprb  7208  fntpb  7209  fconst3  7213  fnfvima  7233  ralima  7237  fnunirn  7253  nvof1o  7280  f1eqcocnv  7301  offun  7690  fnexALT  7949  curry1  8100  curry2  8103  fimaproj  8132  suppvalfng  8164  suppvalfn  8165  suppfnss  8186  fnsuppres  8188  frrlem2  8285  frrlem12  8295  tfrlem4  8366  tfrlem5  8367  tfrlem11  8376  tz7.48-2  8430  tz7.49  8433  naddcllem  8663  naddov2  8666  naddunif  8681  naddasslem1  8682  naddasslem2  8683  fndmeng  9033  fnfi  9163  fodomfi  9273  resfnfinfin  9295  tfsnfin2  9321  finnzfsuppd  9334  fczfsuppd  9347  marypha2lem4  9399  inf0  9591  r1elss  9779  dfac8alem  10014  alephfp  10093  dfac3  10106  dfac9  10121  dfac12lem1  10128  dfac12lem2  10129  r1om  10227  cfsmolem  10255  alephsing  10261  zorn2lem1  10481  zorn2lem5  10485  zorn2lem6  10486  zorn2lem7  10487  ttukeylem3  10496  ttukeylem6  10499  fnct  10522  smobeth  10572  fpwwe2lem8  10624  wunr1om  10705  tskr1om  10753  tskr1om2  10754  uzrdg0i  13997  uzrdgsuci  13998  seqexw  14055  hashkf  14370  cshimadifsn  14868  cshimadifsn0  14869  shftfn  15112  phimullem  16839  imasaddvallem  17584  imasvscaval  17593  dfrngc2  20714  dfringc2  20743  rngcresringcat  20755  lidlval  21315  rspval  21316  psgnghm  21711  iscldtop  23233  2ndcomap  23596  qtoptop  23838  basqtop  23849  qtoprest  23855  kqfvima  23868  isr0  23875  kqreglem1  23879  kqnrmlem1  23881  kqnrmlem2  23882  ustbas  24365  uniiccdif  25718  noextendseq  27809  madeval  28003  oldval  28005  addsval  28133  negsval  28196  negsproplem2  28200  negsunif  28226  mulsval  28280  zsex  28551  nowisdomv  30803  fcoinver  32927  fresunsn  32948  fnpreimac  32993  elrgspnlem2  33541  mdetpmtr1  34191  sseqf  34760  sseqfv2  34762  elorrvc  34832  bnj1371  35395  bnj1497  35426  fnrelpredd  35460  gblacfnacd  35564  onvf1odlem3  35567  onvf1odlem4  35568  onvf1od  35569  nmulprop  36660  filnetlem4  36870  heibor1lem  38438  diaf11N  41801  dibf11N  41913  dibclN  41914  dihintcl  42096  aks6d1c2lem4  42872  ismrc  43412  dnnumch1  43751  aomclem4  43764  aomclem6  43766  tfsconcatrev  44055  tfsnfin  44059  fnimafnex  44146  ntrclsfv1  44761  ntrneifv1  44785  climrescn  46442  icccncfext  46581  stoweidlem29  46723  stoweidlem59  46753  ovolval4lem1  47343  fnresfnco  47755  funcoressn  47756  fnfocofob  47793  fnbrafvb  47868  tz6.12-afv  47887  afvco2  47890  tz6.12-afv2  47954  fnbrafv2b  47962  imaelsetpreimafv  48121  imasetpreimafvbijlemfv  48128  imasetpreimafvbijlemfo  48131  plusfreseq  48906  ackvalsuc0val  49444