Theorem eqidd 2738

Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008.)

Assertion

Ref	Expression
eqidd	⊢ (𝜑 → 𝐴 = 𝐴)

Proof of Theorem eqidd

Step	Hyp	Ref	Expression
1		eqid 2737	. 2 ⊢ 𝐴 = 𝐴
2	1	a1i 11	1 ⊢ (𝜑 → 𝐴 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  nfabd2  2923  neleq1  3043  neleq2  3044  elabd3  3614  nelrdva  3652  sbcbidv  3785  csbie2df  4384  reusngf  4619  rexreusng  4624  reuprg0  4647  iunxdif3  5038  mpteq1  5175  mpteq1i  5177  mpteq2da  5178  mpteq2dva  5179  nfcvb  5314  dfid2  5522  feq23d  6658  f10d  6809  fvmptdv2  6961  elrnrexdm  7036  f1ossf1o  7076  fmptco  7077  cofmpt  7080  fprg  7103  ftpg  7104  fmptsng  7117  fmptsnd  7118  f1dom3fv3dif  7217  f1dom3el3dif  7218  fliftfun  7261  fliftval  7265  nfriotad  7329  cbvmpo  7455  fconstmpo  7478  eqfnov2  7491  ovmpod  7513  ovmpodv2  7519  fvmpopr2d  7523  elovmporab  7607  elovmporab1w  7608  elovmporab1  7609  ovmpt3rab1  7619  elovmpt3rab  7622  ofval  7636  ofrval  7637  offn  7638  fnfvof  7642  off  7643  ofres  7644  coof  7649  ofco  7650  caofref  7656  caofid0l  7658  caofid0r  7659  caofid1  7660  caofid2  7661  caofrss  7664  caoftrn  7666  tfisi  7804  fsplitfpar  8062  fczsupp0  8137  suppssof1  8143  suppofss1d  8148  suppofss2d  8149  fvmpocurryd  8215  fpr3g  8229  iserd  8664  fsetfocdm  8802  ixpsnf1o  8880  mapxpen  9075  dffi3  9338  cantnf0  9590  cantnfp1  9596  cantnflem1  9604  ttrcltr  9631  axcclem  10373  ttukeylem3  10427  fpwwe2lem8  10555  ofsubeq0  12150  ofnegsub  12151  ofsubge0  12152  fzo0to3tp  13701  fzo1to4tp  13703  modsubmod  13885  seqid  14003  seqid2  14004  seqz  14006  seqof  14015  elovmptnn0wrd  14515  ccatdmss  14538  ccatws1ls  14590  pfxsuffeqwrdeq  14654  wrdind  14678  wrd2ind  14679  ccats1pfxeqbi  14698  repswsymb  14730  repswsymball  14735  repswsymballbi  14736  s3eq2  14826  swrds2m  14897  wrdl2exs2  14902  swrd2lsw  14908  wwlktovfo  14914  s3sndisj  14923  s3iunsndisj  14924  relexp0g  14978  relexpsucnnr  14981  relexp1g  14982  rtrclreclem1  15013  rtrclreclem4  15017  dfrtrcl2  15018  rlim2  15452  climcl  15455  rlimcl  15459  clim2  15460  rlimclim1  15501  rlimclim  15502  climrlim2  15503  climuni  15508  rlimres  15514  climeq  15523  2clim  15528  climshftlem  15530  climabs0  15541  climcn1  15548  climcn2  15549  o1of2  15569  o1rlimmul  15575  o1add2  15580  o1mul2  15581  o1sub2  15582  o1dif  15586  climsqz  15597  climsqz2  15598  rlimdiv  15602  isercoll  15624  climsup  15626  climcau  15627  caurcvgr  15630  caucvgb  15636  serf0  15637  iseralt  15641  sumz  15678  fsumss  15681  fsumsplitsn  15700  fsumsplit1  15701  fsumsplitsnun  15711  isumclim3  15715  isummulc2  15718  fsum2dlem  15726  fsumconst  15746  fsumabs  15758  fsumparts  15763  fsumrlim  15768  fsumo1  15769  seqabs  15771  cvgcmpce  15775  fsumiun  15778  ackbijnn  15787  isumshft  15798  isumltss  15807  climcndslem1  15808  climcndslem2  15809  climcnds  15810  mertenslem1  15843  mertenslem2  15844  prod1  15903  fprodss  15907  fprodconst  15937  fprod2dlem  15939  fprodsplitsn  15948  iprodclim3  15959  eftlcl  16068  reeftlcl  16069  eftlub  16070  efsep  16071  effsumlt  16072  eirrlem  16165  rpnnen2lem6  16180  rpnnen2lem7  16181  rpnnen2lem8  16182  rpnnen2lem9  16183  rpnnen2lem12  16186  2tp1odd  16315  sadasslem  16433  smupvallem  16446  smumul  16456  alginv  16538  algfx  16543  cncongr1  16630  qnumdencoprm  16709  qeqnumdivden  16710  vdwlem1  16946  vdwlem12  16957  vdwlem13  16958  prmodvdslcmf  17012  prmgap  17024  prmgaplcm  17025  prmgapprmo  17027  setsexstruct2  17139  setsstruct  17140  prdssca  17413  prdsbas  17414  prdsplusg  17415  prdsmulr  17416  prdsvsca  17417  prdsip  17418  prdsle  17419  prdsds  17421  prdstset  17423  prdshom  17424  prdsco  17425  prdsvscafval  17437  prdsdsval2  17441  prdsdsval3  17442  pwsle  17450  pwsleval  17451  pwsvscaval  17453  imasbas  17470  imasds  17471  imasplusg  17475  imasmulr  17476  imassca  17477  imasvsca  17478  imasip  17479  imastset  17480  imasle  17481  imasvscafn  17495  imasvscaval  17496  qusin  17502  xpsvsca  17535  iscat  17632  iscatd  17633  iscatd2  17641  0catg  17648  homfeq  17654  homfeqd  17655  comfffval2  17661  comffval2  17662  comfeq  17666  comfeqd  17667  oppccatid  17679  2oppccomf  17685  moni  17697  rcaninv  17755  ssc2  17783  ssctr  17786  ssceq  17787  subcssc  17801  subccat  17809  subsubc  17814  funcres  17857  funcres2  17859  idfusubc  17861  funcres2c  17864  idffth  17896  cofull  17897  cofth  17898  ressffth  17901  isnat  17911  fuccofval  17923  fuccatid  17933  fucpropd  17941  elhomai  17994  coafval  18025  setcval  18038  setcbas  18039  setchomfval  18040  setccofval  18043  setcco  18044  setccatid  18045  setcepi  18049  funcsetcres2  18054  catcval  18061  catcbas  18062  catchomfval  18063  catccofval  18065  catcco  18066  catccatid  18067  catcfuccl  18079  estrcval  18084  estrcbas  18085  estrchomfval  18086  estrccofval  18089  estrcco  18090  estrccatid  18092  estrreslem2  18098  fullestrcsetc  18111  fullsetcestrc  18126  xpcbas  18138  xpchomfval  18139  xpccofval  18142  xpccatid  18148  prfval  18159  catcxpccl  18167  xpcpropd  18168  evlfval  18177  curfval  18183  curf1  18185  curf12  18187  curf2  18189  curf2val  18190  hofval  18212  hof2fval  18215  hofcllem  18218  oppchofcl  18220  oppcyon  18229  oyoncl  18230  yonedalem4a  18235  yonedalem4b  18236  yonedainv  18241  oduposb  18287  joinval  18335  meetval  18349  isdlat  18482  ipopos  18496  pfxchn  18570  chnind  18581  chnso  18584  chnccats1  18585  chnccat  18586  chnrev  18587  gsumpropd  18640  gsumpropd2lem  18641  gsumval1  18645  gsumval2a  18647  issgrp  18682  issgrpd  18692  prdssgrpd  18695  ismndd  18718  mndprop  18722  prdsmndd  18732  imasmnd2  18736  insubm  18780  mhmima  18787  frmdbas  18814  frmdmnd  18821  efmnd  18832  smndex1gid  18866  smndex1gidOLD  18867  smndex1n0mnd  18877  smndex2dlinvh  18882  sgrpnmndex  18897  resgrpplusfrn  18920  grpprop  18922  grpsubfval  18953  grpsubfvalALT  18954  grpsubpropd  19015  prdsgrpd  19020  imasgrp2  19025  imasgrp  19026  imasgrpf1  19027  mulgfval  19039  mulgfvalALT  19040  mulgnngsum  19049  mulgnn0gsum  19050  mulgpropd  19086  subgsub  19108  eqgfval  19145  qusgrp  19155  ghmqusnsglem1  19249  ghmqusnsglem2  19250  ghmqusnsg  19251  ghmquskerlem1  19252  ghmquskerlem2  19254  ghmquskerlem3  19255  ghmqusker  19256  oppgmnd  19323  oppgmndb  19324  oppggrp  19326  oppggrpb  19327  symgval  19340  symg1bas  19360  symg2bas  19362  symgvalstruct  19366  symggrp  19369  gsmsymgrfixlem1  19396  gsmsymgreqlem2  19400  symgfixels  19403  symgsssg  19436  symgfisg  19437  psgnunilem4  19466  psgnvalii  19478  oppglsm  19611  lsmelvalmi  19621  efgi0  19689  efgi1  19690  efgtf  19691  efgval2  19693  efginvrel2  19696  frgp0  19729  frgpup3lem  19746  ablprop  19762  subcmn  19806  gex2abl  19820  prdscmnd  19830  qusabl  19834  abl1  19835  cygabl  19860  gsumzf1o  19881  gsumzaddlem  19890  gsumzsplit  19896  gsumconst  19903  gsumconstf  19904  gsummptshft  19905  gsummhm2  19908  gsummptmhm  19909  gsumzunsnd  19925  gsumunsnfd  19926  gsumpt  19931  gsummptf1o  19932  gsummptun  19933  gsum2dlem2  19940  gsumcom2  19944  nn0gsumfz  19953  dprdval  19974  dprdssv  19987  dprdfeq0  19993  dprdsubg  19995  dprdspan  19998  dprdz  20001  subgdmdprd  20005  subgdprd  20006  gsumle  20114  isrng  20129  isrngd  20148  prdsrngd  20151  imasrng  20152  issrg  20163  isring  20212  ringabl  20256  ringprop  20265  isringd  20266  prdsringd  20294  prdscrngd  20295  prds1  20296  pwspjmhmmgpd  20301  imasring  20304  opprrng  20319  opprrngb  20320  opprringb  20322  dvrfval  20376  rnghmf1o  20426  c0mgm  20433  c0mhm  20434  c0snmgmhm  20436  c0snmhm  20437  rngisomring1  20442  rhmf1o  20464  pwsco1rhm  20473  pwsco2rhm  20474  zrrnghm  20507  rhmimasubrng  20537  pwsdiagrhm  20578  rngcbas  20592  rngchomfval  20593  dfrngc2  20599  rnghmsscmap2  20600  rnghmsscmap  20601  rngccat  20605  rngcid  20606  funcrngcsetc  20611  funcrngcsetcALT  20612  zrinitorngc  20613  zrtermorngc  20614  ringcbas  20621  ringchomfval  20622  dfringc2  20628  rhmsscmap2  20629  rhmsscmap  20630  ringccat  20634  ringcid  20635  rngcresringcat  20640  funcringcsetc  20645  zrtermoringc  20646  rhmsubc  20660  drngprop  20715  isdrngd  20736  isdrngrd  20737  isdrngdOLD  20738  isdrngrdOLD  20739  abvtrivd  20803  idsrngd  20827  suborng  20847  islmodd  20855  lmodabl  20898  lss1  20927  lsssn0  20937  islss3  20948  lss1d  20952  lssintcl  20953  prdslmodd  20958  idlmhm  21031  invlmhm  21032  lmhmvsca  21035  lbsextlem2  21152  sralmod  21177  sralmod0  21178  rlm0  21185  rlmvneg  21196  rnglidlmsgrp  21239  rnglidlrng  21240  qus2idrng  21266  crngridl  21273  quscrng  21276  rhmqusnsg  21278  rngqiprngimf1lem  21287  rngqiprngimf1  21293  dfcnfldOLD  21363  absabv  21417  pzriprnglem10  21483  zrhpropd  21507  fermltlchr  21522  znzrh  21535  znbas  21536  zncrng  21537  znzrhfo  21540  znf1o  21544  frgpcyg  21566  evpmodpmf1o  21589  isphld  21647  phlpropd  21648  phssip  21651  phlssphl  21652  pjfval  21699  dsmmval  21727  dsmmsubg  21736  frlmip  21771  frlmipval  21772  frlmphllem  21773  frlmphl  21774  islindf  21805  islindf4  21831  isassa  21849  isassad  21858  issubassa3  21859  asclfval  21871  ressascl  21889  psrval  21908  psrbaglesupp  21915  psrbagcon  21918  psrbaglefi  21919  psrbagleadd1  21921  psrbagconf1o  21922  gsumbagdiaglem  21923  psrass1lem  21925  psrbas  21926  psrplusg  21929  psrmulr  21934  psrsca  21939  psrvscafval  21940  psrvscaval  21942  psrlmod  21951  psrlidm  21953  psrdi  21956  psrdir  21957  psrcom  21959  psrring  21961  psrassa  21964  mplsubglem  21990  mpllsslem  21991  mplvscaval  22007  mplcoe1  22028  mplcoe3  22029  mplcoe5  22031  opsrcrng  22050  opsrassa  22051  mplmon2  22052  evlslem2  22070  evlslem1  22073  evlsvvval  22084  mhpmulcl  22128  psdffval  22136  psdmplcl  22141  psdadd  22142  psdmul  22145  psdmvr  22148  ply1lss  22173  ply1subrg  22174  opsr0  22195  opsr1  22196  subrgply1  22209  psrplusgpropd  22212  psropprmul  22214  opsrring  22221  opsrlmod  22222  ply1mpl0  22233  ply1mpl1  22235  coe1z  22241  coe1mul2  22247  coe1tm  22251  coe1sclmulfv  22261  ply1coe  22276  evls1rhm  22300  evls1sca  22301  evl1rhm  22310  evl1sca  22312  evl1expd  22323  evl1gsumdlem  22334  evl1varpw  22339  evls1maplmhm  22355  mamufval  22370  mamudi  22381  mamudir  22382  mat0  22395  matinvg  22396  matlmod  22407  matinvgcell  22413  matring  22421  matassa  22422  mat0dimcrng  22448  mat1dim0  22451  mat1f1o  22456  dmatmulcl  22478  scmatval  22482  scmatscmiddistr  22486  scmataddcl  22494  scmatsubcl  22495  scmatmulcl  22496  scmatlss  22503  scmatrhmcl  22506  1mavmul  22526  mavmul0  22530  marepvfval  22543  submafval  22557  submaval  22559  mdetleib2  22566  mdet0pr  22570  m1detdiag  22575  mdetrsca  22581  mdetrsca2  22582  mdetrlin2  22585  mdetralt  22586  mdetralt2  22587  mdetunilem2  22591  mdetunilem5  22594  mdetunilem9  22598  mdetuni0  22599  m2detleib  22609  madufval  22615  symgmatr01lem  22631  symgmatr01  22632  gsummatr01lem3  22635  gsummatr01lem4  22636  gsummatr01  22637  smadiadetlem3  22646  smadiadetglem2  22650  smadiadetr  22653  mat2pmatghm  22708  cpm2mfval  22727  m2cpminvid  22731  m2cpminvid2lem  22732  m2cpminvid2  22733  decpmatval  22743  decpmataa0  22746  decpmatmul  22750  pmatcollpw1  22754  pmatcollpw2lem  22755  monmatcollpw  22757  pmatcollpwlem  22758  pmatcollpw  22759  pmatcollpwscmatlem2  22768  pm2mpval  22773  pm2mpcl  22775  pm2mpf1  22777  mptcoe1matfsupp  22780  mp2pm2mplem3  22786  mp2pm2mplem4  22787  pm2mpghm  22794  pm2mpmhmlem2  22797  chpmat1dlem  22813  chp0mat  22824  fvmptnn04ifa  22828  fvmptnn04ifb  22829  fvmptnn04ifc  22830  fvmptnn04ifd  22831  cpmadugsumlemB  22852  chcoeffeqlem  22863  epttop  22987  ordtbas2  23169  ordtopn1  23172  ordtopn2  23173  lmss  23276  2ndci  23426  2ndcsep  23437  dis2ndc  23438  1stcelcls  23439  dissnlocfin  23507  ptbasid  23553  xkoopn  23567  prdstopn  23606  ptrescn  23617  txlm  23626  lmcn2  23627  tx1stc  23628  xkopt  23633  cnmpt2c  23648  cnmptk1  23659  cnmpt1k  23660  cnmptkk  23661  qtopeu  23694  txswaphmeolem  23782  xpstopnlem1  23787  ptcmpfi  23791  xkohmeo  23793  rnelfmlem  23930  rnelfm  23931  hauspwpwf1  23965  lmflf  23983  flfcnp2  23985  alexsubb  24024  tmdgsum  24073  tgpconncomp  24091  qustgphaus  24101  tsmsfbas  24106  tsmspropd  24110  tsmssplit  24130  tsmsxplem1  24131  tsmsxplem2  24132  ustuqtop4  24222  imasdsf1olem  24351  blfvalps  24361  stdbdxmet  24493  met2ndci  24500  prdsxmslem2  24507  metustexhalf  24534  cfilucfil  24537  restmetu  24548  nmfval  24566  nmpropd  24572  nmpropd2  24573  subgnm  24611  tng0  24621  tngnm  24629  tnggrpr  24633  tngngp3  24634  tngnrg  24652  sranlm  24662  qdensere  24747  mpomulcn  24847  fsumcn  24850  cncfcompt2  24888  cncfmpt1f  24894  negfcncf  24903  oprpiece1res2  24932  htpyid  24957  phtpyid  24969  pcofval  24990  pcopt2  25003  om1bas  25011  om1plusg  25014  om1tset  25015  pi1bas  25018  pi1bas2  25021  pi1eluni  25022  pi1bas3  25023  pi1cpbl  25024  pi1addf  25027  pi1addval  25028  pi1grplem  25029  pi1xfr  25035  pi1xfrcnvlem  25036  pi1coghm  25041  cphassr  25192  tcphphl  25207  ipcau2  25214  cphipval  25223  lmnn  25243  iscau  25256  cmetcaulem  25268  iscmet3lem1  25271  causs  25278  lmclim  25283  srabn  25340  rrxprds  25369  rrxip  25370  rrxcph  25372  rrxds  25373  rrxmvallem  25384  rrxmval  25385  rrxdsfival  25393  ehl2eudisval  25403  divcncf  25427  ovollb2lem  25468  ovolfiniun  25481  ovolicc2lem4  25500  shftmbl  25518  volfiniun  25527  ioombl1lem4  25541  uniioombllem2  25563  uniioombllem6  25568  vitalilem4  25591  mbfmulc2lem  25627  mbfmulc2re  25628  mbfneg  25630  mbfaddlem  25640  mbfadd  25641  mbfsub  25642  mbfmulc2  25643  0plef  25652  0pledm  25653  itg1ge0  25666  i1faddlem  25673  i1fmullem  25674  i1fmulclem  25682  itg1mulc  25684  itg1lea  25692  itg1le  25693  mbfi1flimlem  25702  mbfmullem2  25704  mbfmul  25706  xrge0f  25711  itg2ge0  25715  itg2const  25720  itg2const2  25721  itg2uba  25723  itg2lea  25724  itg2splitlem  25728  itg2split  25729  itg2monolem1  25730  itg2mono  25733  itg2i1fseqle  25734  itg2i1fseq  25735  itg2addlem  25738  itg2gt0  25740  itg2cnlem1  25741  itg2cnlem2  25742  isibl2  25746  iblitg  25748  itgcl  25764  ibl0  25767  iblcnlem1  25768  itgcnlem  25770  iblss  25785  iblss2  25786  i1fibl  25788  itgitg1  25789  itgle  25790  itgeqa  25794  iblconst  25798  ibladdlem  25800  ibladd  25801  itgaddlem1  25803  itgfsum  25807  iblabslem  25808  iblabs  25809  iblabsr  25810  iblmulc2  25811  itgmulc2lem1  25812  itgsplit  25816  bddmulibl  25819  bddibl  25820  bddiblnc  25822  limccnp2  25872  limcco  25873  dvidlem  25895  dvcnp2  25900  dvaddbr  25918  dvmulbr  25919  dvaddf  25922  dvcmulf  25925  dvexp  25933  dvmptadd  25940  dvmptmul  25941  dvmptco  25952  dvmptfsum  25955  dvcnvlem  25956  dvef  25960  rolle  25970  mvth  25972  dvlip  25973  dvlipcn  25974  lhop1lem  25993  itgsubstlem  26028  itgpowd  26030  ply1divalg2  26117  uc1pmon1p  26130  q1pval  26133  r1pval  26136  elply2  26174  elplyr  26179  plypf1  26190  plyaddlem1  26191  coeeulem  26202  plyco  26219  coeaddlem  26227  coemulc  26233  dgradd2  26246  dgrcolem1  26251  dgrcolem2  26252  dgrco  26253  ofmulrt  26261  plydivlem3  26275  plydivlem4  26276  plyrem  26285  iaa  26305  aareccl  26306  aannenlem2  26309  aaliou3lem3  26324  aaliou3lem7  26329  taylfval  26338  taylply2  26347  taylply2OLD  26348  dvntaylp  26351  taylthlem2  26354  taylthlem2OLD  26355  ulmclm  26368  ulmres  26369  ulmshftlem  26370  ulm0  26372  ulmcau  26376  ulmss  26378  ulmbdd  26379  ulmcn  26380  mtest  26385  mtestbdd  26386  iblulm  26388  itgulm  26389  pserulm  26403  pserdvlem2  26409  abelthlem5  26416  abelthlem6  26417  abelthlem8  26420  abelthlem9  26421  sincn  26425  coscn  26426  efcvx  26430  efabl  26530  logfac  26581  logcn  26627  chordthmlem  26812  chordthmlem5  26816  mcubic  26827  leibpi  26922  efrlim  26949  efrlimOLD  26950  amgmlem  26970  lgamgulmlem2  27010  basellem7  27067  basellem9  27069  musum  27171  chtublem  27191  logexprlim  27205  dchrbas  27215  dchr1cl  27231  dchrabl  27234  dchrfi  27235  dchrhash  27251  bposlem6  27269  lgsdir2lem5  27309  gausslemma2dlem1  27346  lgseisenlem2  27356  lgseisenlem3  27357  lgseisenlem4  27358  lgsquad2lem2  27365  2lgslem1b  27372  2lgslem3b1  27381  2lgslem3c1  27382  2lgsoddprmlem4  27395  2sqlem8  27406  2sqlem11  27409  2sqreulem1  27426  2sqreunnlem1  27429  chtppilimlem2  27454  chebbnd2  27457  chpchtlim  27459  chpo1ub  27460  vmadivsum  27462  rpvmasumlem  27467  dchrisum0re  27493  dchrisum0  27500  mudivsum  27510  selberglem1  27525  selberglem2  27526  selberg2lem  27530  selberg2  27531  pntrsumo1  27545  selbergr  27548  abvcxp  27595  nosupfv  27687  noinffv  27702  madecut  27892  elons2  28267  oncutlt  28273  oniso  28280  seqsfn  28318  seqs1  28319  seqsp1  28320  n0fincut  28364  zcuts  28416  twocut  28432  expsval  28434  pw2cut2  28471  z12addscl  28486  z12shalf  28489  z12zsodd  28491  istrkgld  28544  istrkg2ld  28545  tgsegconeq  28571  tgbtwnouttr2  28580  ercgrg  28602  cgr3id  28604  tgbtwnxfr  28615  motgrp  28628  tgbtwnconn1lem3  28659  legov  28670  legid  28672  btwnleg  28673  legbtwn  28679  mirreu3  28739  mirinv  28751  miduniq1  28771  colmid  28773  krippenlem  28775  israg  28782  ragcgr  28792  motrag  28793  perpneq  28799  isperp2  28800  isperp2d  28801  footexALT  28803  footexlem1  28804  footexlem2  28805  foot  28807  perprag  28811  perpdragALT  28812  colperpexlem1  28815  mideulem2  28819  opphllem2  28833  opphllem3  28834  opphllem4  28835  midbtwn  28864  midcom  28867  mirmid  28868  lmieu  28869  lmif  28870  islmib  28872  lmilmi  28874  lmieq  28876  lmiinv  28877  lmiisolem  28881  hypcgrlem1  28884  hypcgrlem2  28885  lmiopp  28887  trgcopyeu  28891  iscgra  28894  iscgra1  28895  iscgrad  28896  sacgr  28916  isinag  28923  isinagd  28924  inagflat  28925  inaghl  28930  isleag  28932  isleagd  28933  ttgval  28960  cchhllem  28972  usgredg4  29303  ushgredgedg  29315  ushgredgedgloop  29317  usgrstrrepe  29321  uspgr1e  29330  uhgrspan1  29389  usgrres1  29401  nbgrnself  29445  nbusgredgeu  29452  cusgrfilem2  29543  finsumvtxdg2size  29637  finsumvtxdgeven  29639  wlk1walk  29725  uspgr2wlkeq  29732  uspgr2wlkeqi  29734  wlkonwlk  29747  wlkonwlk1l  29748  usgr2trlncl  29846  crctcshwlkn0lem7  29902  wwlksnredwwlkn  29981  wwlksnextbij  29988  wwlksnextprop  29998  wwlksnwwlksnon  30001  elwwlks2ons3im  30040  clwlkclwwlk2  30091  clwlkclwwlkfo  30097  clwlkclwwlkf1  30098  clwwlkwwlksb  30142  clwlknf1oclwwlkn  30172  clwwlknonmpo  30177  clwwlknonex2lem2  30196  0pthon1  30216  uhgr3cyclex  30270  iseupth  30289  eupth0  30302  eupth2lem2  30307  frgr3vlem1  30361  3vfriswmgrlem  30365  2clwwlk2clwwlklem  30434  wlkl0  30455  numclwlk1lem2  30458  grpodivfval  30623  dipfval  30791  ipval2  30796  lnoval  30841  minvecolem3  30965  h2hcau  31068  h2hlm  31069  opsqrlem3  32231  opsqrlem4  32232  foresf1o  32592  disjnf  32658  disjdifprg  32663  iundisjf  32677  br8d  32699  fnfvor  32700  ofrco  32701  ofrn2  32731  off2  32732  ofresid  32733  fmptcof2  32748  aciunf1  32754  ofpreima  32756  f1ocnt  32891  sgnneg  32924  prodindf  32940  indf1ofs  32944  wrdfsupp  33015  wrdpmcl  33016  pfxf1  33020  s1f1  33021  wrdt2ind  33031  swrdrn2  33032  ressnm  33042  abvpropd2  33043  ismntd  33062  dfmgc2lem  33073  pwrssmgc  33078  gsummpt2d  33128  gsummptf1od  33134  gsummptfsf1o  33139  gsumhashmul  33146  gsumwrd2dccat  33157  wrdpmtrlast  33172  psgnfzto1stlem  33179  fzto1st1  33181  tocycfv  33188  cycpmcl  33195  tocycf  33196  tocyc01  33197  cycpmco2f1  33203  cycpmco2rn  33204  cycpmco2lem1  33205  cycpmco2lem2  33206  cycpmco2lem3  33207  cycpmco2lem4  33208  cycpmco2lem5  33209  cycpmco2lem6  33210  cycpmco2lem7  33211  cycpmco2  33212  cycpm3cl2  33215  cycpmconjv  33221  tocyccntz  33223  cyc3evpm  33229  cyc3genpm  33231  cycpmgcl  33232  cycpmconjslem2  33234  cyc3conja  33236  sgnsv  33239  inftmrel  33259  isinftm  33260  submarchi  33265  isslmd  33281  urpropd  33310  elrgspnlem1  33321  elrgspnlem2  33322  elrgspnlem4  33324  elrgspn  33325  elrgspnsubrun  33328  erlval  33337  rlocval  33338  rlocbas  33346  rlocaddval  33347  rlocmulval  33348  rloccring  33349  resv0g  33416  resvcmn  33418  imaslmod  33431  imasmhm  33432  imasghm  33433  imasrhm  33434  imaslmhm  33435  znfermltl  33444  islinds5  33445  ellspds  33446  linds2eq  33459  lindfpropd  33460  elringlsmd  33472  nsgmgclem  33489  nsgmgc  33490  rhmquskerlem  33503  elrspunsn  33507  idlinsubrg  33509  qsidomlem1  33530  qsidomlem2  33531  opprqusbas  33566  qsdrngi  33573  rprmval  33594  rprmnz  33598  rprmnunit  33599  unitmulrprm  33606  1arithidomlem1  33613  1arithidomlem2  33614  1arithidom  33615  1arithufdlem3  33624  dfufd2lem  33627  ply1dg1rt  33658  ply1mulrtss  33660  ply1degltlss  33674  ply1gsumz  33677  r1pquslmic  33689  mplvrpmfgalem  33706  psrmonprod  33714  esplyfvaln  33736  esplyind  33737  vietalem  33741  sra1r  33743  sradrng  33744  sraidom  33745  srasubrg  33746  resssra  33749  drgext0g  33752  drgextlsp  33756  rlmdim  33772  rgmoddimOLD  33773  tnglvec  33775  tngdim  33776  matdim  33778  ply1degltdimlem  33785  lbsdiflsp0  33789  dimkerim  33790  fedgmullem2  33793  lactlmhm  33797  extdg1id  33829  ccfldsrarelvec  33834  ccfldextdgrr  33835  fldextrspunlsplem  33836  fldextrspunlsp  33837  fldextrspunlem1  33838  fldextrspunfld  33839  fldextrspunlem2  33840  extdgfialglem1  33855  extdgfialglem2  33856  irredminply  33879  algextdeglem3  33882  algextdeglem4  33883  algextdeglem8  33887  constrsslem  33904  constrext2chnlem  33913  constrcon  33937  2sqr3nconstr  33944  cos9thpinconstrlem2  33953  1smat1  33967  submatres  33969  submateq  33972  lmatcl  33979  mdetlap1  33989  madjusmdetlem3  33992  circtopn  34000  locfinref  34004  tpr2rico  34075  lmdvglim  34117  qqhval  34135  esumeq1  34197  esumeq1d  34198  esumeq2d  34200  esumf1o  34213  esumsplit  34216  esumadd  34220  gsumesum  34222  esumlub  34223  esumaddf  34224  esumcst  34226  esumsnf  34227  esumpinfval  34236  esumcocn  34243  esummulc1  34244  esumcvg  34249  esum2d  34256  ofcval  34262  ofcfn  34263  ofcfeqd2  34264  ofcf  34266  ofcfval4  34268  ofcof  34270  sigapildsys  34325  sxval  34353  measvunilem0  34376  measvuni  34377  measiun  34381  meascnbl  34382  measinb  34384  volmeas  34394  sxbrsiga  34453  omssubadd  34463  fiunelcarsg  34479  itgeq12dv  34489  sitgval  34495  eulerpartlems  34523  eulerpartgbij  34535  eulerpartlemn  34544  sseqf  34555  sseqp1  34558  totprobd  34589  probfinmeasb  34591  probmeasb  34593  rrvadd  34615  dstfrvclim1  34641  gsumnunsn  34704  plymul02  34709  plymulx  34711  signsply0  34714  fdvneggt  34763  fdvnegge  34765  itgexpif  34769  reprpmtf1o  34789  circlemethhgt  34806  logdivsqrle  34813  hgt750lemg  34817  hgt750lemb  34819  hgt750lema  34820  f1resfz0f1d  35315  2cycl2d  35340  quartfull  35366  sconnpi1  35440  cvmliftphtlem  35518  cvmlift3lem2  35521  satfv1  35564  satfdmlem  35569  satf0suc  35577  satf0op  35578  sat1el2xp  35580  fmla  35582  fmlasuc0  35585  fmlafvel  35586  fmlasuc  35587  fmla1  35588  satffunlem1lem2  35604  satffunlem2lem2  35607  sategoelfvb  35620  satfv1fvfmla1  35624  2goelgoanfmla1  35625  elmsubrn  35729  msubco  35732  mthmpps  35783  r1peuqusdeg1  35844  sinccvg  35874  circum  35875  br8  35957  br4  35959  brsegle  36309  hilbert1.1  36355  itgeq2sdv  36421  ditgeq3sdv  36424  cbvoprab23davw  36477  cbvoprab13davw  36478  trer  36517  knoppcnlem4  36775  knoppcnlem9  36780  knoppcnlem11  36782  knoppndvlem6  36796  knoppf  36814  bj-imdirco  37523  bj-fvmptunsn2  37591  bj-finsumval0  37618  exrecfnlem  37712  finxpreclem1  37722  matunitlindflem1  37954  matunitlindflem2  37955  poimirlem1  37959  poimirlem2  37960  poimirlem3  37961  poimirlem4  37962  poimirlem5  37963  poimirlem6  37964  poimirlem7  37965  poimirlem10  37968  poimirlem11  37969  poimirlem12  37970  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem22  37980  poimirlem23  37981  poimirlem28  37986  poimirlem29  37987  poimirlem31  37989  broucube  37992  mblfinlem2  37996  volsupnfl  38003  itg2addnclem  38009  itg2addnclem3  38011  itg2addnc  38012  itg2gt0cn  38013  ibladdnclem  38014  itgaddnclem1  38016  itgaddnc  38018  iblabsnclem  38021  iblabsnc  38022  iblmulc2nc  38023  itgmulc2nclem1  38024  itgmulc2nclem2  38025  itgmulc2nc  38026  ftc1anclem2  38032  ftc1anclem4  38034  ftc1anclem5  38035  ftc1anclem6  38036  ftc1anclem7  38037  ftc1anclem8  38038  ftc1anc  38039  areacirc  38051  unirep  38052  upixp  38067  sdc  38082  lmclim2  38096  geomcau  38097  caures  38098  caushft  38099  prdsbnd2  38133  heibor1lem  38147  bfplem2  38161  rrncmslem  38170  isrngo  38235  iuneq2f  38494  dmec2d  38649  lflset  39522  islfld  39525  lfladdcl  39534  lflvscl  39540  lkrsc  39560  eqlkr2  39563  lshpkrlem1  39573  ldualset  39588  ldualvaddval  39594  ldualvsval  39601  ldualgrplem  39608  lduallmodlem  39615  cmtfvalN  39673  isoml  39701  iscvlat  39786  llni2  39975  lplni2  40000  lvoli3  40040  lvoli2  40044  paddfval  40260  lhpset  40458  ltrnfset  40580  trlfset  40623  cdleme21k  40801  cdlemeiota  41048  tgrpfset  41207  tgrpset  41208  tgrpabl  41214  tendo0cbv  41249  tendo02  41250  erngfset  41262  erngset  41263  erngfset-rN  41270  erngset-rN  41271  cdlemkid5  41398  cdlemkid  41399  dvafset  41467  dvaset  41468  diaffval  41493  dialss  41509  diaf11N  41512  dvhfset  41543  dvhset  41544  docaffvalN  41584  dibfval  41604  dibf11N  41624  diblss  41633  diclss  41656  dihord2cN  41684  dihord11b  41685  dihffval  41693  dihord6apre  41719  dihglblem2aN  41756  dihglblem2N  41757  dihjatcclem4  41884  lclkrs  42002  mapdh6dN  42202  mapdh6eN  42203  mapdh6fN  42204  mapdh6jN  42208  hvmapffval  42221  hvmapfval  42222  mapdh8a  42238  mapdh8ad  42242  mapdh8d0N  42245  mapdh8d  42246  mapdh8i  42249  mapdh8j  42250  mapdh9a  42252  mapdh9aOLDN  42253  hdmap1l6d  42276  hdmap1l6e  42277  hdmap1l6f  42278  hdmap1l6j  42282  hdmapval2  42295  hdmapeveclem  42297  hdmapval3lemN  42300  hdmap11lem1  42304  hgmapfval  42349  hlhils0  42408  hlhils1N  42409  hlhillvec  42414  hlhildrng  42415  hlhil0  42418  hlhillsm  42419  rhmzrhval  42428  zndvdchrrhm  42429  3factsumint1  42477  lcmineqlem12  42496  aks4d1p1p4  42527  aks4d1p1p7  42530  aks4d1p9  42544  isprimroot  42549  primrootsunit1  42553  posbezout  42556  primrootscoprbij  42558  remexz  42560  aks6d1c1p2  42565  aks6d1c1p3  42566  aks6d1c1p4  42567  aks6d1c1p5  42568  aks6d1c1p7  42569  evl1gprodd  42573  aks6d1c2p2  42575  hashscontpow  42578  aks6d1c2lem4  42583  aks6d1c2  42586  aks6d1c5lem2  42594  aks6d1c5  42595  deg1gprod  42596  2np3bcnp1  42600  2ap1caineq  42601  sticksstones8  42609  sticksstones10  42611  sticksstones12a  42613  sticksstones12  42614  sticksstones17  42619  sticksstones18  42620  sticksstones19  42621  sticksstones21  42623  sticksstones22  42624  aks6d1c6lem1  42626  aks6d1c6lem2  42627  aks6d1c6lem4  42629  aks6d1c6isolem1  42630  aks5lem3a  42645  grpods  42650  unitscyglem1  42651  unitscyglem2  42652  ofun  42694  redivcan2d  42896  redivcan3d  42897  sn-rediv0d  42902  sn-redividd  42903  rhmpsr1  43013  mplmapghm  43014  evlsmaprhm  43023  selvvvval  43035  evlselv  43037  selvadd  43038  selvmul  43039  fsuppind  43040  mhphf  43047  3cubeslem3r  43136  eldiophb  43206  eldioph  43207  eldioph3  43215  rabren3dioph  43264  pellqrexplicit  43326  rmxycomplete  43366  rmxynorm  43367  acongrep  43429  jm2.26a  43449  jm2.26  43451  fnwe2lem2  43500  fnwe2lem3  43501  aomclem5  43507  aomclem8  43510  imasgim  43549  isnumbasgrplem1  43550  hbtlem5  43577  dgrsub2  43584  rgspnid  43617  rngunsnply  43618  mendval  43628  mendring  43637  mendlmod  43638  mendassa  43639  nnoeomeqom  43761  tfsconcatb0  43793  oaun3  43831  safesnsupfilb  43866  fsovrfovd  44457  fsovcnvlem  44461  mnring0gd  44669  mnringlmodd  44674  mnringmulrcld  44676  colleq1  44702  colleq2  44703  dvgrat  44760  radcnvrat  44762  hashnzfzclim  44770  caofcan  44771  ofsubid  44772  ofmul12  44773  ofdivrec  44774  ofdivcan4  44775  ofdivdiv2  44776  expgrowth  44783  binomcxplemnn0  44797  binomcxplemrat  44798  binomcxplemdvbinom  44801  binomcxplemnotnn0  44804  wessf1ornlem  45636  disjf1o  45642  ssnnf1octb  45645  mapss2  45655  icof  45669  mpteq1df  45686  infnsuprnmpt  45700  upbdrech  45759  divcan8d  45766  dmmcand  45767  suplesup  45790  ssuzfz  45800  supsubc  45804  xralrple2  45805  fprodabs2  46046  fprodcn  46051  clim1fr1  46052  climrec  46054  climexp  46056  climinf  46057  climsuse  46059  climneg  46061  divcnvg  46078  sumnnodd  46081  clim2f  46085  clim2f2  46119  fnlimfvre  46123  climleltrp  46125  climreclmpt  46133  climinf2mpt  46163  climinfmpt  46164  supcnvlimsup  46189  climuzlem  46192  climisp  46195  climrescn  46197  climxrrelem  46198  climxrre  46199  liminfvalxrmpt  46235  liminflbuz2  46264  cncfcompt  46332  dvsinax  46362  fperdvper  46368  dvcosax  46375  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnxpaek  46391  dvnmul  46392  dvmptfprodlem  46393  dvnprodlem1  46395  dvnprodlem2  46396  dvnprodlem3  46397  iblempty  46414  iblsplit  46415  itgcoscmulx  46418  itgsincmulx  46423  itgsubsticc  46425  sublevolico  46433  stoweidlem2  46451  stoweidlem17  46466  stoweidlem21  46470  stoweidlem32  46481  stoweidlem46  46495  stoweidlem55  46504  wallispi  46519  wallispi2lem1  46520  wallispi2lem2  46521  wallispi2  46522  stirlinglem3  46525  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem16  46572  fourierdlem18  46574  fourierdlem21  46577  fourierdlem22  46578  fourierdlem39  46595  fourierdlem53  46608  fourierdlem58  46613  fourierdlem59  46614  fourierdlem62  46617  fourierdlem73  46628  fourierdlem76  46631  fourierdlem81  46636  fourierdlem83  46638  fourierdlem93  46648  fourierdlem101  46656  fourierdlem103  46658  fourierdlem104  46659  fourierdlem111  46666  fourierdlem112  46667  fouriersw  46680  elaa2lem  46682  etransclem18  46701  etransclem32  46715  etransclem33  46716  etransclem46  46729  etransclem48  46731  rrxtopnfi  46736  rrxunitopnfi  46741  salincl  46773  sge0z  46824  sge0tsms  46829  sge0snmpt  46832  sge0sup  46840  sge0resplit  46855  sge0ss  46861  sge0isum  46876  sge0xp  46878  sge0xaddlem2  46883  sge0seq  46895  sge0reuzb  46897  meadjun  46911  meadjiun  46915  ismeannd  46916  meaiunlelem  46917  meaiininclem  46935  caragenunidm  46957  caragenuncllem  46961  omeiunltfirp  46968  carageniuncllem1  46970  caratheodorylem1  46975  0ome  46978  isomenndlem  46979  hoicvr  46997  hoicvrrex  47005  ovn0lem  47014  ovn0  47015  ovnsubaddlem1  47019  hoidmvval0  47036  hoidmvval0b  47039  hoidmv1lelem1  47040  hoidmv1le  47043  hoidmvlelem2  47045  hoidmvlelem3  47046  hoidmvlelem4  47047  hoidmvlelem5  47048  ovnhoilem1  47050  ovnhoilem2  47051  ovnhoi  47052  dmvon  47055  hspval  47058  ovnlecvr2  47059  hoiqssbllem2  47072  hspmbllem2  47076  hspmbl  47078  hoimbl  47080  ovnsubadd2lem  47094  ovolval4lem1  47098  ovnovollem1  47105  vonvolmbl  47110  vonvol2  47113  iccvonmbllem  47127  vonioolem2  47130  vonn0ioo2  47139  vonn0icc2  47141  smfpimltmpt  47195  issmfdmpt  47197  smfconst  47198  smfpimltxrmptf  47207  smflimlem2  47221  smflimlem3  47222  smflim  47226  smfpimgtmpt  47230  smfpimgtxrmptf  47233  smfsupmpt  47264  smfinfmpt  47268  smflimsuplem4  47272  fresfo  47511  fsetsnf  47514  fsetsnprcnex  47518  cfsetsnfsetf  47521  cfsetsnfsetfo  47523  3f1oss1  47538  f1cof1b  47540  funfocofob  47541  afveq1  47597  afveq2  47598  afvco2  47639  rspceaov  47660  faovcl  47663  afv2eq12d  47678  afv2eq1  47679  afv2eq2  47680  dfatcolem  47718  f1oresf1orab  47752  preimafvsnel  47854  preimafvelsetpreimafv  47863  fundcmpsurbijinjpreimafv  47882  fundcmpsurinjimaid  47886  fundcmpsurinjALT  47887  ichnreuop  47947  ichreuopeq  47948  prelspr  47961  sprsymrelf1lem  47966  sprsymrelfolem2  47968  prproropreud  47984  reuopreuprim  48001  fmtnofac2lem  48046  proththd  48092  requad01  48112  dfodd6  48128  nnsum3primesprm  48281  clnbgrvtxel  48320  isgrim  48373  grimid  48377  upgrimtrls  48397  isubgrgrim  48420  clnbgrgrim  48425  usgrgrtrirex  48441  stgrnbgr0  48455  isubgr3stgrlem6  48462  isgrlim  48473  uspgrlim  48483  grlimedgclnbgr  48486  grlimgrtri  48494  grilcbri2  48502  gpgedgiov  48556  gpg5gricstgr3  48581  gpg5grlim  48584  grlimedgnedg  48622  uspgrsprfo  48639  copissgrp  48659  copisnmnd  48660  isasslaw  48683  2zrngamgm  48736  cznrng  48752  rngcvalALTV  48756  rngcbasALTV  48757  rngchomfvalALTV  48758  rngccofvalALTV  48761  rngccoALTV  48762  rngccatidALTV  48763  rhmsubcALTV  48776  ringcvalALTV  48780  ringcbasALTV  48791  ringchomfvalALTV  48792  ringccofvalALTV  48795  ringccoALTV  48796  ringccatidALTV  48797  scmsuppss  48862  ply1mulgsum  48881  dflinc2  48901  lcoop  48902  lincvalsng  48907  lincvalpr  48909  lincvalsc0  48912  lcoc0  48913  lcoel0  48919  lincsum  48920  lincolss  48925  islininds  48937  lindslinindsimp1  48948  lindsrng01  48959  snlindsntorlem  48961  lincresunit3  48972  islindeps2  48974  lmod1lem3  48980  lmod1zr  48984  itcoval  49152  itcoval0  49153  itcoval1  49154  itcoval2  49155  itcoval3  49156  itcovalsuc  49158  itcovalsucov  49159  itcovalendof  49160  itcovalpclem2  49162  itcovalt2lem2  49167  ackvalsuc1mpt  49169  ackval1  49172  ackval2  49173  ackval3  49174  ackvalsucsucval  49179  affinecomb1  49193  rrx2plordisom  49214  lines  49222  line  49223  rrxline  49225  spheres  49237  line2xlem  49244  itsclc0yqsol  49255  itscnhlinecirc02p  49276  fmpod  49360  iscnrm3llem1  49439  iscnrm3llem2  49440  iscnrm3l  49441  glbsscl  49451  posjidm  49462  posmidm  49463  toslat  49472  ipolubdm  49477  ipoglbdm  49480  mreclat  49487  topclat  49488  iinfssc  49547  iinfsubc  49548  infsubc2  49551  iinfconstbas  49556  nelsubc3  49561  initc  49581  funchomf  49587  imaidfu2lem  49599  imaidfu  49600  imaidfu2  49601  cofidf2  49610  funcoppc4  49634  fthcomf  49647  idfth  49648  idsubc  49650  upciclem1  49656  upfval2  49667  upfval3  49668  isuplem  49669  oppcup3lem  49696  uobffth  49708  uobeqw  49709  uptr2  49711  initopropd  49733  termopropd  49734  dfswapf2  49751  swapfelvv  49753  swapf1vala  49756  swapf2fn  49758  swapf2  49764  tposcurf1cl  49786  tposcurf11  49787  tposcurf12  49788  tposcurf1  49789  tposcurf2  49790  tposcurf2val  49791  tposcurf2cl  49792  tposcurfcl  49793  fucoelvv  49810  fucofvalne  49815  fuco11  49816  fuco11cl  49817  fuco21  49826  fuco11b  49827  fuco11bALT  49828  fuco22natlem3  49834  fuco22natlem  49835  fuco23a  49842  fucofunc  49849  fucofunca  49850  fucolid  49851  fucorid  49852  postcofval  49854  precofval  49857  precofvalALT  49858  precoffunc  49862  prcofelvv  49870  reldmprcof1  49871  reldmprcof2  49872  prcoftposcurfuco  49873  prcoffunc  49875  prcoffunca  49876  fucoppcco  49899  fucoppccic  49903  oppfdiag1  49904  oppfdiag1a  49905  isthincd2lem1  49915  oppcthin  49928  oppcthinco  49929  subthinc  49933  fullthinc  49940  thincciso2  49945  indthinc  49952  prsthinc  49954  setcthin  49955  setc2othin  49956  setcsnterm  49980  setc1ocofval  49984  isinito2lem  49988  dfinito4  49991  idfudiag1  50015  arweuthinc  50019  diag1f1olem  50023  prstchomval  50049  prstcprs  50050  prstcthin  50051  prstchom2  50053  oduoppcciso  50056  postcpos  50057  postcposALT  50058  postc  50059  mndtccatid  50077  mndtcid  50079  oppgoppchom  50080  oppgoppcco  50081  oppgoppcid  50082  grptcmon  50083  grptcepi  50084  2arwcat  50090  lanfval  50103  ranfval  50104  lanpropd  50105  ranpropd  50106  rellan  50113  lanrcl5  50125  ranrcl5  50130  lanup  50131  ranup  50132  lmdfval  50139  cmdfval  50140  lmdpropd  50147  cmdpropd  50148  concom  50153  coccom  50154  islmd  50155  iscmd  50156  lmddu  50157  termolmd  50160  lmdran  50161  cmdlan  50162  aacllem  50291  amgmwlem  50292