Theorem eqeq1 2764

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqeq1d 2762	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  eqeq1i  2765  eqtr  2780  eqtr2  2781  iseqsetvlem  2823  eqsb1  2886  cbvexeqsetf  3465  rexraleqim  3601  eqvincf  3604  pm13.183  3620  moeq  3665  mob  3675  euind  3682  reu2eqd  3694  reuind  3711  eqsbc1  3785  sbceqal  3800  csbhypf  3875  uniiunlem  4035  snjust  4583  elsng  4598  elprg  4607  reusngf  4635  rexreusng  4640  reuprg0  4663  rabrsn  4685  preq12bg  4813  intab  4938  uniintsn  4945  dfiun2g  4988  dfiin2g  4989  disji2  5087  disjprg  5099  unopab  5185  eusv1  5356  reusv2lem2  5364  reusv3  5370  axprg  5402  opthg  5453  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  propeqop  5484  euotd  5490  otiunsndisj  5497  elopabw  5504  solin  5590  elxpi  5677  opbrop  5753  relop  5830  ideqg  5831  dmopab2rex  5901  elrnmpt  5942  elrnmpt1  5944  elrnmptg  5945  restidsing  6049  somin1  6127  cnveqb  6190  reu3op  6290  reuop  6291  ordequn  6463  iotaval2  6504  funopg  6568  f0rn0  6761  fvelrnb  6939  fvmptg  6985  fndmin  7038  eldmrexrn  7085  foelrn  7101  foelrnf  7102  foco2  7103  fmptco  7124  funopsn  7145  funopsnOLD  7146  funsndifnop  7149  fmptsng  7167  fmptsnd  7168  tpres  7201  eufnfv  7229  elabrex  7240  elabrexg  7241  abrexco  7242  f1veqaeq  7254  fpropnf1  7265  nf1const  7306  isosolem  7349  f1oiso  7353  eusvobj2  7406  oprabidw  7445  oprabid  7446  f1opr  7470  oprabv  7474  0mpo0  7497  elrnmpog  7549  elrnmpo  7550  elrnmpores  7552  ralrnmpo  7553  ov3  7577  ov6g  7578  ovelrn  7591  caovcang  7616  caovcan  7619  caofidlcan  7717  uniuni  7762  orduninsuc  7840  funcnvuni  7930  fiunlem  7940  fiun  7941  f1iun  7942  f1oweALT  7970  opiota  8057  eloprabi  8061  mpof1o2d  8124  frxp  8125  funsssuppss  8189  dftpos4  8244  tz7.44-2  8397  tz7.44-3  8398  oev  8504  oalimcl  8550  omlimcl  8568  odi  8569  omeu  8575  oeeui  8593  nneob  8647  omopth  8653  eldifsucnn  8655  elqsg  8766  qsdisj  8797  qsel  8799  brecop  8813  eroveu  8815  erovlem  8816  elixpsn  8947  ixpsnf1o  8948  boxcutc  8951  2dom  9040  fundmen  9041  xpf1o  9140  nneneq  9203  fofinf1o  9302  elfi  9386  elfiun  9403  dffi3  9404  brwdom  9542  brwdom3  9557  unwdomg  9559  xpwdomg  9560  noinfep  9642  cantnfp1lem1  9660  cantnfp1lem3  9662  cantnflem1  9671  ssttrcl  9697  ttrclselem2  9708  scott0b  9879  scott0OLD  9880  updjudhcoinrg  9941  updjud  9942  carden2a  9974  cardiun  9990  pm54.43lem  10008  alephval3  10116  dfac5lem3  10131  dfac5lem4  10132  dfac2b  10136  kmlem9  10164  kmlem12  10167  cardcf  10256  cfeq0  10261  cfsuc  10262  cff1  10263  cflim2  10268  cfss  10270  isfin5  10304  fin1a2lem11  10415  fin1a2lem13  10417  brdom7disj  10537  brdom6disj  10538  canthp1lem2  10665  canthp1  10666  tskuni  10795  gruina  10830  genpv  11011  genpelv  11012  addsrmo  11085  mulsrmo  11086  ltsosr  11106  ltresr  11152  axcnre  11176  axpre-lttri  11177  ltordlem  11766  ltord1  11767  fimaxre3  12188  supaddc  12209  supadd  12210  supmul1  12211  supmullem1  12212  supmullem2  12213  supmul  12214  creur  12239  creui  12240  nn1m1nn  12281  elz  12620  nn0ind-raph  12724  xnegeq  13262  xmullem2  13320  xmulasslem  13340  f1resfz0f1d  13851  fleqceilz  13918  fseqsupubi  14045  sqeqor  14283  nn0opth2  14339  hash1snb  14487  hash2prde  14538  prprrab  14541  hash2pwpr  14544  tpf1ofv1  14565  tpf1ofv2  14566  tpfo  14568  fi1uzind  14575  wrd2ind  14795  cshfn  14864  cshf1  14884  2cshwcshw  14899  scshwfzeqfzo  14900  pfx2  15021  s3iunsndisj  15044  relexpsucnnr  15101  relexprelg  15114  rtrclreclem3  15136  shftfval  15146  sgnval  15164  sgn3da  15177  sgn0bi  15179  sgnnbi  15180  sgnpbi  15181  sgnmul  15183  01sqrexlem6  15337  reusq0  15555  summo  15806  fsum  15809  telfsumo  15892  infcvgaux1i  15949  infcvgaux2i  15950  mertenslem1  15976  mertenslem2  15977  mertens  15978  prodmo  16026  fprod  16031  ruclem12  16332  mod2eq1n2dvds  16440  divalg  16496  ndvdssub  16502  sadcp1  16548  smupp1  16573  gcdval  16589  bezoutlem1  16632  bezoutlem3  16634  bezoutlem4  16635  bezout  16636  lcmval  16685  coprmgcdb  16742  coprmdvds1  16745  divgcdcoprmex  16759  dvdsprime  16780  nprm  16781  dvdsprm  16797  coprm  16805  qnumval  16831  qdenval  16832  m1dvdsndvds  16893  reumodprminv  16899  pcval  16939  pceu  16941  pczpre  16942  pcdiv  16947  4sqlem2  17044  4sqlem4  17047  4sqlem12  17051  4sq  17059  vdwapval  17068  vdwapun  17069  vdwlem6  17081  cshwrepswhash1  17197  acsfn  17750  initoid  18093  termoid  18094  cat1lem  18188  posi  18408  gsumval2a  18790  smndex2dnrinv  19030  mgm2nsgrplem2  19034  mgm2nsgrplem3  19035  sgrp2nmndlem5  19044  mgmnsgrpex  19046  sgrpnmndex  19047  degenmgm2nfun  19055  cyccom  19334  ghmf1  19376  conjnmzb  19383  orbsta  19443  symgextfv  19548  symgextfo  19552  symgfixfo  19569  pmtrprfval  19617  pmtrprfvalrn  19618  psgneu  19636  psgnval  19637  psgnvali  19638  psgnvalii  19639  odfval  19662  odval  19664  dfod2  19694  submod  19699  isslw  19738  sylow2alem1  19747  sylow3lem2  19758  lsmelvalm  19781  lsmdisj2  19812  efgrelexlemb  19880  frgpup3lem  19907  cyggeninv  20013  gsumval3eu  20034  gsumval3lem2  20036  gsummpt1n0  20095  nn0gsumfz  20114  dprddisj2  20171  dpjrid  20194  pgpfac1lem3  20209  rrgeq0i  20864  domneq0  20873  domnlcanb  20884  domnrcanb  20886  abveq0  20987  abvtrivd  21001  lss1d  21150  lspsn  21189  ellspsn  21190  lspprel  21281  prmirredlem  21688  znf1o  21767  znfld  21776  znunit  21779  cygznlem3  21785  psgndif  21818  ipeq0  21854  obsip  21937  frlmphl  21997  uvcvval  22002  ellspd  22018  psrlidm  22179  psrridm  22180  psrascl  22196  mvrval2  22200  mvrf1  22203  mplmonmul  22255  evlslem3  22299  selvvvval  22361  mhpsclcl  22378  psdmplcl  22393  psdmul  22397  psdmvr  22400  coe1tm  22502  coe1tmfv2  22504  cply1coe0  22529  cply1coe0bi  22530  gsummoncoe1  22536  mamufacex  22621  mat1comp  22665  mat1dimelbas  22696  mat1dimid  22699  scmatel  22730  scmateALT  22737  mavmulsolcl  22776  marrepeval  22788  marepveval  22793  mdetunilem8  22844  maducoeval2  22865  madugsum  22868  minmar1eval  22874  symgmatr01lem  22878  symgmatr01  22879  gsummatr01lem3  22882  gsummatr01lem4  22883  gsummatr01  22884  m2cpm  22969  m2cpminvid2lem  22982  decpmatid  22998  monmatcollpw  23007  pmatcollpw3fi1lem1  23014  mp2pm2mplem4  23037  fvmptnn04ifc  23080  chfacffsupp  23084  chfacfscmul0  23086  chfacfscmulgsum  23088  chfacfpmmul0  23090  chfacfpmmulgsum  23092  cpmadumatpoly  23111  cayleyhamilton  23118  cayleyhamiltonALT  23119  istopon  23140  toponsspwpw  23150  fctop  23232  cctop  23234  ppttop  23235  pptbas  23236  epttop  23237  t0sep  23552  t1sep2  23597  cmpsublem  23627  cmpsub  23628  unisngl  23756  txuni2  23794  elpt  23801  ptbasfi  23810  xkoopn  23818  ptpjopn  23841  ptclsg  23844  dfac14lem  23846  ptcnp  23851  ptrescn  23868  tx1stc  23879  qtopeu  23945  kqt0lem  23965  isr0  23966  hauspwpwf1  24216  xmeteq0  24567  imasf1oxmet  24604  comet  24742  stdbdxmet  24744  met2ndci  24751  prdsxmslem2  24758  nrmmetd  24803  tngngp  24883  tngngp3  24885  xrsxmet  25039  iccpnfcnv  25175  iccpnfhmeo  25176  cnheibor  25186  elovolm  25706  ovolgelb  25711  ovolicc1  25747  ovolicc  25754  ioorval  25805  uniioombllem6  25819  dyadmax  25829  dyadmbl  25831  i1fadd  25926  i1fmul  25927  itg1addlem3  25929  i1fmulc  25934  itg2l  25960  itg2leub  25965  limcmpt  26113  limcco  26123  dvcobr  26176  deg1ldg  26320  ig1pval  26404  elply  26423  elply2  26424  coeval  26452  coe1termlem  26487  coe1term  26488  plyn0mulidp  26514  quotval  26525  plydivlem4  26529  plydivex  26530  vieta1  26547  aannenlem2  26568  aalioulem2  26572  abelthlem9  26679  logtayllem  26899  logtayl  26900  isosctrlem2  27059  leibpilem2  27181  rlimcnp2  27206  efrlim  27209  mpodvdsmulf1o  27433  dvdsmulf1o  27435  perfectlem2  27469  lgsfval  27541  lgsval2lem  27546  lgsqrmodndvds  27592  lgsdchrval  27593  gausslemma2dlem0i  27603  2lgslem1b  27631  2lgslem3  27643  2sqlem2  27657  2sqlem8  27665  2sqlem9  27666  2sqlem11  27668  addsq2reu  27679  dchrisum0flblem1  27747  padicval  27856  padicabv  27869  ostth1  27872  ltsval2  27895  ltsintdifex  27900  ltsres  27901  nolt02o  27934  madef  28104  addsval2  28231  addsproplem2  28238  addsproplem4  28240  addsproplem5  28241  addsproplem6  28242  addsprop  28244  addcuts  28246  leadds1  28257  addsuniflem  28269  addsunif  28270  addsasslem1  28271  addsasslem2  28272  addbdaylem  28285  negsprop  28303  negsid  28309  mulsval2lem  28378  mulsproplem9  28392  mulsproplem12  28395  mulsprop  28398  sltmuls1  28415  sltmuls2  28416  mulsuniflem  28417  addsdilem1  28419  addsdilem2  28420  mulsasslem1  28431  mulsasslem2  28432  mulsunif2  28438  precsexlemcbv  28474  precsexlem9  28483  precsexlem11  28485  n0s0suc  28610  onsfi  28624  n0s0m1  28630  nn1m1nns  28642  eucliddivs  28644  n0seo  28689  zseo  28690  expsval  28693  bdayfinbndcbv  28734  bdayfinbndlem1  28735  bdayfinbndlem2  28736  bdayfinbnd  28737  elz12s  28740  z12zsodd  28750  z12sge0  28751  recut  28762  elreno2  28763  renegscl  28766  readdscl  28767  remulscllem1  28768  remulscl  28770  axtgcgrid  28807  axtgbtwnid  28810  islmib  29174  inaghl  29246  axpaschlem  29400  axlowdimlem15  29416  axlowdim  29421  upgredg2vtx  29601  edglnl  29603  umgredgnlp  29607  usgredg2vtxeuALT  29685  uspgredg2v  29687  ushgredgedgloop  29694  nbusgredgeu  29829  cusgrfilem2  29919  cusgrfi  29921  vtxdushgrfvedg  29953  1loopgrvd2  29966  rusgr1vtxlem  30050  wlkeq  30096  wlkp1lem8  30141  upgrwlkdvdelem  30204  crctcshwlkn0lem6  30286  wlknwwlksnbij  30359  rusgrnumwwlkl1  30442  clwlkclwwlklem2a1  30465  clwwlknscsh  30535  eleclclwwlkn  30549  hashecclwwlkn1  30550  umgrhashecclwwlk  30551  clwwlknon1sn  30573  acycgrcycl  30635  frgr3vlem1  30756  3vfriswmgrlem  30760  frgrncvvdeqlem3  30784  wlkl0  30850  frgrreggt1  30876  nvz  31153  nmosetn0  31249  nmoolb  31255  nmoubi  31256  nmlno0lem  31277  nmlno0i  31278  hvsubeq0  31552  hvaddcan  31554  normsub0  31620  norm1exi  31734  pjhval  31881  omlsii  31887  omlsi  31888  pjoml  31920  h1de2ci  32040  spansneleq  32054  h1datomi  32065  h1datom  32066  spansncv  32137  5oalem6  32143  pj11  32198  nmopsetn0  32349  nmfnsetn0  32362  nmoplb  32391  nmopub  32392  nmfnlb  32408  nmfnleub  32409  nmlnop0iALT  32479  nmlnop0  32482  lnopeq  32493  nmopun  32498  nmcexi  32510  branmfn  32589  pjnmopi  32632  pj3i  32692  atss  32830  atom1d  32837  chirred  32879  cdj3lem2  32919  eqelbid  32953  elabreximd  32988  disjxpin  33064  disjunsn  33070  br8d  33084  fmptcof2  33133  psgnfzto1stlem  33543  sgnsval  33604  elrgspnlem2  33686  elrgspnlem3  33687  linds2eq  33817  elrspunsn  33860  mxidlmax  33871  1arithidomlem1  33948  1arithidom  33950  1arithufdlem1  33957  1arithufdlem2  33958  1arithufdlem3  33959  1arithufdlem4  33960  1arithufd  33961  dfufd2  33963  ply1dg1rt  33993  selvply1rhmlem2  34034  mplvrpmrhm  34060  psrmonmul  34063  esplyfvaln  34087  lbsdiflsp0  34139  fedgmullem1  34142  fedgmullem2  34143  rtelextdg2lem  34239  constrsuc  34251  constrcbvlem  34268  2sqr3minply  34293  madjusmdetlem2  34341  madjusmdet  34344  zarclssn  34386  xrge0iifcnv  34446  xrge0iifcv  34447  xrge0iifhom  34450  xrge0tmd  34458  xrge0tmdALT  34459  esumc  34564  signspval  35063  tgoldbachgt  35174  bnj1468  35358  fineqvnttrclselem3  35652  fineqvnttrclse  35653  sconnpi1  35821  cvmlift3lem2  35902  satfv0  35940  satfv1  35945  satfbrsuc  35948  satfrnmapom  35952  satfv0fun  35953  satf0op  35959  sat1el2xp  35961  fmlafvel  35967  fmla1  35969  isfmlasuc  35970  fmlaomn0  35972  gonan0  35974  goaln0  35975  gonar  35977  goalr  35979  fmla0disjsuc  35980  fmlasucdisj  35981  satffunlem1lem1  35984  satffunlem2lem1  35986  dmopab3rexdif  35987  satfv0fvfmla0  35995  sategoelfvb  36001  ex-sategoelel  36003  satfv1fvfmla1  36005  2goelgoanfmla1  36006  ex-sategoelelomsuc  36008  ex-sategoelel12  36009  prv1n  36013  ellcsrspsn  36223  r1peuqusdeg1  36225  br8  36338  br6  36339  br4  36340  rdgprc0  36373  dfrdg2  36375  dfbigcup2  36479  elsingles  36498  dfiota3  36503  brimageg  36507  brdomaing  36515  brrangeg  36516  dfrdg4  36533  elaltxp  36558  funtransport  36614  fvtransport  36615  brsegle  36691  funray  36723  fvray  36724  funline  36725  fvline  36727  ellines  36735  linethru  36736  rankeq1o  36754  subtr  36936  subtr2  36937  nn0prpw  36945  bj-elabd2ALT  37672  bj-gabss  37682  bj-imafv  38006  topdifinffinlem  38104  topdifinffin  38105  topdifinfeq  38107  finxpreclem2  38147  finxpreclem3  38150  fvineqsnf1  38167  fvineqsneu  38168  wl-ax12v2cl  38263  wl-dfclel  38272  wl-issetft  38348  fin2so  38364  ptrest  38371  poimirlem25  38397  poimirlem26  38398  poimirlem27  38399  poimirlem28  38400  poimirlem31  38403  poimirlem32  38404  heicant  38407  mblfinlem2  38410  mblfinlem3  38411  mblfinlem4  38412  ismblfin  38413  itg2addnclem  38423  itg2addnclem3  38425  itg2addnc  38426  ftc1anc  38453  unirep  38467  sdclem2  38495  sdclem1  38496  sdc  38497  fdc  38498  isbnd  38533  heibor1lem  38562  heiborlem4  38567  heiborlem6  38569  heiborlem10  38573  ismgmOLD  38603  maxidlmax  38796  prnc  38820  isfldidl  38821  dmnnzd  38828  disjressuc2  39162  qsdisjALTV  39450  eqvrelqsel  39451  riotasvd  39832  lshpdisj  39863  lsat0cv  39909  lcvexchlem4  39913  lcvexchlem5  39914  lshpkrlem1  39986  lshpkrlem2  39987  lshpkrlem3  39988  lshpkrcl  39992  islshpkrN  39996  atnle  40193  glbconxN  40254  isline  40615  ispointN  40618  pmapglbx  40645  ispsubcl2N  40823  lhp2atnle  40909  cdleme43fsv1snlem  41296  cdleme40v  41345  cdlemkid5  41811  cdlemkid  41812  dvhb1dimN  41862  dib1dim  42041  dicopelval  42053  dicelval1sta  42063  diclspsn  42070  dihvalcqpre  42111  dihglblem2aN  42169  dihglblem2N  42170  dih1dimatlem  42205  dihpN  42212  dochfl1  42352  lcfl7N  42377  lcf1o  42427  hvmapvalvalN  42637  hdmapval2lem  42707  aks6d1c1  42985  aks6d1c4  42993  sticksstones10  43024  sticksstones12a  43026  aks6d1c7  43053  sn-iotalem  43094  fiabv  43421  evlsbagval  43435  fsuppind  43439  absnw  43527  elrfi  43542  nacsfg  43553  mzpcompact2lem  43599  eldioph2b  43611  eldioph3  43614  eldiophss  43622  diophrex  43623  elnn0rabdioph  43647  rencldnfilem  43664  elpell1qr  43691  elpell14qr  43693  elpell1234qr  43695  jm2.27  43852  rmydioph  43858  expdiophlem2  43866  wepwsolem  43886  aomclem6  43903  lnr2i  43960  lpirlnr  43961  hbtlem2  43968  hbtlem4  43970  hbtlem5  43972  rngunsnply  44013  flcidc  44014  onsucelab  44107  limnsuc  44109  nnoeomeqom  44156  cantnfresb  44168  tfsconcatfv2  44184  tfsconcatb0  44188  oaun3lem1  44218  oadif1lem  44223  oadif1  44224  clcnvlem  44466  brtrclfv2  44570  frege55lem1c  44759  frege104  44810  clsk1indlem0  44884  clsk1indlem2  44885  clsk1indlem3  44886  clsk1indlem4  44887  clsk1indlem1  44888  pm13.192  45237  equncomVD  45693  csbingVD  45709  csbsngVD  45718  csbfv12gALTVD  45724  relopabVD  45726  refsum2cnlem1  45874  elrnmptf  46016  upbdrech  46141  ssfiunibd  46145  iccshift  46351  iooshift  46355  fsumf1of  46407  limcperiod  46461  climinf2mpt  46545  climinfmpt  46546  cncfshiftioo  46723  itgiccshift  46811  itgperiod  46812  stoweidlem46  46877  fourierdlem29  46967  fourierdlem37  46975  fourierdlem48  46985  fourierdlem51  46988  fourierdlem54  46991  fourierdlem62  46999  fourierdlem79  47016  fourierdlem81  47018  fourierdlem82  47019  fourierdlem92  47029  fourierdlem96  47033  fourierdlem97  47034  fourierdlem98  47035  fourierdlem99  47036  fourierdlem103  47040  fourierdlem104  47041  fourierdlem105  47042  fourierdlem108  47045  fourierdlem110  47047  fourierdlem112  47049  etransclem1  47066  etransclem5  47070  etransclem17  47082  etransclem32  47097  etransclem41  47106  sge0f1o  47213  sge0resplit  47237  sge0fodjrnlem  47247  nnfoctbdjlem  47286  nnfoctbdj  47287  ovnval  47372  ovnlecvr  47389  ovnpnfelsup  47390  ovn0lem  47396  hoidmvval  47408  hoidmvlelem1  47426  ovnhoilem1  47432  ovnhoi  47434  ovnlecvr2  47441  hoidifhspval3  47450  hspmbllem2  47458  hoimbl  47462  ovnsubadd2  47477  ovolval5lem2  47484  ovolval5lem3  47485  ovolval5  47486  ovnovol  47490  sinnpoly  47762  fsetsnf  47942  fsetsnfo  47944  fcoresf1  47960  aiotaval  47986  euoreqb  48000  afv0fv0  48040  afvfv0bi  48043  afvelrnb  48054  afvelrnb0  48055  afv20defat  48123  otiunsndisjX  48170  fun2dmnopgexmpl  48175  2ffzoeq  48219  modmkpkne  48258  elsetpreimafvb  48287  imasetpreimafvbijlemfo  48308  fargshiftf1  48344  fargshiftfo  48345  ichnreuop  48375  ichreuopeq  48376  elsprel  48378  spr0nelg  48379  sprel  48387  prelspr  48389  sprsymrelf1lem  48394  sprsymrelfolem2  48396  paireqne  48414  prprelb  48419  prprelprb  48420  reupr  48425  reuopreuprim  48429  fmtnoprmfac1lem  48470  fmtnofac2  48475  m1expevenALTV  48566  odd2np1ALTV  48593  opoeALTV  48602  opeoALTV  48603  perfectALTVlem2  48641  isgbe  48670  isgbow  48671  isgbo  48672  sbgoldbalt  48700  sgoldbeven3prm  48702  mogoldbb  48704  nnsum3primesgbe  48711  nnsum3primesle9  48713  nnsum4primesodd  48715  nnsum4primesoddALTV  48716  vopnbgrel  48773  dfclnbgr6  48775  dfnbgr6  48776  isuspgrim0  48813  isuspgrimlem  48814  clnbgrgrim  48853  usgrgrtrirex  48869  stgredgel  48876  stgrusgra  48878  stgr1  48880  grlimgrtri  48922  gpgiedgdmel  48968  gpgedgel  48969  gpgprismgr4cycllem10  49023  pgnbgreunbgrlem1  49032  pgnbgreunbgrlem2lem1  49033  pgnbgreunbgrlem2lem2  49034  pgnbgreunbgrlem4  49038  pgnbgreunbgr  49044  uspgrsprf1  49066  uspgrsprfo  49067  0nodd  49088  1odd  49089  2nodd  49090  0even  49155  1neven  49156  2even  49157  2zlidl  49158  2zrngamgm  49163  2zrngagrp  49167  2zrngmmgm  49170  2zrngnmrid  49174  idomnzd  49264  suppmptcfin  49309  lcoval  49345  linc0scn0  49356  linc1  49358  el0ldep  49399  snlindsntor  49404  blenval  49504  nn0sumshdiglemB  49553  itcoval1  49596  mo0  49745  eloprab1st2nd  49799  oppcmndclem  49946  sectpropdlem  49965  invpropdlem  49967  isopropdlem  49969  upciclem1  50095  oppcup3lem  50135  isthincd2lem1  50354  termcbasmo  50412  isinito2lem  50427  arweuthinc  50458  arweutermc  50459  discsntermlem  50499  basrestermcfolem  50500  nellindf  50806