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  3451  cgsex4gOLD  3484  sbhypfOLD  3500  rexraleqim  3602  eqvincf  3605  pm13.183  3621  moeq  3667  mob  3677  euind  3684  reu2eqd  3696  reuind  3713  eqsbc1  3789  sbceqal  3804  csbhypf  3879  uniiunlem  4038  snjust  4576  elsng  4591  elprg  4600  reusngf  4626  rexreusng  4631  reuprg0  4654  rabrsn  4676  preq12bg  4804  intab  4928  uniintsn  4935  dfiun2g  4980  dfiin2g  4981  disji2  5076  disjprg  5088  unopab  5172  eusv1  5330  reusv2lem2  5338  reusv3  5344  opthg  5420  copsexgw  5433  copsexg  5434  propeqop  5450  euotd  5456  otiunsndisj  5463  elopabw  5469  solin  5554  elxpi  5641  opbrop  5717  relop  5793  ideqg  5794  dmopab2rex  5860  elrnmpt  5900  elrnmpt1  5902  elrnmptg  5903  restidsing  6004  somin1  6082  cnveqb  6145  reu3op  6240  reuop  6241  ordequn  6412  iotaval2  6453  funopg  6516  f0rn0  6709  fvelrnb  6883  fvmptg  6928  fndmin  6979  eldmrexrn  7025  foelrn  7041  foelrnf  7042  foco2  7043  fmptco  7063  funopsn  7082  funsndifnop  7085  fmptsng  7104  fmptsnd  7105  tpres  7137  eufnfv  7165  elabrex  7178  elabrexg  7179  abrexco  7180  f1veqaeq  7193  fpropnf1  7204  nf1const  7241  isosolem  7284  f1oiso  7288  eusvobj2  7341  oprabidw  7380  oprabid  7381  f1opr  7405  oprabv  7409  0mpo0  7432  elrnmpog  7484  elrnmpo  7485  elrnmpores  7487  ralrnmpo  7488  ov3  7512  ov6g  7513  ovelrn  7525  caovcang  7550  caovcan  7553  caofidlcan  7651  uniuni  7698  orduninsuc  7776  funcnvuni  7865  fiunlem  7877  fiun  7878  f1iun  7879  f1oweALT  7907  opiota  7994  eloprabi  7998  frxp  8059  funsssuppss  8123  dftpos4  8178  tz7.44-2  8329  tz7.44-3  8330  oev  8432  oalimcl  8478  omlimcl  8496  odi  8497  omeu  8503  oeeui  8520  nneob  8574  omopth  8580  eldifsucnn  8582  elqsg  8691  qsdisj  8721  qsel  8723  brecop  8737  eroveu  8739  erovlem  8740  elixpsn  8864  ixpsnf1o  8865  boxcutc  8868  2dom  8955  fundmen  8956  xpf1o  9056  nneneq  9120  fofinf1o  9222  elfi  9303  elfiun  9320  dffi3  9321  brwdom  9459  brwdom3  9474  unwdomg  9476  xpwdomg  9477  noinfep  9556  cantnfp1lem1  9574  cantnfp1lem3  9576  cantnflem1  9585  ssttrcl  9611  ttrclselem2  9622  scott0  9782  updjudhcoinrg  9829  updjud  9830  carden2a  9862  cardiun  9878  pm54.43lem  9896  alephval3  10004  dfac5lem3  10019  dfac5lem4  10020  dfac5lem4OLD  10022  dfac2b  10025  kmlem9  10053  kmlem12  10056  cardcf  10146  cfeq0  10150  cfsuc  10151  cff1  10152  cflim2  10157  cfss  10159  isfin5  10193  fin1a2lem11  10304  fin1a2lem13  10306  brdom7disj  10425  brdom6disj  10426  canthp1lem2  10547  canthp1  10548  tskuni  10677  gruina  10712  genpv  10893  genpelv  10894  addsrmo  10967  mulsrmo  10968  ltsosr  10988  ltresr  11034  axcnre  11058  axpre-lttri  11059  ltordlem  11645  ltord1  11646  fimaxre3  12071  supaddc  12092  supadd  12093  supmul1  12094  supmullem1  12095  supmullem2  12096  supmul  12097  creur  12122  creui  12123  nn1m1nn  12149  elz  12473  nn0ind-raph  12576  xnegeq  13109  xmullem2  13167  xmulasslem  13187  fleqceilz  13758  fseqsupubi  13885  sqeqor  14123  nn0opth2  14179  hash1snb  14326  hash2prde  14377  prprrab  14380  hash2pwpr  14383  tpf1ofv1  14404  tpf1ofv2  14405  tpfo  14407  fi1uzind  14414  wrd2ind  14629  cshfn  14696  cshf1  14716  2cshwcshw  14732  scshwfzeqfzo  14733  pfx2  14854  s3iunsndisj  14875  relexpsucnnr  14932  relexprelg  14945  rtrclreclem3  14967  shftfval  14977  sgnval  14995  01sqrexlem6  15154  reusq0  15372  summo  15624  fsum  15627  telfsumo  15709  infcvgaux1i  15764  infcvgaux2i  15765  mertenslem1  15791  mertenslem2  15792  mertens  15793  prodmo  15843  fprod  15848  ruclem12  16150  mod2eq1n2dvds  16258  divalg  16314  ndvdssub  16320  sadcp1  16366  smupp1  16391  gcdval  16407  bezoutlem1  16450  bezoutlem3  16452  bezoutlem4  16453  bezout  16454  lcmval  16503  coprmgcdb  16560  coprmdvds1  16563  divgcdcoprmex  16577  dvdsprime  16598  nprm  16599  dvdsprm  16614  coprm  16622  qnumval  16648  qdenval  16649  m1dvdsndvds  16710  reumodprminv  16716  pcval  16756  pceu  16758  pczpre  16759  pcdiv  16764  4sqlem2  16861  4sqlem4  16864  4sqlem12  16868  4sq  16876  vdwapval  16885  vdwapun  16886  vdwlem6  16898  cshwrepswhash1  17014  acsfn  17565  initoid  17908  termoid  17909  cat1lem  18003  posi  18223  gsumval2a  18559  smndex2dnrinv  18789  mgm2nsgrplem2  18793  mgm2nsgrplem3  18794  sgrp2nmndlem5  18803  mgmnsgrpex  18805  sgrpnmndex  18806  cyccom  19082  ghmf1  19125  conjnmzb  19132  orbsta  19192  symgextfv  19297  symgextfo  19301  symgfixfo  19318  pmtrprfval  19366  pmtrprfvalrn  19367  psgneu  19385  psgnval  19386  psgnvali  19387  psgnvalii  19388  odfval  19411  odval  19413  dfod2  19443  submod  19448  isslw  19487  sylow2alem1  19496  sylow3lem2  19507  lsmelvalm  19530  lsmdisj2  19561  efgrelexlemb  19629  frgpup3lem  19656  cyggeninv  19762  gsumval3eu  19783  gsumval3lem2  19785  gsummpt1n0  19844  nn0gsumfz  19863  dprddisj2  19920  dpjrid  19943  pgpfac1lem3  19958  rrgeq0i  20584  domneq0  20593  domnlcanb  20605  domnrcanb  20607  abveq0  20703  abvtrivd  20717  lss1d  20866  lspsn  20905  ellspsn  20906  lspprel  20998  prmirredlem  21379  znf1o  21458  znfld  21467  znunit  21470  cygznlem3  21476  psgndif  21509  ipeq0  21545  obsip  21628  frlmphl  21688  uvcvval  21693  ellspd  21709  psrlidm  21869  psrridm  21870  psrascl  21886  mvrval2  21890  mvrf1  21893  mplmonmul  21941  evlslem3  21985  mhpsclcl  22032  psdmplcl  22047  psdmul  22051  psdmvr  22054  coe1tm  22157  coe1tmfv2  22159  cply1coe0  22186  cply1coe0bi  22187  gsummoncoe1  22193  mamufacex  22281  mat1comp  22325  mat1dimelbas  22356  mat1dimid  22359  scmatel  22390  scmateALT  22397  mavmulsolcl  22436  marrepeval  22448  marepveval  22453  mdetunilem8  22504  maducoeval2  22525  madugsum  22528  minmar1eval  22534  symgmatr01lem  22538  symgmatr01  22539  gsummatr01lem3  22542  gsummatr01lem4  22543  gsummatr01  22544  m2cpm  22626  m2cpminvid2lem  22639  decpmatid  22655  monmatcollpw  22664  pmatcollpw3fi1lem1  22671  mp2pm2mplem4  22694  fvmptnn04ifc  22737  chfacffsupp  22741  chfacfscmul0  22743  chfacfscmulgsum  22745  chfacfpmmul0  22747  chfacfpmmulgsum  22749  cpmadumatpoly  22768  cayleyhamilton  22775  cayleyhamiltonALT  22776  istopon  22797  toponsspwpw  22807  fctop  22889  cctop  22891  ppttop  22892  pptbas  22893  epttop  22894  t0sep  23209  t1sep2  23254  cmpsublem  23284  cmpsub  23285  unisngl  23412  txuni2  23450  elpt  23457  ptbasfi  23466  xkoopn  23474  ptpjopn  23497  ptclsg  23500  dfac14lem  23502  ptcnp  23507  ptrescn  23524  tx1stc  23535  qtopeu  23601  kqt0lem  23621  isr0  23622  hauspwpwf1  23872  xmeteq0  24224  imasf1oxmet  24261  comet  24399  stdbdxmet  24401  met2ndci  24408  prdsxmslem2  24415  nrmmetd  24460  tngngp  24540  tngngp3  24542  xrsxmet  24696  iccpnfcnv  24840  iccpnfhmeo  24841  cnheibor  24852  elovolm  25374  ovolgelb  25379  ovolicc1  25415  ovolicc  25422  ioorval  25473  uniioombllem6  25487  dyadmax  25497  dyadmbl  25499  i1fadd  25594  i1fmul  25595  itg1addlem3  25597  i1fmulc  25602  itg2l  25628  itg2leub  25633  limcmpt  25782  limcco  25792  dvcobr  25847  dvcobrOLD  25848  deg1ldg  25995  ig1pval  26079  elply  26098  elply2  26099  coeval  26126  coe1termlem  26161  coe1term  26162  quotval  26198  plydivlem4  26202  plydivex  26203  vieta1  26218  aannenlem2  26235  aalioulem2  26239  abelthlem9  26348  logtayllem  26566  logtayl  26567  isosctrlem2  26727  leibpilem2  26849  rlimcnp2  26874  efrlim  26877  efrlimOLD  26878  mpodvdsmulf1o  27102  dvdsmulf1o  27104  perfectlem2  27139  lgsfval  27211  lgsval2lem  27216  lgsqrmodndvds  27262  lgsdchrval  27263  gausslemma2dlem0i  27273  2lgslem1b  27301  2lgslem3  27313  2sqlem2  27327  2sqlem8  27335  2sqlem9  27336  2sqlem11  27338  addsq2reu  27349  dchrisum0flblem1  27417  padicval  27526  padicabv  27539  ostth1  27542  sltval2  27566  sltintdifex  27571  sltres  27572  nolt02o  27605  madef  27766  addsval2  27875  addsproplem2  27882  addsproplem4  27884  addsproplem5  27885  addsproplem6  27886  addsprop  27888  addscut  27890  sleadd1  27901  addsuniflem  27913  addsunif  27914  addsasslem1  27915  addsasslem2  27916  addsbdaylem  27928  negsprop  27946  negsid  27952  mulsval2lem  28018  mulsproplem9  28032  mulsproplem12  28035  mulsprop  28038  ssltmul1  28055  ssltmul2  28056  mulsuniflem  28057  addsdilem1  28059  addsdilem2  28060  mulsasslem1  28071  mulsasslem2  28072  mulsunif2  28078  precsexlemcbv  28113  precsexlem9  28122  precsexlem11  28124  n0s0suc  28239  onsfi  28252  n0s0m1  28257  nn1m1nns  28268  eucliddivs  28270  n0seo  28313  zseo  28314  expsval  28317  elzs12  28350  zs12zodd  28359  zs12ge0  28360  recut  28365  0reno  28366  renegscl  28367  readdscl  28368  remulscllem1  28369  remulscl  28371  axtgcgrid  28408  axtgbtwnid  28411  islmib  28732  inaghl  28790  axpaschlem  28885  axlowdimlem15  28901  axlowdim  28906  upgredg2vtx  29086  edglnl  29088  umgredgnlp  29092  usgredg2vtxeuALT  29167  uspgredg2v  29169  ushgredgedgloop  29176  nbusgredgeu  29311  cusgrfilem2  29402  cusgrfi  29404  vtxdushgrfvedg  29436  1loopgrvd2  29449  rusgr1vtxlem  29533  wlkeq  29579  wlkp1lem8  29624  upgrwlkdvdelem  29681  crctcshwlkn0lem6  29760  wlknwwlksnbij  29833  rusgrnumwwlkl1  29913  clwlkclwwlklem2a1  29936  clwwlknscsh  30006  eleclclwwlkn  30020  hashecclwwlkn1  30021  umgrhashecclwwlk  30022  clwwlknon1sn  30044  frgr3vlem1  30217  3vfriswmgrlem  30221  frgrncvvdeqlem3  30245  wlkl0  30311  frgrreggt1  30337  nvz  30613  nmosetn0  30709  nmoolb  30715  nmoubi  30716  nmlno0lem  30737  nmlno0i  30738  hvsubeq0  31012  hvaddcan  31014  normsub0  31080  norm1exi  31194  pjhval  31341  omlsii  31347  omlsi  31348  pjoml  31380  h1de2ci  31500  spansneleq  31514  h1datomi  31525  h1datom  31526  spansncv  31597  5oalem6  31603  pj11  31658  nmopsetn0  31809  nmfnsetn0  31822  nmoplb  31851  nmopub  31852  nmfnlb  31868  nmfnleub  31869  nmlnop0iALT  31939  nmlnop0  31942  lnopeq  31953  nmopun  31958  nmcexi  31970  branmfn  32049  pjnmopi  32092  pj3i  32152  atss  32290  atom1d  32297  chirred  32339  cdj3lem2  32379  eqelbid  32419  elabreximd  32454  disjxpin  32532  disjunsn  32538  br8d  32555  fmptcof2  32601  sgn3da  32780  sgnmul  32781  sgnnbi  32784  sgnpbi  32785  sgn0bi  32786  psgnfzto1stlem  33043  sgnsval  33104  elrgspnlem2  33184  elrgspnlem3  33185  domnlcanOLD  33220  linds2eq  33319  elrspunsn  33367  mxidlmax  33403  1arithidomlem1  33473  1arithidom  33475  1arithufdlem1  33482  1arithufdlem2  33483  1arithufdlem3  33484  1arithufdlem4  33485  1arithufd  33486  dfufd2  33488  ply1dg1rt  33516  lbsdiflsp0  33599  fedgmullem1  33602  fedgmullem2  33603  rtelextdg2lem  33699  constrsuc  33711  constrcbvlem  33728  2sqr3minply  33753  madjusmdetlem2  33801  madjusmdet  33804  zarclssn  33846  xrge0iifcnv  33906  xrge0iifcv  33907  xrge0iifhom  33910  xrge0tmd  33918  xrge0tmdALT  33919  esumc  34024  plymulx0  34521  signspval  34526  tgoldbachgt  34637  bnj1468  34819  fineqvnttrclselem3  35082  fineqvnttrclse  35083  f1resfz0f1d  35097  acycgrcycl  35130  sconnpi1  35222  cvmlift3lem2  35303  satfv0  35341  satfv1  35346  satfbrsuc  35349  satfrnmapom  35353  satfv0fun  35354  satf0op  35360  sat1el2xp  35362  fmlafvel  35368  fmla1  35370  isfmlasuc  35371  fmlaomn0  35373  gonan0  35375  goaln0  35376  gonar  35378  goalr  35380  fmla0disjsuc  35381  fmlasucdisj  35382  satffunlem1lem1  35385  satffunlem2lem1  35387  dmopab3rexdif  35388  satfv0fvfmla0  35396  sategoelfvb  35402  ex-sategoelel  35404  satfv1fvfmla1  35406  2goelgoanfmla1  35407  ex-sategoelelomsuc  35409  ex-sategoelel12  35410  prv1n  35414  ellcsrspsn  35624  r1peuqusdeg1  35626  br8  35739  br6  35740  br4  35741  rdgprc0  35777  dfrdg2  35779  dfbigcup2  35883  elsingles  35902  dfiota3  35907  brimageg  35911  brdomaing  35919  brrangeg  35920  dfrdg4  35935  elaltxp  35959  funtransport  36015  fvtransport  36016  brsegle  36092  funray  36124  fvray  36125  funline  36126  fvline  36128  ellines  36136  linethru  36137  rankeq1o  36155  subtr  36298  subtr2  36299  nn0prpw  36307  bj-elabd2ALT  36909  bj-gabss  36919  bj-imafv  37235  topdifinffinlem  37331  topdifinffin  37332  topdifinfeq  37334  finxpreclem2  37374  finxpreclem3  37377  fvineqsnf1  37394  fvineqsneu  37395  wl-ax12v2cl  37490  wl-issetft  37566  fin2so  37597  ptrest  37609  poimirlem25  37635  poimirlem26  37636  poimirlem27  37637  poimirlem28  37638  poimirlem31  37641  poimirlem32  37642  heicant  37645  mblfinlem2  37648  mblfinlem3  37649  mblfinlem4  37650  ismblfin  37651  itg2addnclem  37661  itg2addnclem3  37663  itg2addnc  37664  ftc1anc  37691  unirep  37704  sdclem2  37732  sdclem1  37733  sdc  37734  fdc  37735  isbnd  37770  heibor1lem  37799  heiborlem4  37804  heiborlem6  37806  heiborlem10  37810  ismgmOLD  37840  maxidlmax  38033  prnc  38057  isfldidl  38058  dmnnzd  38065  disjressuc2  38370  qsdisjALTV  38602  eqvrelqsel  38603  riotasvd  38945  lshpdisj  38976  lsat0cv  39022  lcvexchlem4  39026  lcvexchlem5  39027  lshpkrlem1  39099  lshpkrlem2  39100  lshpkrlem3  39101  lshpkrcl  39105  islshpkrN  39109  atnle  39306  glbconxN  39367  isline  39728  ispointN  39731  pmapglbx  39758  ispsubcl2N  39936  lhp2atnle  40022  cdleme43fsv1snlem  40409  cdleme40v  40458  cdlemkid5  40924  cdlemkid  40925  dvhb1dimN  40975  dib1dim  41154  dicopelval  41166  dicelval1sta  41176  diclspsn  41183  dihvalcqpre  41224  dihglblem2aN  41282  dihglblem2N  41283  dih1dimatlem  41318  dihpN  41325  dochfl1  41465  lcfl7N  41490  lcf1o  41540  hvmapvalvalN  41750  hdmapval2lem  41820  aks6d1c1  42099  aks6d1c4  42107  sticksstones10  42138  sticksstones12a  42140  aks6d1c7  42167  sn-iotalem  42204  f1o2d2  42216  fiabv  42519  evlsbagval  42549  selvvvval  42568  fsuppind  42573  absnw  42661  elrfi  42677  nacsfg  42688  mzpcompact2lem  42734  eldioph2b  42746  eldioph3  42749  eldiophss  42757  diophrex  42758  elnn0rabdioph  42786  rencldnfilem  42803  elpell1qr  42830  elpell14qr  42832  elpell1234qr  42834  jm2.27  42991  rmydioph  42997  expdiophlem2  43005  wepwsolem  43025  aomclem6  43042  lnr2i  43099  lpirlnr  43100  hbtlem2  43107  hbtlem4  43109  hbtlem5  43111  rngunsnply  43152  flcidc  43153  onsucelab  43246  limnsuc  43248  nnoeomeqom  43295  cantnfresb  43307  tfsconcatfv2  43323  tfsconcatb0  43327  oaun3lem1  43357  oadif1lem  43362  oadif1  43363  clcnvlem  43606  brtrclfv2  43710  frege55lem1c  43899  frege104  43950  clsk1indlem0  44024  clsk1indlem2  44025  clsk1indlem3  44026  clsk1indlem4  44027  clsk1indlem1  44028  pm13.192  44393  equncomVD  44851  csbingVD  44867  csbsngVD  44876  csbfv12gALTVD  44882  relopabVD  44884  refsum2cnlem1  45025  elrnmptf  45169  upbdrech  45297  ssfiunibd  45301  iccshift  45509  iooshift  45513  fsumf1of  45565  limcperiod  45619  climinf2mpt  45705  climinfmpt  45706  cncfshiftioo  45883  itgiccshift  45971  itgperiod  45972  stoweidlem46  46037  fourierdlem29  46127  fourierdlem37  46135  fourierdlem48  46145  fourierdlem51  46148  fourierdlem54  46151  fourierdlem62  46159  fourierdlem79  46176  fourierdlem81  46178  fourierdlem82  46179  fourierdlem92  46189  fourierdlem96  46193  fourierdlem97  46194  fourierdlem98  46195  fourierdlem99  46196  fourierdlem103  46200  fourierdlem104  46201  fourierdlem105  46202  fourierdlem108  46205  fourierdlem110  46207  fourierdlem112  46209  etransclem1  46226  etransclem5  46230  etransclem17  46242  etransclem32  46257  etransclem41  46266  sge0f1o  46373  sge0resplit  46397  sge0fodjrnlem  46407  nnfoctbdjlem  46446  nnfoctbdj  46447  ovnval  46532  ovnlecvr  46549  ovnpnfelsup  46550  ovn0lem  46556  hoidmvval  46568  hoidmvlelem1  46586  ovnhoilem1  46592  ovnhoi  46594  ovnlecvr2  46601  hoidifhspval3  46610  hspmbllem2  46618  hoimbl  46622  ovnsubadd2  46637  ovolval5lem2  46644  ovolval5lem3  46645  ovolval5  46646  ovnovol  46650  sinnpoly  46885  fsetsnf  47045  fsetsnfo  47047  fcoresf1  47063  aiotaval  47089  euoreqb  47103  afv0fv0  47143  afvfv0bi  47146  afvelrnb  47157  afvelrnb0  47158  afv20defat  47226  otiunsndisjX  47273  fun2dmnopgexmpl  47278  2ffzoeq  47321  modmkpkne  47355  elsetpreimafvb  47378  imasetpreimafvbijlemfo  47399  fargshiftf1  47435  fargshiftfo  47436  ichnreuop  47466  ichreuopeq  47467  elsprel  47469  spr0nelg  47470  sprel  47478  prelspr  47480  sprsymrelf1lem  47485  sprsymrelfolem2  47487  paireqne  47505  prprelb  47510  prprelprb  47511  reupr  47516  reuopreuprim  47520  fmtnoprmfac1lem  47558  fmtnofac2  47563  m1expevenALTV  47641  odd2np1ALTV  47668  opoeALTV  47677  opeoALTV  47678  perfectALTVlem2  47716  isgbe  47745  isgbow  47746  isgbo  47747  sbgoldbalt  47775  sgoldbeven3prm  47777  mogoldbb  47779  nnsum3primesgbe  47786  nnsum3primesle9  47788  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  vopnbgrel  47848  dfclnbgr6  47850  dfnbgr6  47851  isuspgrim0  47888  isuspgrimlem  47889  clnbgrgrim  47928  usgrgrtrirex  47944  stgredgel  47951  stgrusgra  47953  stgr1  47955  grlimgrtri  47997  gpgiedgdmel  48043  gpgedgel  48044  gpgprismgr4cycllem10  48098  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem4  48113  pgnbgreunbgr  48119  uspgrsprf1  48141  uspgrsprfo  48142  0nodd  48164  1odd  48165  2nodd  48166  0even  48231  1neven  48232  2even  48233  2zlidl  48234  2zrngamgm  48239  2zrngagrp  48243  2zrngmmgm  48246  2zrngnmrid  48250  suppmptcfin  48370  lcoval  48407  linc0scn0  48418  linc1  48420  el0ldep  48461  snlindsntor  48466  blenval  48566  nn0sumshdiglemB  48615  itcoval1  48658  mo0  48808  eloprab1st2nd  48862  oppcmndclem  49012  sectpropdlem  49031  invpropdlem  49033  isopropdlem  49035  upciclem1  49161  oppcup3lem  49201  isthincd2lem1  49420  termcbasmo  49478  isinito2lem  49493  arweuthinc  49524  arweutermc  49525  discsntermlem  49565  basrestermcfolem  49566