Theorem eqeq1 2738

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 2736	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726

This theorem is referenced by:  eqeq1i  2739  eqtr  2754  eqtr2  2755  iseqsetvlem  2797  eqsb1  2860  cbvexeqsetf  3453  cgsex4gOLD  3486  rexraleqim  3599  eqvincf  3602  pm13.183  3618  moeq  3663  mob  3673  euind  3680  reu2eqd  3692  reuind  3709  eqsbc1  3785  sbceqal  3800  csbhypf  3875  uniiunlem  4037  snjust  4577  elsng  4592  elprg  4601  reusngf  4629  rexreusng  4634  reuprg0  4657  rabrsn  4679  preq12bg  4807  intab  4931  uniintsn  4938  dfiun2g  4983  dfiin2g  4984  disji2  5080  disjprg  5092  unopab  5176  eusv1  5334  reusv2lem2  5342  reusv3  5348  opthg  5423  copsexgw  5436  copsexg  5437  propeqop  5453  euotd  5459  otiunsndisj  5466  elopabw  5472  solin  5557  elxpi  5644  opbrop  5720  relop  5797  ideqg  5798  dmopab2rex  5864  elrnmpt  5905  elrnmpt1  5907  elrnmptg  5908  restidsing  6010  somin1  6088  cnveqb  6152  reu3op  6248  reuop  6249  ordequn  6420  iotaval2  6461  funopg  6524  f0rn0  6717  fvelrnb  6892  fvmptg  6937  fndmin  6988  eldmrexrn  7034  foelrn  7050  foelrnf  7051  foco2  7052  fmptco  7072  funopsn  7091  funsndifnop  7094  fmptsng  7112  fmptsnd  7113  tpres  7145  eufnfv  7173  elabrex  7186  elabrexg  7187  abrexco  7188  f1veqaeq  7200  fpropnf1  7211  nf1const  7248  isosolem  7291  f1oiso  7295  eusvobj2  7348  oprabidw  7387  oprabid  7388  f1opr  7412  oprabv  7416  0mpo0  7439  elrnmpog  7491  elrnmpo  7492  elrnmpores  7494  ralrnmpo  7495  ov3  7519  ov6g  7520  ovelrn  7532  caovcang  7557  caovcan  7560  caofidlcan  7658  uniuni  7705  orduninsuc  7783  funcnvuni  7872  fiunlem  7884  fiun  7885  f1iun  7886  f1oweALT  7914  opiota  8001  eloprabi  8005  frxp  8066  funsssuppss  8130  dftpos4  8185  tz7.44-2  8336  tz7.44-3  8337  oev  8439  oalimcl  8485  omlimcl  8503  odi  8504  omeu  8510  oeeui  8528  nneob  8582  omopth  8588  eldifsucnn  8590  elqsg  8699  qsdisj  8729  qsel  8731  brecop  8745  eroveu  8747  erovlem  8748  elixpsn  8873  ixpsnf1o  8874  boxcutc  8877  2dom  8965  fundmen  8966  xpf1o  9065  nneneq  9128  fofinf1o  9230  elfi  9314  elfiun  9331  dffi3  9332  brwdom  9470  brwdom3  9485  unwdomg  9487  xpwdomg  9488  noinfep  9567  cantnfp1lem1  9585  cantnfp1lem3  9587  cantnflem1  9596  ssttrcl  9622  ttrclselem2  9633  scott0  9796  updjudhcoinrg  9843  updjud  9844  carden2a  9876  cardiun  9892  pm54.43lem  9910  alephval3  10018  dfac5lem3  10033  dfac5lem4  10034  dfac5lem4OLD  10036  dfac2b  10039  kmlem9  10067  kmlem12  10070  cardcf  10160  cfeq0  10164  cfsuc  10165  cff1  10166  cflim2  10171  cfss  10173  isfin5  10207  fin1a2lem11  10318  fin1a2lem13  10320  brdom7disj  10439  brdom6disj  10440  canthp1lem2  10562  canthp1  10563  tskuni  10692  gruina  10727  genpv  10908  genpelv  10909  addsrmo  10982  mulsrmo  10983  ltsosr  11003  ltresr  11049  axcnre  11073  axpre-lttri  11074  ltordlem  11660  ltord1  11661  fimaxre3  12086  supaddc  12107  supadd  12108  supmul1  12109  supmullem1  12110  supmullem2  12111  supmul  12112  creur  12137  creui  12138  nn1m1nn  12164  elz  12488  nn0ind-raph  12590  xnegeq  13120  xmullem2  13178  xmulasslem  13198  fleqceilz  13772  fseqsupubi  13899  sqeqor  14137  nn0opth2  14193  hash1snb  14340  hash2prde  14391  prprrab  14394  hash2pwpr  14397  tpf1ofv1  14418  tpf1ofv2  14419  tpfo  14421  fi1uzind  14428  wrd2ind  14644  cshfn  14711  cshf1  14731  2cshwcshw  14746  scshwfzeqfzo  14747  pfx2  14868  s3iunsndisj  14889  relexpsucnnr  14946  relexprelg  14959  rtrclreclem3  14981  shftfval  14991  sgnval  15009  01sqrexlem6  15168  reusq0  15386  summo  15638  fsum  15641  telfsumo  15723  infcvgaux1i  15778  infcvgaux2i  15779  mertenslem1  15805  mertenslem2  15806  mertens  15807  prodmo  15857  fprod  15862  ruclem12  16164  mod2eq1n2dvds  16272  divalg  16328  ndvdssub  16334  sadcp1  16380  smupp1  16405  gcdval  16421  bezoutlem1  16464  bezoutlem3  16466  bezoutlem4  16467  bezout  16468  lcmval  16517  coprmgcdb  16574  coprmdvds1  16577  divgcdcoprmex  16591  dvdsprime  16612  nprm  16613  dvdsprm  16628  coprm  16636  qnumval  16662  qdenval  16663  m1dvdsndvds  16724  reumodprminv  16730  pcval  16770  pceu  16772  pczpre  16773  pcdiv  16778  4sqlem2  16875  4sqlem4  16878  4sqlem12  16882  4sq  16890  vdwapval  16899  vdwapun  16900  vdwlem6  16912  cshwrepswhash1  17028  acsfn  17580  initoid  17923  termoid  17924  cat1lem  18018  posi  18238  gsumval2a  18608  smndex2dnrinv  18838  mgm2nsgrplem2  18842  mgm2nsgrplem3  18843  sgrp2nmndlem5  18852  mgmnsgrpex  18854  sgrpnmndex  18855  cyccom  19130  ghmf1  19173  conjnmzb  19180  orbsta  19240  symgextfv  19345  symgextfo  19349  symgfixfo  19366  pmtrprfval  19414  pmtrprfvalrn  19415  psgneu  19433  psgnval  19434  psgnvali  19435  psgnvalii  19436  odfval  19459  odval  19461  dfod2  19491  submod  19496  isslw  19535  sylow2alem1  19544  sylow3lem2  19555  lsmelvalm  19578  lsmdisj2  19609  efgrelexlemb  19677  frgpup3lem  19704  cyggeninv  19810  gsumval3eu  19831  gsumval3lem2  19833  gsummpt1n0  19892  nn0gsumfz  19911  dprddisj2  19968  dpjrid  19991  pgpfac1lem3  20006  rrgeq0i  20630  domneq0  20639  domnlcanb  20651  domnrcanb  20653  abveq0  20749  abvtrivd  20763  lss1d  20912  lspsn  20951  ellspsn  20952  lspprel  21044  prmirredlem  21425  znf1o  21504  znfld  21513  znunit  21516  cygznlem3  21522  psgndif  21555  ipeq0  21591  obsip  21674  frlmphl  21734  uvcvval  21739  ellspd  21755  psrlidm  21915  psrridm  21916  psrascl  21932  mvrval2  21936  mvrf1  21939  mplmonmul  21989  evlslem3  22033  mhpsclcl  22088  psdmplcl  22103  psdmul  22107  psdmvr  22110  coe1tm  22213  coe1tmfv2  22215  cply1coe0  22243  cply1coe0bi  22244  gsummoncoe1  22250  mamufacex  22338  mat1comp  22382  mat1dimelbas  22413  mat1dimid  22416  scmatel  22447  scmateALT  22454  mavmulsolcl  22493  marrepeval  22505  marepveval  22510  mdetunilem8  22561  maducoeval2  22582  madugsum  22585  minmar1eval  22591  symgmatr01lem  22595  symgmatr01  22596  gsummatr01lem3  22599  gsummatr01lem4  22600  gsummatr01  22601  m2cpm  22683  m2cpminvid2lem  22696  decpmatid  22712  monmatcollpw  22721  pmatcollpw3fi1lem1  22728  mp2pm2mplem4  22751  fvmptnn04ifc  22794  chfacffsupp  22798  chfacfscmul0  22800  chfacfscmulgsum  22802  chfacfpmmul0  22804  chfacfpmmulgsum  22806  cpmadumatpoly  22825  cayleyhamilton  22832  cayleyhamiltonALT  22833  istopon  22854  toponsspwpw  22864  fctop  22946  cctop  22948  ppttop  22949  pptbas  22950  epttop  22951  t0sep  23266  t1sep2  23311  cmpsublem  23341  cmpsub  23342  unisngl  23469  txuni2  23507  elpt  23514  ptbasfi  23523  xkoopn  23531  ptpjopn  23554  ptclsg  23557  dfac14lem  23559  ptcnp  23564  ptrescn  23581  tx1stc  23592  qtopeu  23658  kqt0lem  23678  isr0  23679  hauspwpwf1  23929  xmeteq0  24280  imasf1oxmet  24317  comet  24455  stdbdxmet  24457  met2ndci  24464  prdsxmslem2  24471  nrmmetd  24516  tngngp  24596  tngngp3  24598  xrsxmet  24752  iccpnfcnv  24896  iccpnfhmeo  24897  cnheibor  24908  elovolm  25430  ovolgelb  25435  ovolicc1  25471  ovolicc  25478  ioorval  25529  uniioombllem6  25543  dyadmax  25553  dyadmbl  25555  i1fadd  25650  i1fmul  25651  itg1addlem3  25653  i1fmulc  25658  itg2l  25684  itg2leub  25689  limcmpt  25838  limcco  25848  dvcobr  25903  dvcobrOLD  25904  deg1ldg  26051  ig1pval  26135  elply  26154  elply2  26155  coeval  26182  coe1termlem  26217  coe1term  26218  quotval  26254  plydivlem4  26258  plydivex  26259  vieta1  26274  aannenlem2  26291  aalioulem2  26295  abelthlem9  26404  logtayllem  26622  logtayl  26623  isosctrlem2  26783  leibpilem2  26905  rlimcnp2  26930  efrlim  26933  efrlimOLD  26934  mpodvdsmulf1o  27158  dvdsmulf1o  27160  perfectlem2  27195  lgsfval  27267  lgsval2lem  27272  lgsqrmodndvds  27318  lgsdchrval  27319  gausslemma2dlem0i  27329  2lgslem1b  27357  2lgslem3  27369  2sqlem2  27383  2sqlem8  27391  2sqlem9  27392  2sqlem11  27394  addsq2reu  27405  dchrisum0flblem1  27473  padicval  27582  padicabv  27595  ostth1  27598  sltval2  27622  sltintdifex  27627  sltres  27628  nolt02o  27661  madef  27824  addsval2  27933  addsproplem2  27940  addsproplem4  27942  addsproplem5  27943  addsproplem6  27944  addsprop  27946  addscut  27948  sleadd1  27959  addsuniflem  27971  addsunif  27972  addsasslem1  27973  addsasslem2  27974  addsbdaylem  27986  negsprop  28004  negsid  28010  mulsval2lem  28079  mulsproplem9  28093  mulsproplem12  28096  mulsprop  28099  ssltmul1  28116  ssltmul2  28117  mulsuniflem  28118  addsdilem1  28120  addsdilem2  28121  mulsasslem1  28132  mulsasslem2  28133  mulsunif2  28139  precsexlemcbv  28174  precsexlem9  28183  precsexlem11  28185  n0s0suc  28302  onsfi  28316  n0s0m1  28321  nn1m1nns  28332  eucliddivs  28334  n0seo  28379  zseo  28380  expsval  28383  elzs12  28421  zs12zodd  28431  zs12ge0  28432  recut  28439  elreno2  28440  renegscl  28443  readdscl  28444  remulscllem1  28445  remulscl  28447  axtgcgrid  28484  axtgbtwnid  28487  islmib  28808  inaghl  28866  axpaschlem  28962  axlowdimlem15  28978  axlowdim  28983  upgredg2vtx  29163  edglnl  29165  umgredgnlp  29169  usgredg2vtxeuALT  29244  uspgredg2v  29246  ushgredgedgloop  29253  nbusgredgeu  29388  cusgrfilem2  29479  cusgrfi  29481  vtxdushgrfvedg  29513  1loopgrvd2  29526  rusgr1vtxlem  29610  wlkeq  29656  wlkp1lem8  29701  upgrwlkdvdelem  29758  crctcshwlkn0lem6  29837  wlknwwlksnbij  29910  rusgrnumwwlkl1  29993  clwlkclwwlklem2a1  30016  clwwlknscsh  30086  eleclclwwlkn  30100  hashecclwwlkn1  30101  umgrhashecclwwlk  30102  clwwlknon1sn  30124  frgr3vlem1  30297  3vfriswmgrlem  30301  frgrncvvdeqlem3  30325  wlkl0  30391  frgrreggt1  30417  nvz  30693  nmosetn0  30789  nmoolb  30795  nmoubi  30796  nmlno0lem  30817  nmlno0i  30818  hvsubeq0  31092  hvaddcan  31094  normsub0  31160  norm1exi  31274  pjhval  31421  omlsii  31427  omlsi  31428  pjoml  31460  h1de2ci  31580  spansneleq  31594  h1datomi  31605  h1datom  31606  spansncv  31677  5oalem6  31683  pj11  31738  nmopsetn0  31889  nmfnsetn0  31902  nmoplb  31931  nmopub  31932  nmfnlb  31948  nmfnleub  31949  nmlnop0iALT  32019  nmlnop0  32022  lnopeq  32033  nmopun  32038  nmcexi  32050  branmfn  32129  pjnmopi  32172  pj3i  32232  atss  32370  atom1d  32377  chirred  32419  cdj3lem2  32459  eqelbid  32498  elabreximd  32534  disjxpin  32612  disjunsn  32618  br8d  32635  fmptcof2  32684  sgn3da  32864  sgnmul  32865  sgnnbi  32868  sgnpbi  32869  sgn0bi  32870  psgnfzto1stlem  33131  sgnsval  33192  elrgspnlem2  33274  elrgspnlem3  33275  domnlcanOLD  33311  linds2eq  33411  elrspunsn  33459  mxidlmax  33495  1arithidomlem1  33565  1arithidom  33567  1arithufdlem1  33574  1arithufdlem2  33575  1arithufdlem3  33576  1arithufdlem4  33577  1arithufd  33578  dfufd2  33580  ply1dg1rt  33610  mplvrpmrhm  33661  lbsdiflsp0  33732  fedgmullem1  33735  fedgmullem2  33736  rtelextdg2lem  33832  constrsuc  33844  constrcbvlem  33861  2sqr3minply  33886  madjusmdetlem2  33934  madjusmdet  33937  zarclssn  33979  xrge0iifcnv  34039  xrge0iifcv  34040  xrge0iifhom  34043  xrge0tmd  34051  xrge0tmdALT  34052  esumc  34157  plymulx0  34653  signspval  34658  tgoldbachgt  34769  bnj1468  34951  fineqvnttrclselem3  35228  fineqvnttrclse  35229  f1resfz0f1d  35257  acycgrcycl  35290  sconnpi1  35382  cvmlift3lem2  35463  satfv0  35501  satfv1  35506  satfbrsuc  35509  satfrnmapom  35513  satfv0fun  35514  satf0op  35520  sat1el2xp  35522  fmlafvel  35528  fmla1  35530  isfmlasuc  35531  fmlaomn0  35533  gonan0  35535  goaln0  35536  gonar  35538  goalr  35540  fmla0disjsuc  35541  fmlasucdisj  35542  satffunlem1lem1  35545  satffunlem2lem1  35547  dmopab3rexdif  35548  satfv0fvfmla0  35556  sategoelfvb  35562  ex-sategoelel  35564  satfv1fvfmla1  35566  2goelgoanfmla1  35567  ex-sategoelelomsuc  35569  ex-sategoelel12  35570  prv1n  35574  ellcsrspsn  35784  r1peuqusdeg1  35786  br8  35899  br6  35900  br4  35901  rdgprc0  35934  dfrdg2  35936  dfbigcup2  36040  elsingles  36059  dfiota3  36064  brimageg  36068  brdomaing  36076  brrangeg  36077  dfrdg4  36094  elaltxp  36118  funtransport  36174  fvtransport  36175  brsegle  36251  funray  36283  fvray  36284  funline  36285  fvline  36287  ellines  36295  linethru  36296  rankeq1o  36314  subtr  36457  subtr2  36458  nn0prpw  36466  bj-elabd2ALT  37069  bj-gabss  37079  bj-imafv  37395  topdifinffinlem  37491  topdifinffin  37492  topdifinfeq  37494  finxpreclem2  37534  finxpreclem3  37537  fvineqsnf1  37554  fvineqsneu  37555  wl-ax12v2cl  37650  wl-issetft  37726  fin2so  37747  ptrest  37759  poimirlem25  37785  poimirlem26  37786  poimirlem27  37787  poimirlem28  37788  poimirlem31  37791  poimirlem32  37792  heicant  37795  mblfinlem2  37798  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  itg2addnclem  37811  itg2addnclem3  37813  itg2addnc  37814  ftc1anc  37841  unirep  37854  sdclem2  37882  sdclem1  37883  sdc  37884  fdc  37885  isbnd  37920  heibor1lem  37949  heiborlem4  37954  heiborlem6  37956  heiborlem10  37960  ismgmOLD  37990  maxidlmax  38183  prnc  38207  isfldidl  38208  dmnnzd  38215  disjressuc2  38535  qsdisjALTV  38811  eqvrelqsel  38812  riotasvd  39155  lshpdisj  39186  lsat0cv  39232  lcvexchlem4  39236  lcvexchlem5  39237  lshpkrlem1  39309  lshpkrlem2  39310  lshpkrlem3  39311  lshpkrcl  39315  islshpkrN  39319  atnle  39516  glbconxN  39577  isline  39938  ispointN  39941  pmapglbx  39968  ispsubcl2N  40146  lhp2atnle  40232  cdleme43fsv1snlem  40619  cdleme40v  40668  cdlemkid5  41134  cdlemkid  41135  dvhb1dimN  41185  dib1dim  41364  dicopelval  41376  dicelval1sta  41386  diclspsn  41393  dihvalcqpre  41434  dihglblem2aN  41492  dihglblem2N  41493  dih1dimatlem  41528  dihpN  41535  dochfl1  41675  lcfl7N  41700  lcf1o  41750  hvmapvalvalN  41960  hdmapval2lem  42030  aks6d1c1  42309  aks6d1c4  42317  sticksstones10  42348  sticksstones12a  42350  aks6d1c7  42377  sn-iotalem  42419  f1o2d2  42431  fiabv  42733  evlsbagval  42754  selvvvval  42770  fsuppind  42775  absnw  42863  elrfi  42878  nacsfg  42889  mzpcompact2lem  42935  eldioph2b  42947  eldioph3  42950  eldiophss  42958  diophrex  42959  elnn0rabdioph  42987  rencldnfilem  43004  elpell1qr  43031  elpell14qr  43033  elpell1234qr  43035  jm2.27  43192  rmydioph  43198  expdiophlem2  43206  wepwsolem  43226  aomclem6  43243  lnr2i  43300  lpirlnr  43301  hbtlem2  43308  hbtlem4  43310  hbtlem5  43312  rngunsnply  43353  flcidc  43354  onsucelab  43447  limnsuc  43449  nnoeomeqom  43496  cantnfresb  43508  tfsconcatfv2  43524  tfsconcatb0  43528  oaun3lem1  43558  oadif1lem  43563  oadif1  43564  clcnvlem  43806  brtrclfv2  43910  frege55lem1c  44099  frege104  44150  clsk1indlem0  44224  clsk1indlem2  44225  clsk1indlem3  44226  clsk1indlem4  44227  clsk1indlem1  44228  pm13.192  44593  equncomVD  45050  csbingVD  45066  csbsngVD  45075  csbfv12gALTVD  45081  relopabVD  45083  refsum2cnlem1  45224  elrnmptf  45367  upbdrech  45495  ssfiunibd  45499  iccshift  45706  iooshift  45710  fsumf1of  45762  limcperiod  45816  climinf2mpt  45900  climinfmpt  45901  cncfshiftioo  46078  itgiccshift  46166  itgperiod  46167  stoweidlem46  46232  fourierdlem29  46322  fourierdlem37  46330  fourierdlem48  46340  fourierdlem51  46343  fourierdlem54  46346  fourierdlem62  46354  fourierdlem79  46371  fourierdlem81  46373  fourierdlem82  46374  fourierdlem92  46384  fourierdlem96  46388  fourierdlem97  46389  fourierdlem98  46390  fourierdlem99  46391  fourierdlem103  46395  fourierdlem104  46396  fourierdlem105  46397  fourierdlem108  46400  fourierdlem110  46402  fourierdlem112  46404  etransclem1  46421  etransclem5  46425  etransclem17  46437  etransclem32  46452  etransclem41  46461  sge0f1o  46568  sge0resplit  46592  sge0fodjrnlem  46602  nnfoctbdjlem  46641  nnfoctbdj  46642  ovnval  46727  ovnlecvr  46744  ovnpnfelsup  46745  ovn0lem  46751  hoidmvval  46763  hoidmvlelem1  46781  ovnhoilem1  46787  ovnhoi  46789  ovnlecvr2  46796  hoidifhspval3  46805  hspmbllem2  46813  hoimbl  46817  ovnsubadd2  46832  ovolval5lem2  46839  ovolval5lem3  46840  ovolval5  46841  ovnovol  46845  sinnpoly  47079  fsetsnf  47239  fsetsnfo  47241  fcoresf1  47257  aiotaval  47283  euoreqb  47297  afv0fv0  47337  afvfv0bi  47340  afvelrnb  47351  afvelrnb0  47352  afv20defat  47420  otiunsndisjX  47467  fun2dmnopgexmpl  47472  2ffzoeq  47515  modmkpkne  47549  elsetpreimafvb  47572  imasetpreimafvbijlemfo  47593  fargshiftf1  47629  fargshiftfo  47630  ichnreuop  47660  ichreuopeq  47661  elsprel  47663  spr0nelg  47664  sprel  47672  prelspr  47674  sprsymrelf1lem  47679  sprsymrelfolem2  47681  paireqne  47699  prprelb  47704  prprelprb  47705  reupr  47710  reuopreuprim  47714  fmtnoprmfac1lem  47752  fmtnofac2  47757  m1expevenALTV  47835  odd2np1ALTV  47862  opoeALTV  47871  opeoALTV  47872  perfectALTVlem2  47910  isgbe  47939  isgbow  47940  isgbo  47941  sbgoldbalt  47969  sgoldbeven3prm  47971  mogoldbb  47973  nnsum3primesgbe  47980  nnsum3primesle9  47982  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  vopnbgrel  48042  dfclnbgr6  48044  dfnbgr6  48045  isuspgrim0  48082  isuspgrimlem  48083  clnbgrgrim  48122  usgrgrtrirex  48138  stgredgel  48145  stgrusgra  48147  stgr1  48149  grlimgrtri  48191  gpgiedgdmel  48237  gpgedgel  48238  gpgprismgr4cycllem10  48292  pgnbgreunbgrlem1  48301  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem4  48307  pgnbgreunbgr  48313  uspgrsprf1  48335  uspgrsprfo  48336  0nodd  48358  1odd  48359  2nodd  48360  0even  48425  1neven  48426  2even  48427  2zlidl  48428  2zrngamgm  48433  2zrngagrp  48437  2zrngmmgm  48440  2zrngnmrid  48444  suppmptcfin  48564  lcoval  48600  linc0scn0  48611  linc1  48613  el0ldep  48654  snlindsntor  48659  blenval  48759  nn0sumshdiglemB  48808  itcoval1  48851  mo0  49001  eloprab1st2nd  49055  oppcmndclem  49204  sectpropdlem  49223  invpropdlem  49225  isopropdlem  49227  upciclem1  49353  oppcup3lem  49393  isthincd2lem1  49612  termcbasmo  49670  isinito2lem  49685  arweuthinc  49716  arweutermc  49717  discsntermlem  49757  basrestermcfolem  49758