Theorem eqeq1 2733

Description: Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Assertion

Ref	Expression
eqeq1	⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Proof of Theorem eqeq1

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq1d 2731	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqeq1i  2734  eqtr  2749  eqtr2  2750  iseqsetvlem  2792  eqsb1  2854  cbvexeqsetf  3462  cgsex4gOLD  3495  sbhypfOLD  3511  rexraleqim  3613  eqvincf  3616  pm13.183  3632  moeq  3678  mob  3688  euind  3695  reu2eqd  3707  reuind  3724  eqsbc1  3800  sbceqal  3815  csbhypf  3890  uniiunlem  4050  snjust  4588  elsng  4603  elprg  4612  reusngf  4638  rexreusng  4643  reuprg0  4666  rabrsn  4688  preq12bg  4817  intab  4942  uniintsn  4949  dfiun2g  4994  dfiin2g  4996  disji2  5091  disjprg  5103  unopab  5187  eusv1  5346  reusv2lem2  5354  reusv3  5360  opthg  5437  copsexgw  5450  copsexg  5451  propeqop  5467  euotd  5473  otiunsndisj  5480  elopabw  5486  solin  5573  elxpi  5660  opbrop  5736  relop  5814  ideqg  5815  dmopab2rex  5881  elrnmpt  5922  elrnmpt1  5924  elrnmptg  5925  restidsing  6024  somin1  6106  cnveqb  6169  reu3op  6265  reuop  6266  ordequn  6437  iotaval2  6479  funopg  6550  f0rn0  6745  fvelrnb  6921  fvmptg  6966  fndmin  7017  eldmrexrn  7063  foelrn  7079  foelrnf  7080  foco2  7081  fmptco  7101  funopsn  7120  funsndifnop  7123  fmptsng  7142  fmptsnd  7143  tpres  7175  eufnfv  7203  elabrex  7216  elabrexg  7217  abrexco  7218  f1veqaeq  7231  fpropnf1  7242  nf1const  7279  isosolem  7322  f1oiso  7326  eusvobj2  7379  oprabidw  7418  oprabid  7419  f1opr  7445  oprabv  7449  0mpo0  7472  elrnmpog  7524  elrnmpo  7525  elrnmpores  7527  ralrnmpo  7528  ov3  7552  ov6g  7553  ovelrn  7565  caovcang  7590  caovcan  7593  caofidlcan  7691  uniuni  7738  orduninsuc  7819  funcnvuni  7908  fiunlem  7920  fiun  7921  f1iun  7922  f1oweALT  7951  opiota  8038  eloprabi  8042  frxp  8105  funsssuppss  8169  dftpos4  8224  tz7.44-2  8375  tz7.44-3  8376  oev  8478  oalimcl  8524  omlimcl  8542  odi  8543  omeu  8549  oeeui  8566  nneob  8620  omopth  8626  eldifsucnn  8628  elqsg  8737  qsdisj  8767  qsel  8769  brecop  8783  eroveu  8785  erovlem  8786  elixpsn  8910  ixpsnf1o  8911  boxcutc  8914  2dom  9001  fundmen  9002  xpf1o  9103  nneneq  9170  fofinf1o  9283  elfi  9364  elfiun  9381  dffi3  9382  brwdom  9520  brwdom3  9535  unwdomg  9537  xpwdomg  9538  noinfep  9613  cantnfp1lem1  9631  cantnfp1lem3  9633  cantnflem1  9642  ssttrcl  9668  ttrclselem2  9679  scott0  9839  updjudhcoinrg  9886  updjud  9887  carden2a  9919  cardiun  9935  pm54.43lem  9953  alephval3  10063  dfac5lem3  10078  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2b  10084  kmlem9  10112  kmlem12  10115  cardcf  10205  cfeq0  10209  cfsuc  10210  cff1  10211  cflim2  10216  cfss  10218  isfin5  10252  fin1a2lem11  10363  fin1a2lem13  10365  brdom7disj  10484  brdom6disj  10485  canthp1lem2  10606  canthp1  10607  tskuni  10736  gruina  10771  genpv  10952  genpelv  10953  addsrmo  11026  mulsrmo  11027  ltsosr  11047  ltresr  11093  axcnre  11117  axpre-lttri  11118  ltordlem  11703  ltord1  11704  fimaxre3  12129  supaddc  12150  supadd  12151  supmul1  12152  supmullem1  12153  supmullem2  12154  supmul  12155  creur  12180  creui  12181  nn1m1nn  12207  elz  12531  nn0ind-raph  12634  xnegeq  13167  xmullem2  13225  xmulasslem  13245  fleqceilz  13816  fseqsupubi  13943  sqeqor  14181  nn0opth2  14237  hash1snb  14384  hash2prde  14435  prprrab  14438  hash2pwpr  14441  tpf1ofv1  14462  tpf1ofv2  14463  tpfo  14465  fi1uzind  14472  wrd2ind  14688  cshfn  14755  cshf1  14775  2cshwcshw  14791  scshwfzeqfzo  14792  pfx2  14913  s3iunsndisj  14934  relexpsucnnr  14991  relexprelg  15004  rtrclreclem3  15026  shftfval  15036  sgnval  15054  01sqrexlem6  15213  reusq0  15431  summo  15683  fsum  15686  telfsumo  15768  infcvgaux1i  15823  infcvgaux2i  15824  mertenslem1  15850  mertenslem2  15851  mertens  15852  prodmo  15902  fprod  15907  ruclem12  16209  mod2eq1n2dvds  16317  divalg  16373  ndvdssub  16379  sadcp1  16425  smupp1  16450  gcdval  16466  bezoutlem1  16509  bezoutlem3  16511  bezoutlem4  16512  bezout  16513  lcmval  16562  coprmgcdb  16619  coprmdvds1  16622  divgcdcoprmex  16636  dvdsprime  16657  nprm  16658  dvdsprm  16673  coprm  16681  qnumval  16707  qdenval  16708  m1dvdsndvds  16769  reumodprminv  16775  pcval  16815  pceu  16817  pczpre  16818  pcdiv  16823  4sqlem2  16920  4sqlem4  16923  4sqlem12  16927  4sq  16935  vdwapval  16944  vdwapun  16945  vdwlem6  16957  cshwrepswhash1  17073  acsfn  17620  initoid  17963  termoid  17964  cat1lem  18058  posi  18278  gsumval2a  18612  smndex2dnrinv  18842  mgm2nsgrplem2  18846  mgm2nsgrplem3  18847  sgrp2nmndlem5  18856  mgmnsgrpex  18858  sgrpnmndex  18859  cyccom  19135  ghmf1  19178  conjnmzb  19185  orbsta  19245  symgextfv  19348  symgextfo  19352  symgfixfo  19369  pmtrprfval  19417  pmtrprfvalrn  19418  psgneu  19436  psgnval  19437  psgnvali  19438  psgnvalii  19439  odfval  19462  odval  19464  dfod2  19494  submod  19499  isslw  19538  sylow2alem1  19547  sylow3lem2  19558  lsmelvalm  19581  lsmdisj2  19612  efgrelexlemb  19680  frgpup3lem  19707  cyggeninv  19813  gsumval3eu  19834  gsumval3lem2  19836  gsummpt1n0  19895  nn0gsumfz  19914  dprddisj2  19971  dpjrid  19994  pgpfac1lem3  20009  rrgeq0i  20608  domneq0  20617  domnlcanb  20629  domnrcanb  20631  abveq0  20727  abvtrivd  20741  lss1d  20869  lspsn  20908  ellspsn  20909  lspprel  21001  prmirredlem  21382  znf1o  21461  znfld  21470  znunit  21473  cygznlem3  21479  psgndif  21511  ipeq0  21547  obsip  21630  frlmphl  21690  uvcvval  21695  ellspd  21711  psrlidm  21871  psrridm  21872  psrascl  21888  mvrval2  21892  mvrf1  21895  mplmonmul  21943  evlslem3  21987  mhpsclcl  22034  psdmplcl  22049  psdmul  22053  psdmvr  22056  coe1tm  22159  coe1tmfv2  22161  cply1coe0  22188  cply1coe0bi  22189  gsummoncoe1  22195  mamufacex  22283  mat1comp  22327  mat1dimelbas  22358  mat1dimid  22361  scmatel  22392  scmateALT  22399  mavmulsolcl  22438  marrepeval  22450  marepveval  22455  mdetunilem8  22506  maducoeval2  22527  madugsum  22530  minmar1eval  22536  symgmatr01lem  22540  symgmatr01  22541  gsummatr01lem3  22544  gsummatr01lem4  22545  gsummatr01  22546  m2cpm  22628  m2cpminvid2lem  22641  decpmatid  22657  monmatcollpw  22666  pmatcollpw3fi1lem1  22673  mp2pm2mplem4  22696  fvmptnn04ifc  22739  chfacffsupp  22743  chfacfscmul0  22745  chfacfscmulgsum  22747  chfacfpmmul0  22749  chfacfpmmulgsum  22751  cpmadumatpoly  22770  cayleyhamilton  22777  cayleyhamiltonALT  22778  istopon  22799  toponsspwpw  22809  fctop  22891  cctop  22893  ppttop  22894  pptbas  22895  epttop  22896  t0sep  23211  t1sep2  23256  cmpsublem  23286  cmpsub  23287  unisngl  23414  txuni2  23452  elpt  23459  ptbasfi  23468  xkoopn  23476  ptpjopn  23499  ptclsg  23502  dfac14lem  23504  ptcnp  23509  ptrescn  23526  tx1stc  23537  qtopeu  23603  kqt0lem  23623  isr0  23624  hauspwpwf1  23874  xmeteq0  24226  imasf1oxmet  24263  comet  24401  stdbdxmet  24403  met2ndci  24410  prdsxmslem2  24417  nrmmetd  24462  tngngp  24542  tngngp3  24544  xrsxmet  24698  iccpnfcnv  24842  iccpnfhmeo  24843  cnheibor  24854  elovolm  25376  ovolgelb  25381  ovolicc1  25417  ovolicc  25424  ioorval  25475  uniioombllem6  25489  dyadmax  25499  dyadmbl  25501  i1fadd  25596  i1fmul  25597  itg1addlem3  25599  i1fmulc  25604  itg2l  25630  itg2leub  25635  limcmpt  25784  limcco  25794  dvcobr  25849  dvcobrOLD  25850  deg1ldg  25997  ig1pval  26081  elply  26100  elply2  26101  coeval  26128  coe1termlem  26163  coe1term  26164  quotval  26200  plydivlem4  26204  plydivex  26205  vieta1  26220  aannenlem2  26237  aalioulem2  26241  abelthlem9  26350  logtayllem  26568  logtayl  26569  isosctrlem2  26729  leibpilem2  26851  rlimcnp2  26876  efrlim  26879  efrlimOLD  26880  mpodvdsmulf1o  27104  dvdsmulf1o  27106  perfectlem2  27141  lgsfval  27213  lgsval2lem  27218  lgsqrmodndvds  27264  lgsdchrval  27265  gausslemma2dlem0i  27275  2lgslem1b  27303  2lgslem3  27315  2sqlem2  27329  2sqlem8  27337  2sqlem9  27338  2sqlem11  27340  addsq2reu  27351  dchrisum0flblem1  27419  padicval  27528  padicabv  27541  ostth1  27544  sltval2  27568  sltintdifex  27573  sltres  27574  nolt02o  27607  madef  27764  addsval2  27870  addsproplem2  27877  addsproplem4  27879  addsproplem5  27880  addsproplem6  27881  addsprop  27883  addscut  27885  sleadd1  27896  addsuniflem  27908  addsunif  27909  addsasslem1  27910  addsasslem2  27911  addsbdaylem  27923  negsprop  27941  negsid  27947  mulsval2lem  28013  mulsproplem9  28027  mulsproplem12  28030  mulsprop  28033  ssltmul1  28050  ssltmul2  28051  mulsuniflem  28052  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  mulsunif2  28073  precsexlemcbv  28108  precsexlem9  28117  precsexlem11  28119  n0s0suc  28234  onsfi  28247  n0s0m1  28252  nn1m1nns  28263  eucliddivs  28265  n0seo  28307  zseo  28308  expsval  28311  elzs12  28337  zs12ge0  28342  recut  28347  0reno  28348  renegscl  28349  readdscl  28350  remulscllem1  28351  remulscl  28353  axtgcgrid  28390  axtgbtwnid  28393  islmib  28714  inaghl  28772  axpaschlem  28867  axlowdimlem15  28883  axlowdim  28888  upgredg2vtx  29068  edglnl  29070  umgredgnlp  29074  usgredg2vtxeuALT  29149  uspgredg2v  29151  ushgredgedgloop  29158  nbusgredgeu  29293  cusgrfilem2  29384  cusgrfi  29386  vtxdushgrfvedg  29418  1loopgrvd2  29431  rusgr1vtxlem  29515  wlkeq  29562  wlkp1lem8  29608  upgrwlkdvdelem  29666  crctcshwlkn0lem6  29745  wlknwwlksnbij  29818  rusgrnumwwlkl1  29898  clwlkclwwlklem2a1  29921  clwwlknscsh  29991  eleclclwwlkn  30005  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  clwwlknon1sn  30029  frgr3vlem1  30202  3vfriswmgrlem  30206  frgrncvvdeqlem3  30230  wlkl0  30296  frgrreggt1  30322  nvz  30598  nmosetn0  30694  nmoolb  30700  nmoubi  30701  nmlno0lem  30722  nmlno0i  30723  hvsubeq0  30997  hvaddcan  30999  normsub0  31065  norm1exi  31179  pjhval  31326  omlsii  31332  omlsi  31333  pjoml  31365  h1de2ci  31485  spansneleq  31499  h1datomi  31510  h1datom  31511  spansncv  31582  5oalem6  31588  pj11  31643  nmopsetn0  31794  nmfnsetn0  31807  nmoplb  31836  nmopub  31837  nmfnlb  31853  nmfnleub  31854  nmlnop0iALT  31924  nmlnop0  31927  lnopeq  31938  nmopun  31943  nmcexi  31955  branmfn  32034  pjnmopi  32077  pj3i  32137  atss  32275  atom1d  32282  chirred  32324  cdj3lem2  32364  eqelbid  32404  elabreximd  32439  disjxpin  32517  disjunsn  32523  br8d  32538  fmptcof2  32581  sgn3da  32759  sgnmul  32760  sgnnbi  32763  sgnpbi  32764  sgn0bi  32765  psgnfzto1stlem  33057  sgnsval  33118  elrgspnlem2  33194  elrgspnlem3  33195  domnlcanOLD  33230  linds2eq  33352  elrspunsn  33400  mxidlmax  33436  1arithidomlem1  33506  1arithidom  33508  1arithufdlem1  33515  1arithufdlem2  33516  1arithufdlem3  33517  1arithufdlem4  33518  1arithufd  33519  dfufd2  33521  ply1dg1rt  33548  lbsdiflsp0  33622  fedgmullem1  33625  fedgmullem2  33626  rtelextdg2lem  33716  constrsuc  33728  constrcbvlem  33745  2sqr3minply  33770  madjusmdetlem2  33818  madjusmdet  33821  zarclssn  33863  xrge0iifcnv  33923  xrge0iifcv  33924  xrge0iifhom  33927  xrge0tmd  33935  xrge0tmdALT  33936  esumc  34041  plymulx0  34538  signspval  34543  tgoldbachgt  34654  bnj1468  34836  f1resfz0f1d  35101  acycgrcycl  35134  sconnpi1  35226  cvmlift3lem2  35307  satfv0  35345  satfv1  35350  satfbrsuc  35353  satfrnmapom  35357  satfv0fun  35358  satf0op  35364  sat1el2xp  35366  fmlafvel  35372  fmla1  35374  isfmlasuc  35375  fmlaomn0  35377  gonan0  35379  goaln0  35380  gonar  35382  goalr  35384  fmla0disjsuc  35385  fmlasucdisj  35386  satffunlem1lem1  35389  satffunlem2lem1  35391  dmopab3rexdif  35392  satfv0fvfmla0  35400  sategoelfvb  35406  ex-sategoelel  35408  satfv1fvfmla1  35410  2goelgoanfmla1  35411  ex-sategoelelomsuc  35413  ex-sategoelel12  35414  prv1n  35418  ellcsrspsn  35628  r1peuqusdeg1  35630  br8  35743  br6  35744  br4  35745  rdgprc0  35781  dfrdg2  35783  dfbigcup2  35887  elsingles  35906  dfiota3  35911  brimageg  35915  brdomaing  35923  brrangeg  35924  dfrdg4  35939  elaltxp  35963  funtransport  36019  fvtransport  36020  brsegle  36096  funray  36128  fvray  36129  funline  36130  fvline  36132  ellines  36140  linethru  36141  rankeq1o  36159  subtr  36302  subtr2  36303  nn0prpw  36311  bj-elabd2ALT  36913  bj-gabss  36923  bj-imafv  37239  topdifinffinlem  37335  topdifinffin  37336  topdifinfeq  37338  finxpreclem2  37378  finxpreclem3  37381  fvineqsnf1  37398  fvineqsneu  37399  wl-ax12v2cl  37494  wl-issetft  37570  fin2so  37601  ptrest  37613  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem31  37645  poimirlem32  37646  heicant  37649  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  ftc1anc  37695  unirep  37708  sdclem2  37736  sdclem1  37737  sdc  37738  fdc  37739  isbnd  37774  heibor1lem  37803  heiborlem4  37808  heiborlem6  37810  heiborlem10  37814  ismgmOLD  37844  maxidlmax  38037  prnc  38061  isfldidl  38062  dmnnzd  38069  disjressuc2  38374  qsdisjALTV  38606  eqvrelqsel  38607  riotasvd  38949  lshpdisj  38980  lsat0cv  39026  lcvexchlem4  39030  lcvexchlem5  39031  lshpkrlem1  39103  lshpkrlem2  39104  lshpkrlem3  39105  lshpkrcl  39109  islshpkrN  39113  atnle  39310  glbconxN  39372  isline  39733  ispointN  39736  pmapglbx  39763  ispsubcl2N  39941  lhp2atnle  40027  cdleme43fsv1snlem  40414  cdleme40v  40463  cdlemkid5  40929  cdlemkid  40930  dvhb1dimN  40980  dib1dim  41159  dicopelval  41171  dicelval1sta  41181  diclspsn  41188  dihvalcqpre  41229  dihglblem2aN  41287  dihglblem2N  41288  dih1dimatlem  41323  dihpN  41330  dochfl1  41470  lcfl7N  41495  lcf1o  41545  hvmapvalvalN  41755  hdmapval2lem  41825  aks6d1c1  42104  aks6d1c4  42112  sticksstones10  42143  sticksstones12a  42145  aks6d1c7  42172  sn-iotalem  42209  f1o2d2  42221  fiabv  42524  evlsbagval  42554  selvvvval  42573  fsuppind  42578  absnw  42666  elrfi  42682  nacsfg  42693  mzpcompact2lem  42739  eldioph2b  42751  eldioph3  42754  eldiophss  42762  diophrex  42763  elnn0rabdioph  42791  rencldnfilem  42808  elpell1qr  42835  elpell14qr  42837  elpell1234qr  42839  jm2.27  42997  rmydioph  43003  expdiophlem2  43011  wepwsolem  43031  aomclem6  43048  lnr2i  43105  lpirlnr  43106  hbtlem2  43113  hbtlem4  43115  hbtlem5  43117  rngunsnply  43158  flcidc  43159  onsucelab  43252  limnsuc  43254  nnoeomeqom  43301  cantnfresb  43313  tfsconcatfv2  43329  tfsconcatb0  43333  oaun3lem1  43363  oadif1lem  43368  oadif1  43369  clcnvlem  43612  brtrclfv2  43716  frege55lem1c  43905  frege104  43956  clsk1indlem0  44030  clsk1indlem2  44031  clsk1indlem3  44032  clsk1indlem4  44033  clsk1indlem1  44034  pm13.192  44399  equncomVD  44857  csbingVD  44873  csbsngVD  44882  csbfv12gALTVD  44888  relopabVD  44890  refsum2cnlem1  45031  elrnmptf  45175  upbdrech  45303  ssfiunibd  45307  iccshift  45516  iooshift  45520  fsumf1of  45572  limcperiod  45626  climinf2mpt  45712  climinfmpt  45713  cncfshiftioo  45890  itgiccshift  45978  itgperiod  45979  stoweidlem46  46044  fourierdlem29  46134  fourierdlem37  46142  fourierdlem48  46152  fourierdlem51  46155  fourierdlem54  46158  fourierdlem62  46166  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem92  46196  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem103  46207  fourierdlem104  46208  fourierdlem105  46209  fourierdlem108  46212  fourierdlem110  46214  fourierdlem112  46216  etransclem1  46233  etransclem5  46237  etransclem17  46249  etransclem32  46264  etransclem41  46273  sge0f1o  46380  sge0resplit  46404  sge0fodjrnlem  46414  nnfoctbdjlem  46453  nnfoctbdj  46454  ovnval  46539  ovnlecvr  46556  ovnpnfelsup  46557  ovn0lem  46563  hoidmvval  46575  hoidmvlelem1  46593  ovnhoilem1  46599  ovnhoi  46601  ovnlecvr2  46608  hoidifhspval3  46617  hspmbllem2  46625  hoimbl  46629  ovnsubadd2  46644  ovolval5lem2  46651  ovolval5lem3  46652  ovolval5  46653  ovnovol  46657  sinnpoly  46892  fsetsnf  47052  fsetsnfo  47054  fcoresf1  47070  aiotaval  47096  euoreqb  47110  afv0fv0  47150  afvfv0bi  47153  afvelrnb  47164  afvelrnb0  47165  afv20defat  47233  otiunsndisjX  47280  fun2dmnopgexmpl  47285  2ffzoeq  47328  modmkpkne  47362  elsetpreimafvb  47385  imasetpreimafvbijlemfo  47406  fargshiftf1  47442  fargshiftfo  47443  ichnreuop  47473  ichreuopeq  47474  elsprel  47476  spr0nelg  47477  sprel  47485  prelspr  47487  sprsymrelf1lem  47492  sprsymrelfolem2  47494  paireqne  47512  prprelb  47517  prprelprb  47518  reupr  47523  reuopreuprim  47527  fmtnoprmfac1lem  47565  fmtnofac2  47570  m1expevenALTV  47648  odd2np1ALTV  47675  opoeALTV  47684  opeoALTV  47685  perfectALTVlem2  47723  isgbe  47752  isgbow  47753  isgbo  47754  sbgoldbalt  47782  sgoldbeven3prm  47784  mogoldbb  47786  nnsum3primesgbe  47793  nnsum3primesle9  47795  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  vopnbgrel  47854  dfclnbgr6  47856  dfnbgr6  47857  isuspgrim0  47894  isuspgrimlem  47895  clnbgrgrim  47934  usgrgrtrirex  47949  stgredgel  47956  stgrusgra  47958  stgr1  47960  grlimgrtri  47995  gpgiedgdmel  48040  gpgedgel  48041  gpgprismgr4cycllem10  48094  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem4  48109  pgnbgreunbgr  48115  uspgrsprf1  48135  uspgrsprfo  48136  0nodd  48158  1odd  48159  2nodd  48160  0even  48225  1neven  48226  2even  48227  2zlidl  48228  2zrngamgm  48233  2zrngagrp  48237  2zrngmmgm  48240  2zrngnmrid  48244  suppmptcfin  48364  lcoval  48401  linc0scn0  48412  linc1  48414  el0ldep  48455  snlindsntor  48460  blenval  48560  nn0sumshdiglemB  48609  itcoval1  48652  mo0  48802  eloprab1st2nd  48856  oppcmndclem  49006  sectpropdlem  49025  invpropdlem  49027  isopropdlem  49029  upciclem1  49155  oppcup3lem  49195  isthincd2lem1  49414  termcbasmo  49472  isinito2lem  49487  arweuthinc  49518  arweutermc  49519  discsntermlem  49559  basrestermcfolem  49560