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  3459  cgsex4gOLD  3492  sbhypfOLD  3508  rexraleqim  3610  eqvincf  3613  pm13.183  3629  moeq  3675  mob  3685  euind  3692  reu2eqd  3704  reuind  3721  eqsbc1  3797  sbceqal  3812  csbhypf  3887  uniiunlem  4046  snjust  4584  elsng  4599  elprg  4608  reusngf  4634  rexreusng  4639  reuprg0  4662  rabrsn  4684  preq12bg  4813  intab  4938  uniintsn  4945  dfiun2g  4990  dfiin2g  4991  disji2  5086  disjprg  5098  unopab  5182  eusv1  5341  reusv2lem2  5349  reusv3  5355  opthg  5432  copsexgw  5445  copsexg  5446  propeqop  5462  euotd  5468  otiunsndisj  5475  elopabw  5481  solin  5566  elxpi  5653  opbrop  5728  relop  5804  ideqg  5805  dmopab2rex  5871  elrnmpt  5911  elrnmpt1  5913  elrnmptg  5914  restidsing  6013  somin1  6094  cnveqb  6157  reu3op  6253  reuop  6254  ordequn  6425  iotaval2  6467  funopg  6534  f0rn0  6727  fvelrnb  6903  fvmptg  6948  fndmin  6999  eldmrexrn  7045  foelrn  7061  foelrnf  7062  foco2  7063  fmptco  7083  funopsn  7102  funsndifnop  7105  fmptsng  7124  fmptsnd  7125  tpres  7157  eufnfv  7185  elabrex  7198  elabrexg  7199  abrexco  7200  f1veqaeq  7213  fpropnf1  7224  nf1const  7261  isosolem  7304  f1oiso  7308  eusvobj2  7361  oprabidw  7400  oprabid  7401  f1opr  7425  oprabv  7429  0mpo0  7452  elrnmpog  7504  elrnmpo  7505  elrnmpores  7507  ralrnmpo  7508  ov3  7532  ov6g  7533  ovelrn  7545  caovcang  7570  caovcan  7573  caofidlcan  7671  uniuni  7718  orduninsuc  7799  funcnvuni  7888  fiunlem  7900  fiun  7901  f1iun  7902  f1oweALT  7930  opiota  8017  eloprabi  8021  frxp  8082  funsssuppss  8146  dftpos4  8201  tz7.44-2  8352  tz7.44-3  8353  oev  8455  oalimcl  8501  omlimcl  8519  odi  8520  omeu  8526  oeeui  8543  nneob  8597  omopth  8603  eldifsucnn  8605  elqsg  8714  qsdisj  8744  qsel  8746  brecop  8760  eroveu  8762  erovlem  8763  elixpsn  8887  ixpsnf1o  8888  boxcutc  8891  2dom  8978  fundmen  8979  xpf1o  9080  nneneq  9147  fofinf1o  9259  elfi  9340  elfiun  9357  dffi3  9358  brwdom  9496  brwdom3  9511  unwdomg  9513  xpwdomg  9514  noinfep  9589  cantnfp1lem1  9607  cantnfp1lem3  9609  cantnflem1  9618  ssttrcl  9644  ttrclselem2  9655  scott0  9815  updjudhcoinrg  9862  updjud  9863  carden2a  9895  cardiun  9911  pm54.43lem  9929  alephval3  10039  dfac5lem3  10054  dfac5lem4  10055  dfac5lem4OLD  10057  dfac2b  10060  kmlem9  10088  kmlem12  10091  cardcf  10181  cfeq0  10185  cfsuc  10186  cff1  10187  cflim2  10192  cfss  10194  isfin5  10228  fin1a2lem11  10339  fin1a2lem13  10341  brdom7disj  10460  brdom6disj  10461  canthp1lem2  10582  canthp1  10583  tskuni  10712  gruina  10747  genpv  10928  genpelv  10929  addsrmo  11002  mulsrmo  11003  ltsosr  11023  ltresr  11069  axcnre  11093  axpre-lttri  11094  ltordlem  11679  ltord1  11680  fimaxre3  12105  supaddc  12126  supadd  12127  supmul1  12128  supmullem1  12129  supmullem2  12130  supmul  12131  creur  12156  creui  12157  nn1m1nn  12183  elz  12507  nn0ind-raph  12610  xnegeq  13143  xmullem2  13201  xmulasslem  13221  fleqceilz  13792  fseqsupubi  13919  sqeqor  14157  nn0opth2  14213  hash1snb  14360  hash2prde  14411  prprrab  14414  hash2pwpr  14417  tpf1ofv1  14438  tpf1ofv2  14439  tpfo  14441  fi1uzind  14448  wrd2ind  14664  cshfn  14731  cshf1  14751  2cshwcshw  14767  scshwfzeqfzo  14768  pfx2  14889  s3iunsndisj  14910  relexpsucnnr  14967  relexprelg  14980  rtrclreclem3  15002  shftfval  15012  sgnval  15030  01sqrexlem6  15189  reusq0  15407  summo  15659  fsum  15662  telfsumo  15744  infcvgaux1i  15799  infcvgaux2i  15800  mertenslem1  15826  mertenslem2  15827  mertens  15828  prodmo  15878  fprod  15883  ruclem12  16185  mod2eq1n2dvds  16293  divalg  16349  ndvdssub  16355  sadcp1  16401  smupp1  16426  gcdval  16442  bezoutlem1  16485  bezoutlem3  16487  bezoutlem4  16488  bezout  16489  lcmval  16538  coprmgcdb  16595  coprmdvds1  16598  divgcdcoprmex  16612  dvdsprime  16633  nprm  16634  dvdsprm  16649  coprm  16657  qnumval  16683  qdenval  16684  m1dvdsndvds  16745  reumodprminv  16751  pcval  16791  pceu  16793  pczpre  16794  pcdiv  16799  4sqlem2  16896  4sqlem4  16899  4sqlem12  16903  4sq  16911  vdwapval  16920  vdwapun  16921  vdwlem6  16933  cshwrepswhash1  17049  acsfn  17596  initoid  17939  termoid  17940  cat1lem  18034  posi  18254  gsumval2a  18588  smndex2dnrinv  18818  mgm2nsgrplem2  18822  mgm2nsgrplem3  18823  sgrp2nmndlem5  18832  mgmnsgrpex  18834  sgrpnmndex  18835  cyccom  19111  ghmf1  19154  conjnmzb  19161  orbsta  19221  symgextfv  19324  symgextfo  19328  symgfixfo  19345  pmtrprfval  19393  pmtrprfvalrn  19394  psgneu  19412  psgnval  19413  psgnvali  19414  psgnvalii  19415  odfval  19438  odval  19440  dfod2  19470  submod  19475  isslw  19514  sylow2alem1  19523  sylow3lem2  19534  lsmelvalm  19557  lsmdisj2  19588  efgrelexlemb  19656  frgpup3lem  19683  cyggeninv  19789  gsumval3eu  19810  gsumval3lem2  19812  gsummpt1n0  19871  nn0gsumfz  19890  dprddisj2  19947  dpjrid  19970  pgpfac1lem3  19985  rrgeq0i  20584  domneq0  20593  domnlcanb  20605  domnrcanb  20607  abveq0  20703  abvtrivd  20717  lss1d  20845  lspsn  20884  ellspsn  20885  lspprel  20977  prmirredlem  21358  znf1o  21437  znfld  21446  znunit  21449  cygznlem3  21455  psgndif  21487  ipeq0  21523  obsip  21606  frlmphl  21666  uvcvval  21671  ellspd  21687  psrlidm  21847  psrridm  21848  psrascl  21864  mvrval2  21868  mvrf1  21871  mplmonmul  21919  evlslem3  21963  mhpsclcl  22010  psdmplcl  22025  psdmul  22029  psdmvr  22032  coe1tm  22135  coe1tmfv2  22137  cply1coe0  22164  cply1coe0bi  22165  gsummoncoe1  22171  mamufacex  22259  mat1comp  22303  mat1dimelbas  22334  mat1dimid  22337  scmatel  22368  scmateALT  22375  mavmulsolcl  22414  marrepeval  22426  marepveval  22431  mdetunilem8  22482  maducoeval2  22503  madugsum  22506  minmar1eval  22512  symgmatr01lem  22516  symgmatr01  22517  gsummatr01lem3  22520  gsummatr01lem4  22521  gsummatr01  22522  m2cpm  22604  m2cpminvid2lem  22617  decpmatid  22633  monmatcollpw  22642  pmatcollpw3fi1lem1  22649  mp2pm2mplem4  22672  fvmptnn04ifc  22715  chfacffsupp  22719  chfacfscmul0  22721  chfacfscmulgsum  22723  chfacfpmmul0  22725  chfacfpmmulgsum  22727  cpmadumatpoly  22746  cayleyhamilton  22753  cayleyhamiltonALT  22754  istopon  22775  toponsspwpw  22785  fctop  22867  cctop  22869  ppttop  22870  pptbas  22871  epttop  22872  t0sep  23187  t1sep2  23232  cmpsublem  23262  cmpsub  23263  unisngl  23390  txuni2  23428  elpt  23435  ptbasfi  23444  xkoopn  23452  ptpjopn  23475  ptclsg  23478  dfac14lem  23480  ptcnp  23485  ptrescn  23502  tx1stc  23513  qtopeu  23579  kqt0lem  23599  isr0  23600  hauspwpwf1  23850  xmeteq0  24202  imasf1oxmet  24239  comet  24377  stdbdxmet  24379  met2ndci  24386  prdsxmslem2  24393  nrmmetd  24438  tngngp  24518  tngngp3  24520  xrsxmet  24674  iccpnfcnv  24818  iccpnfhmeo  24819  cnheibor  24830  elovolm  25352  ovolgelb  25357  ovolicc1  25393  ovolicc  25400  ioorval  25451  uniioombllem6  25465  dyadmax  25475  dyadmbl  25477  i1fadd  25572  i1fmul  25573  itg1addlem3  25575  i1fmulc  25580  itg2l  25606  itg2leub  25611  limcmpt  25760  limcco  25770  dvcobr  25825  dvcobrOLD  25826  deg1ldg  25973  ig1pval  26057  elply  26076  elply2  26077  coeval  26104  coe1termlem  26139  coe1term  26140  quotval  26176  plydivlem4  26180  plydivex  26181  vieta1  26196  aannenlem2  26213  aalioulem2  26217  abelthlem9  26326  logtayllem  26544  logtayl  26545  isosctrlem2  26705  leibpilem2  26827  rlimcnp2  26852  efrlim  26855  efrlimOLD  26856  mpodvdsmulf1o  27080  dvdsmulf1o  27082  perfectlem2  27117  lgsfval  27189  lgsval2lem  27194  lgsqrmodndvds  27240  lgsdchrval  27241  gausslemma2dlem0i  27251  2lgslem1b  27279  2lgslem3  27291  2sqlem2  27305  2sqlem8  27313  2sqlem9  27314  2sqlem11  27316  addsq2reu  27327  dchrisum0flblem1  27395  padicval  27504  padicabv  27517  ostth1  27520  sltval2  27544  sltintdifex  27549  sltres  27550  nolt02o  27583  madef  27740  addsval2  27846  addsproplem2  27853  addsproplem4  27855  addsproplem5  27856  addsproplem6  27857  addsprop  27859  addscut  27861  sleadd1  27872  addsuniflem  27884  addsunif  27885  addsasslem1  27886  addsasslem2  27887  addsbdaylem  27899  negsprop  27917  negsid  27923  mulsval2lem  27989  mulsproplem9  28003  mulsproplem12  28006  mulsprop  28009  ssltmul1  28026  ssltmul2  28027  mulsuniflem  28028  addsdilem1  28030  addsdilem2  28031  mulsasslem1  28042  mulsasslem2  28043  mulsunif2  28049  precsexlemcbv  28084  precsexlem9  28093  precsexlem11  28095  n0s0suc  28210  onsfi  28223  n0s0m1  28228  nn1m1nns  28239  eucliddivs  28241  n0seo  28283  zseo  28284  expsval  28287  elzs12  28313  zs12ge0  28318  recut  28323  0reno  28324  renegscl  28325  readdscl  28326  remulscllem1  28327  remulscl  28329  axtgcgrid  28366  axtgbtwnid  28369  islmib  28690  inaghl  28748  axpaschlem  28843  axlowdimlem15  28859  axlowdim  28864  upgredg2vtx  29044  edglnl  29046  umgredgnlp  29050  usgredg2vtxeuALT  29125  uspgredg2v  29127  ushgredgedgloop  29134  nbusgredgeu  29269  cusgrfilem2  29360  cusgrfi  29362  vtxdushgrfvedg  29394  1loopgrvd2  29407  rusgr1vtxlem  29491  wlkeq  29537  wlkp1lem8  29582  upgrwlkdvdelem  29639  crctcshwlkn0lem6  29718  wlknwwlksnbij  29791  rusgrnumwwlkl1  29871  clwlkclwwlklem2a1  29894  clwwlknscsh  29964  eleclclwwlkn  29978  hashecclwwlkn1  29979  umgrhashecclwwlk  29980  clwwlknon1sn  30002  frgr3vlem1  30175  3vfriswmgrlem  30179  frgrncvvdeqlem3  30203  wlkl0  30269  frgrreggt1  30295  nvz  30571  nmosetn0  30667  nmoolb  30673  nmoubi  30674  nmlno0lem  30695  nmlno0i  30696  hvsubeq0  30970  hvaddcan  30972  normsub0  31038  norm1exi  31152  pjhval  31299  omlsii  31305  omlsi  31306  pjoml  31338  h1de2ci  31458  spansneleq  31472  h1datomi  31483  h1datom  31484  spansncv  31555  5oalem6  31561  pj11  31616  nmopsetn0  31767  nmfnsetn0  31780  nmoplb  31809  nmopub  31810  nmfnlb  31826  nmfnleub  31827  nmlnop0iALT  31897  nmlnop0  31900  lnopeq  31911  nmopun  31916  nmcexi  31928  branmfn  32007  pjnmopi  32050  pj3i  32110  atss  32248  atom1d  32255  chirred  32297  cdj3lem2  32337  eqelbid  32377  elabreximd  32412  disjxpin  32490  disjunsn  32496  br8d  32511  fmptcof2  32554  sgn3da  32732  sgnmul  32733  sgnnbi  32736  sgnpbi  32737  sgn0bi  32738  psgnfzto1stlem  33030  sgnsval  33091  elrgspnlem2  33167  elrgspnlem3  33168  domnlcanOLD  33203  linds2eq  33325  elrspunsn  33373  mxidlmax  33409  1arithidomlem1  33479  1arithidom  33481  1arithufdlem1  33488  1arithufdlem2  33489  1arithufdlem3  33490  1arithufdlem4  33491  1arithufd  33492  dfufd2  33494  ply1dg1rt  33521  lbsdiflsp0  33595  fedgmullem1  33598  fedgmullem2  33599  rtelextdg2lem  33689  constrsuc  33701  constrcbvlem  33718  2sqr3minply  33743  madjusmdetlem2  33791  madjusmdet  33794  zarclssn  33836  xrge0iifcnv  33896  xrge0iifcv  33897  xrge0iifhom  33900  xrge0tmd  33908  xrge0tmdALT  33909  esumc  34014  plymulx0  34511  signspval  34516  tgoldbachgt  34627  bnj1468  34809  f1resfz0f1d  35074  acycgrcycl  35107  sconnpi1  35199  cvmlift3lem2  35280  satfv0  35318  satfv1  35323  satfbrsuc  35326  satfrnmapom  35330  satfv0fun  35331  satf0op  35337  sat1el2xp  35339  fmlafvel  35345  fmla1  35347  isfmlasuc  35348  fmlaomn0  35350  gonan0  35352  goaln0  35353  gonar  35355  goalr  35357  fmla0disjsuc  35358  fmlasucdisj  35359  satffunlem1lem1  35362  satffunlem2lem1  35364  dmopab3rexdif  35365  satfv0fvfmla0  35373  sategoelfvb  35379  ex-sategoelel  35381  satfv1fvfmla1  35383  2goelgoanfmla1  35384  ex-sategoelelomsuc  35386  ex-sategoelel12  35387  prv1n  35391  ellcsrspsn  35601  r1peuqusdeg1  35603  br8  35716  br6  35717  br4  35718  rdgprc0  35754  dfrdg2  35756  dfbigcup2  35860  elsingles  35879  dfiota3  35884  brimageg  35888  brdomaing  35896  brrangeg  35897  dfrdg4  35912  elaltxp  35936  funtransport  35992  fvtransport  35993  brsegle  36069  funray  36101  fvray  36102  funline  36103  fvline  36105  ellines  36113  linethru  36114  rankeq1o  36132  subtr  36275  subtr2  36276  nn0prpw  36284  bj-elabd2ALT  36886  bj-gabss  36896  bj-imafv  37212  topdifinffinlem  37308  topdifinffin  37309  topdifinfeq  37311  finxpreclem2  37351  finxpreclem3  37354  fvineqsnf1  37371  fvineqsneu  37372  wl-ax12v2cl  37467  wl-issetft  37543  fin2so  37574  ptrest  37586  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  poimirlem28  37615  poimirlem31  37618  poimirlem32  37619  heicant  37622  mblfinlem2  37625  mblfinlem3  37626  mblfinlem4  37627  ismblfin  37628  itg2addnclem  37638  itg2addnclem3  37640  itg2addnc  37641  ftc1anc  37668  unirep  37681  sdclem2  37709  sdclem1  37710  sdc  37711  fdc  37712  isbnd  37747  heibor1lem  37776  heiborlem4  37781  heiborlem6  37783  heiborlem10  37787  ismgmOLD  37817  maxidlmax  38010  prnc  38034  isfldidl  38035  dmnnzd  38042  disjressuc2  38347  qsdisjALTV  38579  eqvrelqsel  38580  riotasvd  38922  lshpdisj  38953  lsat0cv  38999  lcvexchlem4  39003  lcvexchlem5  39004  lshpkrlem1  39076  lshpkrlem2  39077  lshpkrlem3  39078  lshpkrcl  39082  islshpkrN  39086  atnle  39283  glbconxN  39345  isline  39706  ispointN  39709  pmapglbx  39736  ispsubcl2N  39914  lhp2atnle  40000  cdleme43fsv1snlem  40387  cdleme40v  40436  cdlemkid5  40902  cdlemkid  40903  dvhb1dimN  40953  dib1dim  41132  dicopelval  41144  dicelval1sta  41154  diclspsn  41161  dihvalcqpre  41202  dihglblem2aN  41260  dihglblem2N  41261  dih1dimatlem  41296  dihpN  41303  dochfl1  41443  lcfl7N  41468  lcf1o  41518  hvmapvalvalN  41728  hdmapval2lem  41798  aks6d1c1  42077  aks6d1c4  42085  sticksstones10  42116  sticksstones12a  42118  aks6d1c7  42145  sn-iotalem  42182  f1o2d2  42194  fiabv  42497  evlsbagval  42527  selvvvval  42546  fsuppind  42551  absnw  42639  elrfi  42655  nacsfg  42666  mzpcompact2lem  42712  eldioph2b  42724  eldioph3  42727  eldiophss  42735  diophrex  42736  elnn0rabdioph  42764  rencldnfilem  42781  elpell1qr  42808  elpell14qr  42810  elpell1234qr  42812  jm2.27  42970  rmydioph  42976  expdiophlem2  42984  wepwsolem  43004  aomclem6  43021  lnr2i  43078  lpirlnr  43079  hbtlem2  43086  hbtlem4  43088  hbtlem5  43090  rngunsnply  43131  flcidc  43132  onsucelab  43225  limnsuc  43227  nnoeomeqom  43274  cantnfresb  43286  tfsconcatfv2  43302  tfsconcatb0  43306  oaun3lem1  43336  oadif1lem  43341  oadif1  43342  clcnvlem  43585  brtrclfv2  43689  frege55lem1c  43878  frege104  43929  clsk1indlem0  44003  clsk1indlem2  44004  clsk1indlem3  44005  clsk1indlem4  44006  clsk1indlem1  44007  pm13.192  44372  equncomVD  44830  csbingVD  44846  csbsngVD  44855  csbfv12gALTVD  44861  relopabVD  44863  refsum2cnlem1  45004  elrnmptf  45148  upbdrech  45276  ssfiunibd  45280  iccshift  45489  iooshift  45493  fsumf1of  45545  limcperiod  45599  climinf2mpt  45685  climinfmpt  45686  cncfshiftioo  45863  itgiccshift  45951  itgperiod  45952  stoweidlem46  46017  fourierdlem29  46107  fourierdlem37  46115  fourierdlem48  46125  fourierdlem51  46128  fourierdlem54  46131  fourierdlem62  46139  fourierdlem79  46156  fourierdlem81  46158  fourierdlem82  46159  fourierdlem92  46169  fourierdlem96  46173  fourierdlem97  46174  fourierdlem98  46175  fourierdlem99  46176  fourierdlem103  46180  fourierdlem104  46181  fourierdlem105  46182  fourierdlem108  46185  fourierdlem110  46187  fourierdlem112  46189  etransclem1  46206  etransclem5  46210  etransclem17  46222  etransclem32  46237  etransclem41  46246  sge0f1o  46353  sge0resplit  46377  sge0fodjrnlem  46387  nnfoctbdjlem  46426  nnfoctbdj  46427  ovnval  46512  ovnlecvr  46529  ovnpnfelsup  46530  ovn0lem  46536  hoidmvval  46548  hoidmvlelem1  46566  ovnhoilem1  46572  ovnhoi  46574  ovnlecvr2  46581  hoidifhspval3  46590  hspmbllem2  46598  hoimbl  46602  ovnsubadd2  46617  ovolval5lem2  46624  ovolval5lem3  46625  ovolval5  46626  ovnovol  46630  sinnpoly  46865  fsetsnf  47025  fsetsnfo  47027  fcoresf1  47043  aiotaval  47069  euoreqb  47083  afv0fv0  47123  afvfv0bi  47126  afvelrnb  47137  afvelrnb0  47138  afv20defat  47206  otiunsndisjX  47253  fun2dmnopgexmpl  47258  2ffzoeq  47301  modmkpkne  47335  elsetpreimafvb  47358  imasetpreimafvbijlemfo  47379  fargshiftf1  47415  fargshiftfo  47416  ichnreuop  47446  ichreuopeq  47447  elsprel  47449  spr0nelg  47450  sprel  47458  prelspr  47460  sprsymrelf1lem  47465  sprsymrelfolem2  47467  paireqne  47485  prprelb  47490  prprelprb  47491  reupr  47496  reuopreuprim  47500  fmtnoprmfac1lem  47538  fmtnofac2  47543  m1expevenALTV  47621  odd2np1ALTV  47648  opoeALTV  47657  opeoALTV  47658  perfectALTVlem2  47696  isgbe  47725  isgbow  47726  isgbo  47727  sbgoldbalt  47755  sgoldbeven3prm  47757  mogoldbb  47759  nnsum3primesgbe  47766  nnsum3primesle9  47768  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  vopnbgrel  47827  dfclnbgr6  47829  dfnbgr6  47830  isuspgrim0  47867  isuspgrimlem  47868  clnbgrgrim  47907  usgrgrtrirex  47922  stgredgel  47929  stgrusgra  47931  stgr1  47933  grlimgrtri  47968  gpgiedgdmel  48013  gpgedgel  48014  gpgprismgr4cycllem10  48067  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem4  48082  pgnbgreunbgr  48088  uspgrsprf1  48108  uspgrsprfo  48109  0nodd  48131  1odd  48132  2nodd  48133  0even  48198  1neven  48199  2even  48200  2zlidl  48201  2zrngamgm  48206  2zrngagrp  48210  2zrngmmgm  48213  2zrngnmrid  48217  suppmptcfin  48337  lcoval  48374  linc0scn0  48385  linc1  48387  el0ldep  48428  snlindsntor  48433  blenval  48533  nn0sumshdiglemB  48582  itcoval1  48625  mo0  48775  eloprab1st2nd  48829  oppcmndclem  48979  sectpropdlem  48998  invpropdlem  49000  isopropdlem  49002  upciclem1  49128  oppcup3lem  49168  isthincd2lem1  49387  termcbasmo  49445  isinito2lem  49460  arweuthinc  49491  arweutermc  49492  discsntermlem  49532  basrestermcfolem  49533