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  17600  initoid  17943  termoid  17944  cat1lem  18038  posi  18258  gsumval2a  18594  smndex2dnrinv  18824  mgm2nsgrplem2  18828  mgm2nsgrplem3  18829  sgrp2nmndlem5  18838  mgmnsgrpex  18840  sgrpnmndex  18841  cyccom  19117  ghmf1  19160  conjnmzb  19167  orbsta  19227  symgextfv  19332  symgextfo  19336  symgfixfo  19353  pmtrprfval  19401  pmtrprfvalrn  19402  psgneu  19420  psgnval  19421  psgnvali  19422  psgnvalii  19423  odfval  19446  odval  19448  dfod2  19478  submod  19483  isslw  19522  sylow2alem1  19531  sylow3lem2  19542  lsmelvalm  19565  lsmdisj2  19596  efgrelexlemb  19664  frgpup3lem  19691  cyggeninv  19797  gsumval3eu  19818  gsumval3lem2  19820  gsummpt1n0  19879  nn0gsumfz  19898  dprddisj2  19955  dpjrid  19978  pgpfac1lem3  19993  rrgeq0i  20619  domneq0  20628  domnlcanb  20640  domnrcanb  20642  abveq0  20738  abvtrivd  20752  lss1d  20901  lspsn  20940  ellspsn  20941  lspprel  21033  prmirredlem  21414  znf1o  21493  znfld  21502  znunit  21505  cygznlem3  21511  psgndif  21544  ipeq0  21580  obsip  21663  frlmphl  21723  uvcvval  21728  ellspd  21744  psrlidm  21904  psrridm  21905  psrascl  21921  mvrval2  21925  mvrf1  21928  mplmonmul  21976  evlslem3  22020  mhpsclcl  22067  psdmplcl  22082  psdmul  22086  psdmvr  22089  coe1tm  22192  coe1tmfv2  22194  cply1coe0  22221  cply1coe0bi  22222  gsummoncoe1  22228  mamufacex  22316  mat1comp  22360  mat1dimelbas  22391  mat1dimid  22394  scmatel  22425  scmateALT  22432  mavmulsolcl  22471  marrepeval  22483  marepveval  22488  mdetunilem8  22539  maducoeval2  22560  madugsum  22563  minmar1eval  22569  symgmatr01lem  22573  symgmatr01  22574  gsummatr01lem3  22577  gsummatr01lem4  22578  gsummatr01  22579  m2cpm  22661  m2cpminvid2lem  22674  decpmatid  22690  monmatcollpw  22699  pmatcollpw3fi1lem1  22706  mp2pm2mplem4  22729  fvmptnn04ifc  22772  chfacffsupp  22776  chfacfscmul0  22778  chfacfscmulgsum  22780  chfacfpmmul0  22782  chfacfpmmulgsum  22784  cpmadumatpoly  22803  cayleyhamilton  22810  cayleyhamiltonALT  22811  istopon  22832  toponsspwpw  22842  fctop  22924  cctop  22926  ppttop  22927  pptbas  22928  epttop  22929  t0sep  23244  t1sep2  23289  cmpsublem  23319  cmpsub  23320  unisngl  23447  txuni2  23485  elpt  23492  ptbasfi  23501  xkoopn  23509  ptpjopn  23532  ptclsg  23535  dfac14lem  23537  ptcnp  23542  ptrescn  23559  tx1stc  23570  qtopeu  23636  kqt0lem  23656  isr0  23657  hauspwpwf1  23907  xmeteq0  24259  imasf1oxmet  24296  comet  24434  stdbdxmet  24436  met2ndci  24443  prdsxmslem2  24450  nrmmetd  24495  tngngp  24575  tngngp3  24577  xrsxmet  24731  iccpnfcnv  24875  iccpnfhmeo  24876  cnheibor  24887  elovolm  25409  ovolgelb  25414  ovolicc1  25450  ovolicc  25457  ioorval  25508  uniioombllem6  25522  dyadmax  25532  dyadmbl  25534  i1fadd  25629  i1fmul  25630  itg1addlem3  25632  i1fmulc  25637  itg2l  25663  itg2leub  25668  limcmpt  25817  limcco  25827  dvcobr  25882  dvcobrOLD  25883  deg1ldg  26030  ig1pval  26114  elply  26133  elply2  26134  coeval  26161  coe1termlem  26196  coe1term  26197  quotval  26233  plydivlem4  26237  plydivex  26238  vieta1  26253  aannenlem2  26270  aalioulem2  26274  abelthlem9  26383  logtayllem  26601  logtayl  26602  isosctrlem2  26762  leibpilem2  26884  rlimcnp2  26909  efrlim  26912  efrlimOLD  26913  mpodvdsmulf1o  27137  dvdsmulf1o  27139  perfectlem2  27174  lgsfval  27246  lgsval2lem  27251  lgsqrmodndvds  27297  lgsdchrval  27298  gausslemma2dlem0i  27308  2lgslem1b  27336  2lgslem3  27348  2sqlem2  27362  2sqlem8  27370  2sqlem9  27371  2sqlem11  27373  addsq2reu  27384  dchrisum0flblem1  27452  padicval  27561  padicabv  27574  ostth1  27577  sltval2  27601  sltintdifex  27606  sltres  27607  nolt02o  27640  madef  27801  addsval2  27910  addsproplem2  27917  addsproplem4  27919  addsproplem5  27920  addsproplem6  27921  addsprop  27923  addscut  27925  sleadd1  27936  addsuniflem  27948  addsunif  27949  addsasslem1  27950  addsasslem2  27951  addsbdaylem  27963  negsprop  27981  negsid  27987  mulsval2lem  28053  mulsproplem9  28067  mulsproplem12  28070  mulsprop  28073  ssltmul1  28090  ssltmul2  28091  mulsuniflem  28092  addsdilem1  28094  addsdilem2  28095  mulsasslem1  28106  mulsasslem2  28107  mulsunif2  28113  precsexlemcbv  28148  precsexlem9  28157  precsexlem11  28159  n0s0suc  28274  onsfi  28287  n0s0m1  28292  nn1m1nns  28303  eucliddivs  28305  n0seo  28348  zseo  28349  expsval  28352  elzs12  28385  zs12zodd  28394  zs12ge0  28395  recut  28400  0reno  28401  renegscl  28402  readdscl  28403  remulscllem1  28404  remulscl  28406  axtgcgrid  28443  axtgbtwnid  28446  islmib  28767  inaghl  28825  axpaschlem  28920  axlowdimlem15  28936  axlowdim  28941  upgredg2vtx  29121  edglnl  29123  umgredgnlp  29127  usgredg2vtxeuALT  29202  uspgredg2v  29204  ushgredgedgloop  29211  nbusgredgeu  29346  cusgrfilem2  29437  cusgrfi  29439  vtxdushgrfvedg  29471  1loopgrvd2  29484  rusgr1vtxlem  29568  wlkeq  29614  wlkp1lem8  29659  upgrwlkdvdelem  29716  crctcshwlkn0lem6  29795  wlknwwlksnbij  29868  rusgrnumwwlkl1  29948  clwlkclwwlklem2a1  29971  clwwlknscsh  30041  eleclclwwlkn  30055  hashecclwwlkn1  30056  umgrhashecclwwlk  30057  clwwlknon1sn  30079  frgr3vlem1  30252  3vfriswmgrlem  30256  frgrncvvdeqlem3  30280  wlkl0  30346  frgrreggt1  30372  nvz  30648  nmosetn0  30744  nmoolb  30750  nmoubi  30751  nmlno0lem  30772  nmlno0i  30773  hvsubeq0  31047  hvaddcan  31049  normsub0  31115  norm1exi  31229  pjhval  31376  omlsii  31382  omlsi  31383  pjoml  31415  h1de2ci  31535  spansneleq  31549  h1datomi  31560  h1datom  31561  spansncv  31632  5oalem6  31638  pj11  31693  nmopsetn0  31844  nmfnsetn0  31857  nmoplb  31886  nmopub  31887  nmfnlb  31903  nmfnleub  31904  nmlnop0iALT  31974  nmlnop0  31977  lnopeq  31988  nmopun  31993  nmcexi  32005  branmfn  32084  pjnmopi  32127  pj3i  32187  atss  32325  atom1d  32332  chirred  32374  cdj3lem2  32414  eqelbid  32454  elabreximd  32489  disjxpin  32567  disjunsn  32573  br8d  32588  fmptcof2  32631  sgn3da  32809  sgnmul  32810  sgnnbi  32813  sgnpbi  32814  sgn0bi  32815  psgnfzto1stlem  33072  sgnsval  33133  elrgspnlem2  33210  elrgspnlem3  33211  domnlcanOLD  33246  linds2eq  33345  elrspunsn  33393  mxidlmax  33429  1arithidomlem1  33499  1arithidom  33501  1arithufdlem1  33508  1arithufdlem2  33509  1arithufdlem3  33510  1arithufdlem4  33511  1arithufd  33512  dfufd2  33514  ply1dg1rt  33541  lbsdiflsp0  33615  fedgmullem1  33618  fedgmullem2  33619  rtelextdg2lem  33709  constrsuc  33721  constrcbvlem  33738  2sqr3minply  33763  madjusmdetlem2  33811  madjusmdet  33814  zarclssn  33856  xrge0iifcnv  33916  xrge0iifcv  33917  xrge0iifhom  33920  xrge0tmd  33928  xrge0tmdALT  33929  esumc  34034  plymulx0  34531  signspval  34536  tgoldbachgt  34647  bnj1468  34829  f1resfz0f1d  35094  acycgrcycl  35127  sconnpi1  35219  cvmlift3lem2  35300  satfv0  35338  satfv1  35343  satfbrsuc  35346  satfrnmapom  35350  satfv0fun  35351  satf0op  35357  sat1el2xp  35359  fmlafvel  35365  fmla1  35367  isfmlasuc  35368  fmlaomn0  35370  gonan0  35372  goaln0  35373  gonar  35375  goalr  35377  fmla0disjsuc  35378  fmlasucdisj  35379  satffunlem1lem1  35382  satffunlem2lem1  35384  dmopab3rexdif  35385  satfv0fvfmla0  35393  sategoelfvb  35399  ex-sategoelel  35401  satfv1fvfmla1  35403  2goelgoanfmla1  35404  ex-sategoelelomsuc  35406  ex-sategoelel12  35407  prv1n  35411  ellcsrspsn  35621  r1peuqusdeg1  35623  br8  35736  br6  35737  br4  35738  rdgprc0  35774  dfrdg2  35776  dfbigcup2  35880  elsingles  35899  dfiota3  35904  brimageg  35908  brdomaing  35916  brrangeg  35917  dfrdg4  35932  elaltxp  35956  funtransport  36012  fvtransport  36013  brsegle  36089  funray  36121  fvray  36122  funline  36123  fvline  36125  ellines  36133  linethru  36134  rankeq1o  36152  subtr  36295  subtr2  36296  nn0prpw  36304  bj-elabd2ALT  36906  bj-gabss  36916  bj-imafv  37232  topdifinffinlem  37328  topdifinffin  37329  topdifinfeq  37331  finxpreclem2  37371  finxpreclem3  37374  fvineqsnf1  37391  fvineqsneu  37392  wl-ax12v2cl  37487  wl-issetft  37563  fin2so  37594  ptrest  37606  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  poimirlem28  37635  poimirlem31  37638  poimirlem32  37639  heicant  37642  mblfinlem2  37645  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  itg2addnclem  37658  itg2addnclem3  37660  itg2addnc  37661  ftc1anc  37688  unirep  37701  sdclem2  37729  sdclem1  37730  sdc  37731  fdc  37732  isbnd  37767  heibor1lem  37796  heiborlem4  37801  heiborlem6  37803  heiborlem10  37807  ismgmOLD  37837  maxidlmax  38030  prnc  38054  isfldidl  38055  dmnnzd  38062  disjressuc2  38367  qsdisjALTV  38599  eqvrelqsel  38600  riotasvd  38942  lshpdisj  38973  lsat0cv  39019  lcvexchlem4  39023  lcvexchlem5  39024  lshpkrlem1  39096  lshpkrlem2  39097  lshpkrlem3  39098  lshpkrcl  39102  islshpkrN  39106  atnle  39303  glbconxN  39365  isline  39726  ispointN  39729  pmapglbx  39756  ispsubcl2N  39934  lhp2atnle  40020  cdleme43fsv1snlem  40407  cdleme40v  40456  cdlemkid5  40922  cdlemkid  40923  dvhb1dimN  40973  dib1dim  41152  dicopelval  41164  dicelval1sta  41174  diclspsn  41181  dihvalcqpre  41222  dihglblem2aN  41280  dihglblem2N  41281  dih1dimatlem  41316  dihpN  41323  dochfl1  41463  lcfl7N  41488  lcf1o  41538  hvmapvalvalN  41748  hdmapval2lem  41818  aks6d1c1  42097  aks6d1c4  42105  sticksstones10  42136  sticksstones12a  42138  aks6d1c7  42165  sn-iotalem  42202  f1o2d2  42214  fiabv  42517  evlsbagval  42547  selvvvval  42566  fsuppind  42571  absnw  42659  elrfi  42675  nacsfg  42686  mzpcompact2lem  42732  eldioph2b  42744  eldioph3  42747  eldiophss  42755  diophrex  42756  elnn0rabdioph  42784  rencldnfilem  42801  elpell1qr  42828  elpell14qr  42830  elpell1234qr  42832  jm2.27  42990  rmydioph  42996  expdiophlem2  43004  wepwsolem  43024  aomclem6  43041  lnr2i  43098  lpirlnr  43099  hbtlem2  43106  hbtlem4  43108  hbtlem5  43110  rngunsnply  43151  flcidc  43152  onsucelab  43245  limnsuc  43247  nnoeomeqom  43294  cantnfresb  43306  tfsconcatfv2  43322  tfsconcatb0  43326  oaun3lem1  43356  oadif1lem  43361  oadif1  43362  clcnvlem  43605  brtrclfv2  43709  frege55lem1c  43898  frege104  43949  clsk1indlem0  44023  clsk1indlem2  44024  clsk1indlem3  44025  clsk1indlem4  44026  clsk1indlem1  44027  pm13.192  44392  equncomVD  44850  csbingVD  44866  csbsngVD  44875  csbfv12gALTVD  44881  relopabVD  44883  refsum2cnlem1  45024  elrnmptf  45168  upbdrech  45296  ssfiunibd  45300  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  47847  dfclnbgr6  47849  dfnbgr6  47850  isuspgrim0  47887  isuspgrimlem  47888  clnbgrgrim  47927  usgrgrtrirex  47942  stgredgel  47949  stgrusgra  47951  stgr1  47953  grlimgrtri  47988  gpgiedgdmel  48033  gpgedgel  48034  gpgprismgr4cycllem10  48087  pgnbgreunbgrlem1  48096  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem4  48102  pgnbgreunbgr  48108  uspgrsprf1  48128  uspgrsprfo  48129  0nodd  48151  1odd  48152  2nodd  48153  0even  48218  1neven  48219  2even  48220  2zlidl  48221  2zrngamgm  48226  2zrngagrp  48230  2zrngmmgm  48233  2zrngnmrid  48237  suppmptcfin  48357  lcoval  48394  linc0scn0  48405  linc1  48407  el0ldep  48448  snlindsntor  48453  blenval  48553  nn0sumshdiglemB  48602  itcoval1  48645  mo0  48795  eloprab1st2nd  48849  oppcmndclem  48999  sectpropdlem  49018  invpropdlem  49020  isopropdlem  49022  upciclem1  49148  oppcup3lem  49188  isthincd2lem1  49407  termcbasmo  49465  isinito2lem  49480  arweuthinc  49511  arweutermc  49512  discsntermlem  49552  basrestermcfolem  49553