Theorem fvmpt 7029

Description: Value of a function given in maps-to notation. (Contributed by NM, 17-Aug-2011.)

Hypotheses

Ref	Expression
fvmptg.1	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
fvmptg.2	⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
fvmpt.3	⊢ 𝐶 ∈ V

Assertion

Ref	Expression
fvmpt	⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem fvmpt

Step	Hyp	Ref	Expression
1		fvmpt.3	. 2 ⊢ 𝐶 ∈ V
2		fvmptg.1	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
3		fvmptg.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
4	2, 3	fvmptg 7027	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V) → (𝐹‘𝐴) = 𝐶)
5	1, 4	mpan2 690	1 ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  Vcvv 3488   ↦ cmpt 5249  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581

This theorem is referenced by:  fvmptex  7043  fvmptrabfv  7061  mptfvmpt  7265  fvmptopab  7504  ofval  7725  caofinvl  7745  fvresex  8000  1stval  8032  2ndval  8033  reldm  8085  curry1val  8146  curry2val  8150  fsplitfpar  8159  fnwelem  8172  brtpos2  8273  onovuni  8398  tz7.44-1  8462  oasuc  8580  oesuclem  8581  omsuc  8582  onasuc  8584  onmsuc  8585  fsetfocdm  8919  fvmptmap  8939  xpcomco  9128  unxpdomlem1  9313  unfilem2  9372  ordtypelem3  9589  ixpiunwdom  9659  inf3lema  9693  noinfep  9729  cantnfval  9737  cantnflem1d  9757  cantnflem1  9758  ssttrcl  9784  ttrcltr  9785  ttrclselem2  9795  r1sucg  9838  r0weon  10081  infxpenc2lem1  10088  fseqenlem1  10093  fseqenlem2  10094  dfac8alem  10098  ac5num  10105  acni2  10115  dfac4  10191  dfac2a  10199  dfacacn  10211  dfac12lem1  10213  ackbij1lem7  10294  ackbij2lem2  10308  ackbij2lem3  10309  cfsmolem  10339  fin23lem28  10409  fin23lem39  10419  isf32lem6  10427  isf32lem7  10428  isf32lem8  10429  fin1a2lem3  10471  itunifval  10485  itunisuc  10488  axdc2lem  10517  axdc3lem2  10520  axcclem  10526  zorn2lem1  10565  negiso  12275  infrenegsup  12278  uzval  12905  flval  13845  ceilval  13889  ceilval2  13891  monoord2  14084  seqf1olem2  14093  seqf1o  14094  seqdistr  14104  serle  14108  seqof  14110  swrdfv  14696  revval  14808  revfv  14811  wwlktovf1  15006  wwlktovfo  15007  sgnval  15137  cjval  15151  reval  15155  imval  15156  sqrtval  15286  absval  15287  limsupval  15520  limsupgval  15522  climmpt  15617  climle  15686  rlimdiv  15694  isercolllem1  15713  isercoll2  15717  caurcvg2  15726  fsumser  15778  isumadd  15815  fsumcnv  15821  fsumrev  15827  fsumshft  15828  iserabs  15863  cvgcmp  15864  cvgcmpce  15866  incexclem  15884  isumless  15893  divcnvshft  15903  supcvg  15904  harmonic  15907  trireciplem  15910  trirecip  15911  expcnv  15912  explecnv  15913  geolim  15918  geolim2  15919  geo2lim  15923  geomulcvg  15924  geoisum  15925  geoisumr  15926  geoisum1  15927  geoisum1c  15928  cvgrat  15931  mertenslem2  15933  mertens  15934  prodfdiv  15944  fprodser  15997  fprodshft  16024  fprodrev  16025  fprodcnv  16031  iprodmul  16051  bpolylem  16096  eftval  16124  efval  16127  efcvgfsum  16134  ege2le3  16138  eftlub  16157  eflegeo  16169  sinval  16170  cosval  16171  tanval  16176  eirrlem  16252  rpnnen2lem1  16262  rpnnen2lem2  16263  bitsfval  16469  bitsinv2  16489  bitsinv  16494  sadcf  16499  sadc0  16500  sadcp1  16501  smupf  16524  smup0  16525  smupp1  16526  qnumval  16784  qdenval  16785  phival  16814  crth  16825  phimullem  16826  eulerthlem2  16829  phisum  16837  odzval  16838  iserodd  16882  pcmpt  16939  prmreclem1  16963  prmreclem2  16964  prmreclem4  16966  prmreclem5  16967  prmreclem6  16968  1arithlem1  16970  1arithlem2  16971  vdwapfval  17018  vdwlem2  17029  vdwlem6  17033  vdwlem8  17035  vdwlem9  17036  ramub1lem2  17074  ramcl  17076  prmoval  17080  strfvnd  17232  topnval  17494  prdsplusgfval  17534  prdsmulrfval  17536  isacs  17709  acsfn  17717  homffval  17748  comfffval  17756  oppcval  17771  monfval  17793  oppcmon  17799  sectffval  17811  invffval  17819  isoval  17826  idfuval  17940  homafval  18096  arwval  18110  coafval  18131  yonedainv  18351  oduval  18358  pltfval  18401  lubfval  18420  lubval  18426  glbfval  18433  glbval  18439  p0val  18497  p1val  18498  ipoval  18600  plusffval  18684  grpidval  18699  issubmgm  18740  issubm  18838  prdspjmhm  18864  efmnd  18905  smndex1igid  18939  grpinvfval  19018  grpinvval  19020  grpsubfval  19023  grpsubfvalALT  19024  grplactval  19082  prdsinvlem  19089  mulgfval  19109  mulgfvalALT  19110  pwsmulg  19159  issubg  19166  isnsg  19195  cycsubmel  19240  cycsubgcl  19246  conjghm  19289  conjnmz  19292  cntrval  19359  cntzfval  19360  cntzval  19361  oppgval  19387  psgnfval  19542  psgnval  19549  odfval  19574  odval  19576  sylow1lem4  19643  pgpssslw  19656  sylow2blem3  19664  sylow3lem2  19670  lsmfval  19680  pj1fval  19736  efgval  19759  efgsval  19773  frgpval  19800  vrgpval  19809  mulgmhm  19869  mulgghm  19870  ablfaclem1  20129  mgpval  20164  srglmhm  20248  srgrmhm  20249  ringlghm  20335  ringrghm  20336  pwspjmhmmgpd  20351  pwsexpg  20352  opprval  20361  dvdsrval  20387  isunit  20399  invrfval  20415  dvrfval  20428  isirred  20445  issubrng  20573  issubrg  20599  rrgval  20719  fidomndrnglem  20795  issdrg  20811  abvfval  20833  abvtrivd  20855  staffval  20864  stafval  20865  scaffval  20900  lmodvsghm  20943  lssset  20954  lspfval  20994  islbs  21098  sraval  21197  rlmval  21221  2idlval  21284  lpival  21357  expmhm  21477  expghm  21509  mulgghm2  21510  mulgrhm  21511  zrhval  21541  zrhmulg  21543  zlmval  21549  chrval  21561  znval  21573  znzrhval  21588  evpmss  21627  psgnevpmb  21628  ip0l  21677  ipffval  21689  ocvfval  21707  ocvval  21708  cssval  21723  thlval  21736  pjfval  21749  pjval  21753  isobs  21763  prdsinvgd2  21785  uvcresum  21836  frlmup1  21841  frlmup2  21842  islinds  21852  islindf5  21882  aspval  21916  asclval  21923  psrmulval  21987  psrlidm  22005  psrridm  22006  psrascl  22022  mvrval  22025  mvrval2  22026  mplmonmul  22077  evlslem3  22127  evlslem1  22129  evlsval  22133  evlssca  22136  evlsvar  22137  psdmul  22193  psr1val  22208  vr1val  22214  ply1val  22216  coe1fval  22228  coe1fv  22229  coe1tmmul2  22300  coe1tmmul  22301  coe1tmmul2fv  22302  coe1pwmulfv  22304  evls1val  22345  evl1fval  22353  evl1val  22354  mamulid  22468  mamurid  22469  mdetleib  22614  mdetleib1  22618  mdetunilem9  22647  mdetuni0  22648  mdetmul  22650  cpmidpmatlem1  22897  ordtval  23218  cnpval  23265  ptpjpre1  23600  ptpjopn  23641  dfac14  23647  upxp  23652  uptx  23654  hauseqlcld  23675  txlm  23677  xkoptsub  23683  xkoinjcn  23716  kqval  23755  xpstopnlem1  23838  fmval  23972  flfval  24019  ptcmplem2  24082  ptcmplem3  24083  symgtgp  24135  qustgpopn  24149  ussval  24289  iscfilu  24318  ispsmet  24335  ismet  24354  isxmet  24355  mopnval  24469  prdsxmslem2  24563  nmfval  24622  nmval  24623  nmoval  24757  metdsval  24888  divcnOLD  24909  divcn  24911  mulc1cncf  24950  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  cnheiborlem  25005  evth  25010  evth2  25011  lebnumlem3  25014  isphtpy  25032  isphtpc  25045  pcofval  25062  pcovalg  25064  pco1  25067  pcopt  25074  pcopt2  25075  pcoass  25076  pcorevcl  25077  pcorevlem  25078  pcorev2  25080  pi1xfrcnv  25109  cphnm  25246  tcphval  25271  tcphnmval  25282  cfilfval  25317  iscmet  25337  iscmet3lem3  25343  rrxval  25440  ehlval  25467  ivth2  25509  ovolval  25527  ovollb2lem  25542  ovolunlem1a  25550  ovolunlem1  25551  ovoliunlem1  25556  ovoliunlem2  25557  ovolicc1  25570  voliunlem1  25604  voliunlem2  25605  voliunlem3  25606  volsup  25610  ioorval  25628  uniioombllem3  25639  uniioombllem6  25642  volsup2  25659  volcn  25660  volivth  25661  vitalilem2  25663  vitalilem3  25664  vitalilem4  25665  vitali  25667  mbfmax  25703  mbfimaopnlem  25709  itg1val  25737  i1f1lem  25743  itg11  25745  itg1addlem4  25753  itg1addlem4OLD  25754  itg1mulc  25759  i1fres  25760  itg1climres  25769  mbfi1fseqlem2  25771  mbfi1fseqlem3  25772  mbfi1fseqlem6  25775  mbfi1flimlem  25777  mbfi1flim  25778  mbfmullem2  25779  itg2seq  25797  itg2uba  25798  itg2splitlem  25803  itg2monolem1  25805  itg2monolem2  25806  itg2monolem3  25807  itg2mono  25808  itg2i1fseqle  25809  itg2i1fseq  25810  itg2i1fseq2  25811  itg2addlem  25813  itg2cnlem1  25816  itg2cn  25818  limccnp2  25947  dvnff  25979  dvnp1  25981  cpnfval  25988  elcpn  25990  dvrec  26013  dvcnvlem  26034  dveflem  26037  dvef  26038  dvferm1  26043  dvferm2  26045  rolle  26048  dvlip  26052  dvlipcn  26053  dv11cn  26060  dvivthlem1  26067  dvivth  26069  lhop1lem  26072  ftc1lem1  26096  ftc1lem5  26101  ftc2  26105  itgsubstlem  26109  tdeglem3  26118  tdeglem4  26119  mdegval  26122  mdegmullem  26137  deg1fval  26139  deg1ldg  26151  deg1leb  26154  coe1mul3  26158  uc1pval  26199  mon1pval  26201  mon1pid  26213  q1pval  26214  r1pval  26217  ply1remlem  26224  ig1pval  26235  plyval  26252  elply2  26255  plyeq0lem  26269  coeval  26282  dgrval  26287  coeid2  26298  coemullem  26309  coemul  26311  elqaalem1  26379  elqaalem2  26380  elqaalem3  26381  iaa  26385  aareccl  26386  aannenlem1  26388  geolim3  26399  aaliou3lem1  26402  aaliou3lem2  26403  aaliou3lem5  26407  aaliou3lem6  26408  aaliou3lem7  26409  aaliou3  26411  tayl0  26421  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmshftlem  26450  ulmshft  26451  ulmuni  26453  ulmcau  26456  ulmdvlem1  26461  ulmdvlem3  26463  mtest  26465  mtestbdd  26466  mbfulm  26467  iblulm  26468  itgulm  26469  pserval  26471  pserval2  26472  radcnvlem1  26474  radcnvlem2  26475  dvradcnv  26482  pserulm  26483  pserdvlem2  26490  pserdv  26491  abelthlem1  26493  abelthlem3  26495  abelthlem4  26496  abelthlem5  26497  abelthlem6  26498  abelthlem7  26500  abelthlem8  26501  abelthlem9  26502  resinf1o  26596  efif1olem4  26605  eff1olem  26608  logcnlem5  26706  logtayllem  26719  logtayl  26720  logtaylsum  26721  logtayl2  26722  logccv  26723  asinval  26943  acosval  26944  atanval  26945  atantayl  26998  leibpilem2  27002  leibpi  27003  leibpisum  27004  log2cnv  27005  log2tlbnd  27006  areaval  27025  efrlim  27030  efrlimOLD  27031  dfef2  27032  amgmlem  27051  emcllem2  27058  emcllem3  27059  emcllem4  27060  emcllem5  27061  emcllem6  27062  emcllem7  27063  zetacvg  27076  lgamgulmlem4  27093  lgamgulmlem5  27094  lgamgulm2  27097  lgamcvglem  27101  igamval  27108  lgamcvg2  27116  gamcvg2lem  27120  ftalem7  27140  basellem2  27143  basellem3  27144  basellem4  27145  basellem5  27146  basellem6  27147  basellem8  27149  basellem9  27150  chtval  27171  vmaval  27174  chpval  27183  ppival  27188  muval  27193  prmorcht  27239  sqff1o  27243  dvdsflsumcom  27249  musum  27252  muinv  27254  sgmppw  27259  fsumvma  27275  pclogsum  27277  dchrfi  27317  bposlem5  27350  bposlem7  27352  bposlem8  27353  bposlem9  27354  lgsfval  27364  lgsdir  27394  lgsdilem2  27395  lgsdi  27396  lgsne0  27397  lgsqrlem2  27409  lgsqrlem4  27411  lgseisenlem2  27438  dchrmusum2  27556  dchrvmasumlem1  27557  dchrvmasumiflem1  27563  dchrvmaeq0  27566  dchrisum0fval  27567  dchrisum0re  27575  mulog2sumlem1  27596  pntrval  27624  pntsval  27634  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntlem3  27671  abvcxp  27677  padicfval  27678  padicval  27679  padicabv  27692  ostth1  27695  ostth2  27699  ostth3  27700  nosupfv  27769  noinffv  27784  newval  27912  leftval  27920  rightval  27921  iscgrg  28538  legval  28610  ishpg  28785  iscgra  28835  isinag  28864  isleag  28873  iseqlg  28893  ttgval  28901  ttgvalOLD  28902  elee  28927  axsegconlem1  28950  axsegconlem9  28958  axsegconlem10  28959  axpasch  28974  axlowdimlem15  28989  axlowdim  28994  axeuclidlem  28995  axcontlem2  28998  eengv  29012  vtxval  29035  iedgval  29036  edgval  29084  vtxdgval  29504  wwlksnextinj  29932  wwlksnextsurj  29933  clwwlkfv  30080  clwwlknonmpo  30121  fusgreg2wsplem  30365  fusgreghash2wsp  30370  numclwwlk1lem2fv  30388  gidval  30544  grpoinvval  30555  bafval  30636  imsval  30717  dipfval  30734  sspval  30755  nmooval  30795  hmoval  30842  ipasslem8  30869  ipasslem9  30870  ipblnfi  30887  ubthlem2  30903  htthlem  30949  normval  31156  ocval  31312  occllem  31335  hsupval  31366  pjhfval  31428  pjhval  31429  chscllem2  31670  chscllem3  31671  hosval  31772  homval  31773  hodval  31774  hfsval  31775  hfmval  31776  brafval  31975  braval  31976  kbval  31986  eigvalval  31992  cnlnadjlem1  32099  nmopadjlei  32120  hmopidmchi  32183  strlem2  32283  hstrlem2  32291  cdj3lem2  32467  ofpreima  32683  psgnfzto1stlem  33093  evpmval  33138  altgnsg  33142  inftmrel  33160  isinftm  33161  qusker  33342  qusvscpbl  33344  qusvsval  33345  mxidlval  33454  idlsrgval  33496  dimval  33613  dimvalfi  33614  smatfval  33741  lmatval  33759  locfinreflem  33786  rspecval  33810  rmulccn  33874  xrmulc1cn  33876  xrge0iifcv  33880  xrge0iifiso  33881  xrge0iifhom  33883  xrge0iif1  33884  qqhval  33920  rrhval  33942  xrhval  33964  ddeval1  34198  ddeval0  34199  sxbrsigalem0  34236  sxbrsigalem3  34237  eulerpartlemgv  34338  rrvmbfm  34407  dstrvval  34435  coinflippv  34448  ballotlem2  34453  ballotlemfval  34454  ballotlemi  34465  ballotlemsval  34473  ballotlemrval  34482  ballotth  34502  plymulx  34525  signstfv  34540  signsvvfval  34555  derangval  35135  subfacval  35141  erdszelem3  35161  erdszelem9  35167  erdszelem10  35168  txpconn  35200  indispconn  35202  cvxpconn  35210  cvmlift2lem2  35272  cvmlift2lem3  35273  cvmlift2lem7  35277  cvmliftphtlem  35285  cvmlift3lem4  35290  snmlfval  35298  snmlval  35299  gonafv  35318  mvtval  35468  mrsubffval  35475  mrsubcv  35478  mrsubrn  35481  elmrsubrn  35488  msubffval  35491  mvhval  35502  mpstval  35503  mstaval  35512  mclsval  35531  mppsval  35540  sinccvglem  35640  circum  35642  divcnvlin  35695  iprodefisum  35703  iprodgam  35704  faclimlem1  35705  faclimlem2  35706  faclim  35708  iprodfac  35709  faclim2  35710  dfrdg2  35759  findabrcl  36420  dnival  36437  bj-evalval  37041  bj-inftyexpitaudisj  37171  bj-inftyexpiinv  37174  bj-inftyexpidisj  37176  curfv  37560  finixpnum  37565  poimirlem16  37596  poimir  37613  broucube  37614  mblfinlem2  37618  voliunnfl  37624  volsupnfl  37625  itg2addnclem  37631  itg2addnclem3  37633  ftc1cnnc  37652  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anc  37661  ftc2nc  37662  fvopabf4g  37682  sdclem2  37702  fdc  37705  lmclim2  37718  geomcau  37719  istotbnd  37729  isbnd  37740  prdsbnd2  37755  heiborlem6  37776  heiborlem7  37777  heiborlem8  37778  rrnval  37787  rrncmslem  37792  idlval  37973  pridlval  37993  maxidlval  37999  lshpset  38934  lsatset  38946  lcvfbr  38976  lflset  39015  lflnegcl  39031  lshpkrlem1  39066  lshpkrlem2  39067  lshpkrlem3  39068  ldualset  39081  cmtfvalN  39166  cvrfval  39224  pats  39241  llnset  39462  lplnset  39486  lvolset  39529  lineset  39695  pointsetN  39698  psubspset  39701  pmapval  39714  paddfval  39754  pclfvalN  39846  polfvalN  39861  polvalN  39862  psubclsetN  39893  watvalN  39950  lhpset  39952  lautset  40039  pautsetN  40055  ldilset  40066  ltrnset  40075  dilsetN  40110  trnsetN  40113  trlset  40118  trlval  40119  tgrpset  40702  tendoset  40716  tendo02  40744  erngset  40757  erngset-rN  40765  cdlemksv  40801  dvaset  40962  dvaplusgv  40967  diafval  40988  diaval  40989  dvhset  41038  cdlemm10N  41075  docafvalN  41079  djafvalN  41091  dibfval  41098  dibval  41099  dicfval  41132  dicval  41133  dihval  41189  dochfval  41307  djhfval  41354  dochfl1  41433  lpolsetN  41439  lcdval  41546  mapdhval  41681  hvmapfval  41716  hdmap1fval  41753  fimgmcyc  42489  prjspval  42558  isnacs  42660  mzpclval  42681  mzpsubst  42704  mzprename  42705  mzpcompact2lem  42707  eldiophb  42713  diophrw  42715  eldioph2  42718  diophin  42728  diophun  42729  diophren  42769  pell1qrval  42802  pell14qrval  42804  pell1234qrval  42806  pellfundval  42836  rmxypairf1o  42868  rmxyval  42872  mzpcong  42929  pw2f1ocnv  42994  dnnumch1  43001  dfac11  43019  hbtlem1  43080  hbtlem7  43082  elmnc  43093  dgraaval  43101  mpaaval  43108  itgoval  43118  rgspnval  43125  flcidc  43131  mendval  43140  cytpval  43163  cantnfub  43283  cantnfresb  43286  tfsconcatrev  43310  elcnvlem  43563  comptiunov2i  43668  dftrcl3  43682  trclfvcom  43685  cnvtrclfv  43686  cotrcltrcl  43687  trclimalb2  43688  trclfvdecomr  43690  dfrtrcl3  43695  dfrtrcl4  43700  clsk1indlem0  44003  clsk1indlem2  44004  clsk1indlem3  44005  clsk1indlem4  44006  clsk1indlem1  44007  k0004val  44112  lhe4.4ex1a  44298  addrfv  44438  subrfv  44439  mulvfv  44440  monoord2xrv  45399  sumnnodd  45551  liminfgval  45683  ioodvbdlimc2lem  45855  itgsin0pilem1  45871  stoweidlem55  45976  wallispilem1  45986  wallispilem2  45987  wallispilem4  45989  wallispi2lem1  45992  wallispi2lem2  45993  dirkerval  46012  fourierdlem2  46030  fourierdlem3  46031  fourierdlem29  46057  fourierdlem62  46089  fourierdlem80  46107  fourierdlem103  46130  fourierdlem104  46131  fourierswlem  46151  fouriersw  46152  iundjiunlem  46380  carageniuncllem2  46443  0ome  46450  hoidmv1le  46515  hoidmvlelem3  46518  smflimsuplem7  46747  iccpval  47289  fppr  47600  bigoval  48283  ackval0  48414  ackval41a  48428  eenglngeehlnm  48473  prstcval  48731  mndtcval  48752  vsetrec  48795  onsetreclem1  48797  elpglem3  48805  pgindnf  48808  sinhval-named  48828  coshval-named  48829  tanhval-named  48830  secval  48839  cscval  48840  cotval  48841  aacllem  48895