Theorem eleq2d 2850

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eleq2d	⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Proof of Theorem eleq2d

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1d.1	. . . 4 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dfcleq 2756	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	sylib 221	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		anbi2 646	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1866	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 18	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		dfclel 2840	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		dfclel 2840	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4g 317	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2147

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  eleq2  2853  eleq12d  2858  eleqtrd  2866  neleqtrd  2886  eqabrd  2905  raleqbidv  3338  rexeqbidv  3339  reueqbidv  3405  rabeqbidva  3432  elabd2  3627  sbcbid  3796  sbcbi2  3800  csbeq2d  3857  csbeq2dv  3858  cbvcsbw  3861  cbvcsb  3862  cbvcsbv  3863  csbie  3886  csbied  3887  csbie2g  3891  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  sbcel12  4372  sbcel1g  4377  sbcel2  4379  prel12g  4822  eliuni  4960  iuneqconst  4966  iuneq12df  4981  iuneq12d  4983  cbviun  4996  cbviin  4997  cbviung  4998  cbviing  4999  cbviunv  5000  cbviinv  5001  iinxsng  5051  iinxprg  5052  iunxsng  5053  iunxsngf  5055  cbvdisj  5083  cbvdisjv  5084  disjor  5088  disjiund  5097  mpteq12da  5191  mpteq12f  5193  mpteq12dva  5194  axpweq  5316  rabxfrd  5383  brab2d  5516  rbropapd  5541  opeliunxp  5722  opeliun2xp  5723  opeliunxp2  5820  iunxpf  5831  elimampt  6046  elrelimasn  6095  elimasni  6100  xpdifid  6170  xpdifcnvepel  6171  imadifssranOLDOLD  6215  ressn  6303  funfni  6664  fnbr  6666  dffv3  6901  elfv2ex  6948  fvelrnb  6965  foelcdmi  6966  fvun1  6996  fvco2  7002  funcnvmpt  7015  elfvmptrab1w  7041  elfvmptrab1  7042  elfvmptrab  7043  elpreima  7077  elpreimaOLD  7078  dff3  7121  fmptco  7151  fnelfp  7200  fnelnfp  7202  tpres  7227  fnprb  7234  fntpb  7235  funfvima3  7262  eluniima  7274  dff13  7278  f1ounsn  7300  f1eqcocnv  7329  isoini  7366  riotaeqdv  7398  mpoeq123dva  7514  cbvmpox  7533  elimampo  7578  ovelrn  7618  elovmpod  7686  elovmpo  7687  elovmporab  7688  elovmporab1w  7689  elovmporab1  7690  elovmpt3rab1  7702  fiun  7976  f1iun  7977  zfrep6OLD  7988  fmpox  8100  el2mpocsbcl  8118  el2mpocl  8119  bropopvvv  8123  bropfvvvv  8125  xpord2indlem  8188  xpord3inddlem  8195  elsuppfng  8211  elsuppfn  8212  suppfnss  8231  opeliunxp2f  8252  mpoxopn0yelv  8255  mpoxopovel  8262  rntpos  8281  mpocurryd  8311  fpr2  8347  wfr2  8370  onoviun  8376  smoel  8393  smoiso  8395  smoel2  8396  smo11  8397  tfrlem9  8418  oalimcl  8593  oaass  8594  omordi  8599  omordlim  8610  omlimcl  8611  odi  8612  omeulem1  8615  omeulem2  8616  oen0  8620  oeordi  8621  oeordsuc  8628  oelimcl  8634  oeeulem  8635  oeeui  8636  nnmordi  8665  oaabs2  8683  omabs  8685  omsmolem  8691  ereldm  8796  iiner  8835  elmapg  8884  elpmg  8888  curf  8915  uncf  8916  elixpsn  8990  ixpsnf1o  8991  boxriin  8993  omxpenlem  9122  pw2f1olem  9125  phplem2  9245  php3  9249  infn0  9319  elfi  9429  dffi3  9447  marypha2lem2  9452  ordiso2  9533  wemapsolem  9568  elharval  9579  inf3lemd  9652  inf3lem1  9653  inf3lem2  9654  inf3lem3  9655  cantnfs  9691  cantnfp1lem3  9705  cantnflem1b  9711  cantnflem1  9714  ttrclselem2  9751  trcl  9753  frr2  9788  r1sdom  9805  r1ordg  9809  r1pwss  9815  tz9.12lem3  9820  tz9.12  9821  r1elwf  9828  rankr1ai  9830  rankidb  9832  rankr1bg  9835  rankval2  9851  rankval2b  9859  rankelg  9876  rankunb  9888  tcrank  9925  r1filimi  9927  elhf2  9934  0hf  9941  acni  10148  acni2  10149  acndom  10154  infpwfien  10165  alephnbtwn  10174  cardaleph  10192  cardinfima  10200  iunfictbso  10217  dfac3  10224  dfac5lem5  10230  dfac5  10231  dfac9  10239  dfac12r  10249  kmlem2  10254  kmlem12  10264  kmlem13  10265  kmlem14  10266  ackbij2lem3  10342  ackbij2  10344  cofsmo  10371  alephsing  10378  fin23lem30  10444  isf32lem9  10463  itunisuc  10521  axcc2lem  10538  axcc3  10540  domtriomlem  10544  axdc2lem  10550  axdc2  10551  axdc3lem2  10553  axdc3lem4  10555  axdc4lem  10557  ac6c4  10583  zorn2lem1  10598  ttukeylem6  10616  pwcfsdom  10692  axregndlem2  10712  axinfndlem1  10714  axacndlem4  10719  axacnd  10721  pwfseqlem1  10767  inar1  10884  inatsk  10887  gruurn  10907  grur1  10929  eltskm  10952  genpelv  11109  eluz1  12993  elixx1  13509  elixx3g  13513  elioo2  13541  elfz1  13668  elfz2  13670  elfzp1  13732  fzpr  13737  fzsuc2  13740  fzrev3  13748  elfzp12  13761  fzm1  13765  elfzo  13819  fz0add1fz1  13894  elfzo0l  13915  elfzom1b  13925  fzosplitsni  13938  elfzr  13940  elfzlmr  13941  zmodidfzo  14064  seqp1  14183  seqf1o  14210  bcval  14472  bcpasc  14489  hashf1lem1  14624  fundmge2nop0  14671  wrdmap  14715  elovmpowrd  14727  ccatfval  14742  elfzelfzccat  14749  ccatlid  14756  ccatass  14758  ccatrn  14759  ccatf1  14760  ccatalpha  14764  swrdrn3  14827  swrdfv2  14836  ccatswrd  14843  swrdccat2  14844  pfxfv  14857  pfxeq  14870  ccatpfx  14875  swrdswrd  14879  swrdpfx  14881  pfxpfx  14882  cats1un  14895  swrdccatfn  14898  swrdccatin1  14899  pfxccatin12lem4  14900  pfxccatin12lem1  14902  swrdccatin2  14903  pfxccatin12lem2c  14904  pfxccatin12lem2  14905  swrdccat3blem  14913  swrdccatin1d  14917  swrdccatin2d  14918  pfxccatin12d  14919  revccat  14940  revrev  14941  revpfxsfxrev  14942  repswpfx  14961  repswccat  14962  cshwidxmod  14979  2cshw  14989  cshwcshid  15003  cshwcsh2id  15004  cshimadifsn  15005  cshimadifsn0  15006  revco  15010  ccatco  15011  cshco  15012  swrdco  15013  ofccat  15148  shftfn  15252  shftval  15253  limsupgle  15670  ello12  15709  elo12  15720  isercolllem3  15860  sumeq1  15882  fsumsplit  15933  sumsplit  15960  fsum2dlem  15962  fsumcom2  15966  fsumparts  15999  explecnv  16060  pwdif  16063  fprodser  16142  fprodsplit  16159  fprod2dlem  16173  fprodcom2  16177  eftlub  16303  divalgmod  16602  bitsval  16620  bitsp1e  16628  bitsp1o  16629  sadfval  16648  sadcp1  16651  sadval  16652  sadcadd  16654  sadadd2  16656  saddisjlem  16660  sadadd  16663  sadass  16667  smufval  16673  smuval  16677  smuval2  16678  smupvallem  16679  smu01lem  16681  smueqlem  16686  smumul  16689  bezoutlem2  16739  bezoutlem4  16741  algfx  16781  eucalgcvga  16787  reumodprminv  17008  nnnn0modprm0  17010  unbenlem  17112  prmreclem5  17124  vdwapval  17177  vdwapun  17178  vdwnnlem1  17199  vdwnn  17202  ramval  17212  0ram  17224  ramub1lem2  17231  prmgaplem7  17261  prmlem0  17309  elrest  17624  prdsbasmpt  17667  prdsleval  17674  prdsbasmpt2  17679  pwselbasb  17685  imasaddfnlem  17726  imasvscafn  17735  divsfval  17745  ismre  17786  mreunirn  17797  mrisval  17830  ismri  17831  isacs  17851  catidd  17880  iscatd2  17881  ismon  17934  isepi  17941  sectffval  17951  sectfval  17952  dfiso2  17973  cicsym  18005  issubc  18036  catsubcat  18040  isfunc  18065  funcres  18097  funcpropd  18103  ffthiso  18132  isnat  18151  isnat2  18152  fuciso  18179  initoval  18194  termoval  18195  isinito  18197  istermo  18198  iszeroo  18199  isinitoi  18200  istermoi  18201  initoid  18202  termoid  18203  iszeroi  18210  2initoinv  18211  initoeu1  18212  initoeu2  18217  2termoinv  18218  termoeu1  18219  arwhoma  18246  elsetchom  18282  setcmon  18288  setcepi  18289  setciso  18292  catciso  18312  elestrchom  18328  estrcbasbas  18331  funcestrcsetclem7  18346  funcestrcsetclem8  18347  funcestrcsetclem9  18348  fthestrcsetc  18350  fullestrcsetc  18351  equivestrcsetc  18352  setc1strwun  18353  funcsetcestrclem7  18361  funcsetcestrclem8  18362  funcsetcestrclem9  18363  fthsetcestrc  18365  fullsetcestrc  18366  hofcl  18459  hofpropd  18467  yonedalem4c  18477  yonedainv  18481  yonffthlem  18482  lubeldm  18551  glbeldm  18564  joindef  18574  meetdef  18588  poslubdg  18612  acsficl2d  18752  acsmapd  18754  psref  18774  psss  18780  dirge  18803  chnccats1  18825  chnccat  18826  chnrev  18827  mgmpropd  18855  issstrmgm  18857  grpidval  18866  grpidpropd  18868  grpidd  18878  imasmgm2  18889  ismgmhm  18911  issubmgm  18917  issgrpd  18945  sgrppropd  18946  ismndd  18972  mndpropd  18977  imasmnd2  18994  imasmnd  18995  xpsmnd0  18998  ismhm  19006  issubm  19024  gsumsgrpccat  19062  elefmndbas2  19096  smndex1mndlem  19134  imasgrp2  19291  imasgrp  19292  issubg  19362  subginv  19369  isnsg  19391  eqg0el  19424  quselbas  19425  isghm  19456  resghm2b  19474  conjnmzb  19493  conjnsg  19494  ghmpropd  19496  imasgim  19510  isga  19532  elcntz  19563  elcntzsn  19566  cntzrcl  19568  resscntz  19574  symgextf1  19662  gsmsymgreqlem2  19672  f1otrspeq  19688  pmtrfrn  19699  pmtrdifellem3  19719  pmtrdifellem4  19720  psgnunilem1  19734  psgnunilem5  19735  psgnunilem2  19736  psgnunilem3  19737  psgneldm2  19745  psgnfitr  19758  psgnsn  19761  gexdvds  19825  gex1  19832  isslw  19849  sylow3lem2  19869  lsmelvalx  19881  pj1ghm  19944  efgtlen  19967  efgsfo  19980  efgredlemc  19986  frgp0  20001  frgpmhm  20006  qusabl  20106  frgpnabllem1  20114  imasabl  20117  cycsubmcmn  20130  0cyg  20134  cycsubgcyg  20142  gsumval3  20148  gsumcllem  20149  gsumzaddlem  20162  gsumzsplit  20168  gsummptfzcl  20210  eldprd  20247  dprdcntz2  20281  dprd2d2  20287  dmdprdsplit2lem  20288  dmdprdsplit2  20289  dprdsplit  20291  ablfac2  20332  isrngd  20422  rngpropd  20423  imasrng  20426  qusrng  20429  ringurd  20438  isringd  20549  imasring  20587  xpsring1d  20590  dvdsrval  20618  isunit  20630  dvdsrpropd  20673  isirred  20676  isrnghm  20698  isrngim  20702  c0ghm  20718  c0snghm  20721  isrhm0  20733  isrhm  20736  isrim0  20740  crngrhmfo  20753  islring  20819  issubrng  20826  opprsubrng  20838  issubrg  20850  opprsubrg  20872  resrhm2b  20881  rhmpropd  20888  rnghmresel  20899  elrngchom  20903  rnghmsubcsetclem1  20910  rnghmsubcsetclem2  20911  rngcid  20914  rngcsect  20915  rngciso  20917  funcrngcsetcALT  20920  zrinitorngc  20921  zrtermorngc  20922  rhmresel  20928  elringchom  20932  rhmsubcsetclem1  20939  rhmsubcsetclem2  20940  ringcid  20943  rhmsscrnghm  20944  rhmsubcrngclem1  20945  rhmsubcrngclem2  20946  ringcsect  20949  ringciso  20951  ringcbasbas  20952  zrtermoringc  20954  srhmsubc  20959  rhmsubclem3  20966  rhmsubclem4  20967  drngunit  21012  isdrng4  21019  isdrngd  21049  isdrngdOLD  21051  issdrg  21072  sdrgunit  21080  isabv  21095  issrngd  21139  islmod  21166  lmodprop2d  21226  islss  21236  islssd  21237  lssats2  21302  ellspsn  21305  islmhm  21329  lmhmf1o  21348  lmhmima  21349  lmhmpreima  21350  reslmhm  21354  pwssplit3  21363  lmhmpropd  21375  islbs  21378  lspprel  21396  lspfixed  21433  lbsacsbs  21461  lbsextlem1  21463  lbsextlem2  21464  lbsextlem3  21465  lbsextlem4  21466  ixpsnbasval  21510  isridlrng  21525  rnglidlmmgm  21560  isridl  21572  quscrng  21606  rngqiprngimfolem  21613  rngqiprngimf1lem  21617  rngqiprngimfo  21624  isprmidl  21646  qsidomlem1  21663  qsidomlem2  21664  islpidl  21676  lidldvgen  21685  irinitoringc  21812  pzriprnglem13  21826  pzriprnglem14  21827  zrhrhmb  21843  znf1o  21884  frgpcyg  21906  psgnevpmb  21920  isphld  21987  phlssphl  21992  elocv  22001  iscss  22016  isobs  22053  obs2ss  22062  dsmmfi  22071  dsmmelbas  22072  dsmmlss  22077  frlmelbas  22089  frlmlbs  22130  frlmup1  22131  ellspd  22135  islinds  22142  islindf2  22147  f1lindf  22155  islindf4  22171  lindsdom  22183  lindsenlbs  22184  assamulgscmlem2  22235  psrgrp  22291  mplsubglem  22333  mpllsslem  22334  mplmonmul  22372  subrgascl  22402  subrgasclcl  22403  mpfind  22451  ismhp  22488  gsumply1subr  22578  lply1binomsc  22656  matbas2d  22765  matecl  22767  matvscl  22773  mat1  22789  mat0dim0  22809  mat0dimid  22810  mat0dimscm  22811  mat1dimelbas  22813  dmatel  22835  scmatel  22847  scmateALT  22854  scmataddcl  22858  scmatsubcl  22859  smatvscl  22866  scmatghm  22875  mat1scmat  22881  mdetunilem7  22960  mdetunilem9  22962  smadiadetr  23017  matunitlindflem1  23021  matunitlindflem2  23022  matunitlindf  23023  cramerimplem2  23029  cramer0  23035  pmatcoe1fsupp  23046  cpmatpmat  23055  cpmatel  23056  cpmatacl  23061  cpmatinvcl  23062  mat2pmatghm  23075  mat2pmatmul  23076  decpmatmullem  23116  pmatcollpwlem  23125  pmatcollpw3fi1lem1  23131  pmatcollpwscmatlem1  23134  monmat2matmon  23169  chfacfscmul0  23203  chfacfscmulgsum  23205  chfacfpmmulgsum  23209  cayhamlem1  23211  cpmadugsumlemB  23219  cpmadugsumlemC  23220  cpmadugsumlemF  23221  cayhamlem2  23229  istopon  23257  eltg  23302  eltg2  23303  eltop  23319  eltop2  23320  eltop3  23321  pptbas  23353  iscld  23372  neiss2  23446  isnei  23448  neiptopnei  23477  neiptopreu  23478  lpfval  23483  lpval  23484  islp  23485  maxlp  23492  islpi  23494  neitr  23525  restlp  23528  ordtbas2  23536  ordtrest2  23549  lmfval  23577  cnfval  23578  iscn  23580  iscnp  23582  tgcn  23597  tgcnp  23598  lmbrf  23605  cnpresti  23633  ist1  23666  ist1-2  23692  cnt1  23695  haust1  23697  cmpfi  23753  cmpfii  23754  1stcfb  23790  2ndc1stc  23796  1stcrest  23798  2ndcdisj  23802  1stcelcls  23807  nllyi  23821  subislly  23827  islocfin  23863  lfinpfin  23870  locfindis  23876  locfincf  23877  comppfsc  23878  kgenval  23881  elkgen  23882  kgencn2  23903  txbas  23913  eltx  23914  ptval  23916  ptpjpre1  23917  ptopn2  23930  ptpjopn  23958  ptclsg  23961  xkoccn  23965  txdis  23978  txdis1cn  23981  ptrescn  23985  hausdiag  23991  hauseqlcld  23992  txhaus  23993  xkohaus  23999  elqtop  24043  qtopeu  24062  kqcldsat  24079  hmeofval  24104  ptuncnv  24153  ptunhmeo  24154  elmptrab  24173  fbdmn0  24180  elfg  24217  elfilss  24222  filunirn  24228  fixufil  24268  elfm  24293  rnelfmlem  24298  rnelfm  24299  fmfnfmlem4  24303  elflim2  24310  flimtopon  24316  elflim  24317  hausflim  24327  flimcls  24331  flfnei  24337  isflf  24339  hausflf  24343  cnpflf  24347  cnflf  24348  txflf  24352  isfcls  24355  fclstopon  24358  isfcls2  24359  fclssscls  24364  fclsnei  24365  fclsfnflim  24373  flimfnfcls  24374  isfcf  24380  fcfelbas  24382  cnpfcf  24387  cnfcf  24388  flfcntr  24389  alexsublem  24390  alexsubALTlem3  24395  cnextfun  24410  cnextfvval  24411  cnextf  24412  cnextcn  24413  tmdgsum2  24442  tgpconncomp  24459  ghmcnp  24461  qustgplem  24467  eltsms  24479  haustsms  24482  tsmsgsum  24485  tsmssubm  24489  tsmssplit  24498  isust  24550  ustbas  24573  elutop  24579  ustuqtoplem  24585  ustuqtop4  24590  ustuqtop  24592  utopsnneiplem  24593  utopsnneip  24594  utopsnnei  24595  isusp  24607  isucn  24623  ucncn  24630  iscfilu  24633  neipcfilu  24641  iscusp  24644  cnextucn  24648  ispsmet  24650  ismet  24669  isxmet  24670  elblps  24733  elbl  24734  elmopn  24788  prdsbl  24837  neibl  24847  met1stc  24867  metrest  24870  prdsxmslem2  24875  txmetcnp  24893  txmetcn  24894  metustsym  24901  cfilucfil2  24907  elbl4  24909  metuel  24910  psmetutop  24913  restmetu  24916  metucn  24917  tngngp  25000  isnmhm  25092  zcld  25160  metnrmlem1a  25205  elcncf  25237  cncfcnvcn  25273  cnheibor  25303  lebnumlem1  25309  ishtpy  25320  isphtpy  25329  om1elbas  25380  elpi1  25393  pi1xfr  25403  pi1coghm  25409  tcphcph  25585  lmmbrf  25610  iscfil  25613  iscau  25624  iscauf  25628  caucfil  25631  iscmet  25632  cmetcaulem  25636  iscmet3lem1  25639  iscmet3lem2  25640  iscmet3  25641  bcthlem1  25672  cmsss  25699  cmetcusp1  25701  cmetcusp  25702  cmscsscms  25721  rrxcph  25740  minveclem3b  25776  ovolfioo  25815  ovolficc  25816  ovolctb  25838  ovoliunnul  25855  ovolshftlem1  25857  sca2rab  25860  ovolscalem1  25861  ovolicc2lem1  25865  ovolicc2lem2  25866  ovolicc2lem4  25868  ovolicc2lem5  25869  iundisj  25896  iunmbl2  25905  uniioombllem3  25933  vitalilem2  25957  vitalilem3  25958  mbfss  25994  i1faddlem  26041  i1fmullem  26042  mbfi1fseqlem2  26064  mbfi1fseqlem4  26066  mbfi1fseq  26069  itg2splitlem  26096  itg2split  26097  itg2monolem1  26098  itg2gt0  26108  isibl  26113  iblss2  26153  itgss3  26162  itgsplit  26183  ellimc  26220  limcmo  26229  cnlimc  26235  limciun  26241  limcun  26242  eldv  26245  dvbsss  26249  dvreslem  26256  elcpn  26281  dvaddf  26289  dvmulf  26290  dvcof  26295  rolle  26337  dvlip2  26342  dvivthlem1  26355  lhop1  26361  lhop2  26362  ftc1cn  26390  fta1glem2  26514  plyco0  26537  elply  26540  ply1termlem  26548  eltayl  26714  tayl0  26716  taylplem1  26717  taylplem2  26718  dvtaylp  26724  taylthlem1  26727  taylthlem2  26728  abelth  26795  cxpcn3  27103  rlimcnp  27320  fsumharmonic  27366  dchrelbas  27590  pntrsumbnd2  27921  ostth2lem2  27988  nolesgn2ores  28056  nogesgn1ores  28058  nosupprefixmo  28084  noinfprefixmo  28085  nosupcbv  28086  nosupdm  28088  nosupfv  28090  nosupres  28091  nosupbnd1lem1  28092  nosupbnd1lem3  28094  nosupbnd1lem5  28096  nosupbnd2lem1  28099  noinfcbv  28101  noinfdm  28103  noinffv  28105  noinfres  28106  noinfbnd1lem1  28107  noinfbnd1lem3  28109  noinfbnd1lem5  28111  noinfbnd2lem1  28114  elmade  28270  elold  28272  sltsleft  28273  sltsright  28274  oldlim  28300  madebday  28313  newbday  28315  ltslpss  28321  bdayiun  28328  cofcutr  28337  cofcutrtime  28340  lrrecval  28352  lrrecval2  28353  addsval  28375  precsexlem9  28628  precsexlem11  28630  ltonold  28674  onnolt  28679  onlts  28680  noseqrdgfn  28719  istrkgb  28944  istrkgcb  28945  istrkge  28946  istrkgl  28947  istrkgld  28948  axtgsegcon  28953  axtg5seg  28954  axtgbtwnid  28955  axtgpasch  28956  axtgupdim2  28960  axtgeucl  28961  tgsegconeu  28976  tgdim01  28997  iscgrg  29002  isismt  29024  tglnunirn  29038  tglngval  29041  tgellng  29043  legval  29074  legov  29075  legov2  29076  ishlg2  29092  ishlg  29095  mirreu3  29153  mirval  29154  mirfv  29155  mircgr  29156  mirbtwn  29157  ismir  29158  mireq  29164  symquadlem  29188  israg  29199  perpln1  29212  perpln2  29213  isperp  29214  islnopp  29242  outpasch  29260  ishpg  29264  tgplnfn  29280  plngval  29282  isplng  29283  elplng  29285  elplngid  29287  lnincplng  29289  plngcplem  29290  plngcp  29291  plngrot  29295  nhpmirhp  29303  lnperpexs  29337  iscgra  29343  dfcgra2  29365  ragraghl  29373  tgaaddcpbllem2  29377  tgaaddcpbl2  29380  isinag  29384  isleag  29393  cgrabasimass  29405  angmgmaddeu1  29406  angmgmval  29421  iseqlg  29439  brprlng  29443  prlnghpg  29451  prlngmo  29459  f1otrgitv  29474  f1otrg  29475  f1otrge  29476  ttgval  29479  ttgelitv  29487  elee  29498  brbtwn  29504  brcgr  29505  axlowdimlem16  29562  ebtwntg  29587  elntg2  29590  upgrex  29697  edgupgr  29739  upgredg  29742  edglnl  29748  numedglnl  29749  uhgr2edg  29816  umgr2edg1  29819  usgredg2vlem1  29833  usgredg2vlem2  29834  ushgredgedg  29837  ushgredgedgloop  29839  uhgrspansubgrlem  29898  fusgrfisstep  29937  nbgrval  29944  nbgrel  29948  nbupgrel  29953  nbgr2vtx1edg  29958  nbuhgr2vtx1edgblem  29959  nbuhgr2vtx1edgb  29960  nbusgreledg  29961  usgrnbcnvfv  29973  uvtxval  29995  uvtxel  29996  uvtx01vtx  30005  uvtxusgrel  30011  nbcplgr  30042  cplgr3v  30043  cusgrexi  30051  structtocusgr  30054  vtxdgfval  30075  vtxdg0v  30081  vtxdeqd  30085  vtxdun  30089  1loopgrnb0  30110  1loopgrvd0  30112  1hevtxdg0  30113  1hevtxdg1  30114  1egrvtxdg1  30117  umgr2v2evtxel  30130  umgr2v2enb1  30134  umgr2v2evd2  30135  vtxdginducedm1lem4  30150  vtxdginducedm1  30151  finsumvtxdg2sstep  30157  ewlksfval  30209  isewlk  30210  wksfval  30217  iswlk  30218  uspgr2wlkeq  30253  wlkres  30276  pfxwlk  30293  revwlk  30294  dfpth2  30341  usgr2pthlem  30376  clwlkcompim  30394  uspgrn2crct  30424  wwlks  30451  iswwlksn  30454  wwlknvtx  30461  wlkiswwlks2  30491  wwlksm1edg  30497  wwlksnred  30508  wwlksnext  30509  wwlksnredwwlkn  30511  wwlksnredwwlkn0  30512  wwlksnwwlksnon  30531  wspn0  30540  usgr2wspthons3  30583  rusgrnumwwlkb0  30590  clwwlk  30601  clwwlkccatlem  30607  clwlkclwwlklem2a4  30615  clwlkclwwlk  30620  clwwisshclwwslem  30632  clwwlkinwwlk  30658  clwwlkel  30664  clwwlkf  30665  clwwlkext2edg  30674  wwlksext2clwwlk  30675  wwlksubclwwlk  30676  clwwnisshclwwsn  30677  eleclclwwlknlem2  30679  erclwwlknsym  30688  erclwwlkntr  30689  umgrhashecclwwlk  30696  clwwlkvbij  30731  eupth2lem3lem3  30858  eupth2lem3lem4  30859  eupth2lem3lem6  30861  eupth2lemb  30865  eucrct2eupth  30873  fusgreg2wsplem  30961  2clwwlklem  30971  2clwwlk2clwwlklem  30974  2clwwlkel  30977  2clwwlk2clwwlk  30978  extwwlkfabel  30981  clwwlknonclwlknonf1o  30990  dlwwlknondlwlknonf1olem1  30992  numclwwlk2lem1  31004  numclwlk2lem2f  31005  numclwlk2lem2f1o  31007  ex-res  31069  isssp  31353  sspn  31365  islno  31382  isblo  31411  nmlno0  31424  ishmo  31440  dipdir  31471  dipass  31474  ubthlem1  31499  ubthlem2  31500  htthlem  31546  htth  31547  ocel  31910  ocnel  31927  shsel  31943  shsel2  31951  shmodsi  32018  pjhtheu  32023  pjeq  32028  axpjpj  32049  pjoc2  32068  elspani  32172  h1de2ctlem  32184  elspansn  32195  elspansn2  32196  elnlfn  32557  eleigvec  32586  riesz3i  32691  tgextancd  33095  cbviunf  33219  iuneq12daf  33220  iunrdx  33227  iunrnmptss  33228  cbvdisjf  33234  disjorf  33242  disjabrex  33245  disjabrexf  33246  iundisjf  33252  disjrdx  33254  fresunsn  33288  2ndresdju  33312  abfmpunirn  33315  abfmpeld  33317  abfmpel  33318  fmptcof2  33320  acunirnmpt2  33323  acunirnmpt2f  33324  aciunf1lem  33325  suppss3  33382  fpwrelmap  33392  xrofsup  33426  iundisjfi  33455  eliccioo  33564  s3f1  33578  ccatws1f1o  33581  ismnt  33611  mgcoval  33614  gsummpt2co  33676  gsumpart  33691  gsumhashmul  33695  gsummulsubdishift1  33696  xrge0tsmsbi  33702  gsumwrd2dccatlem  33705  gsumwrd2dccat  33706  cycpmco2  33761  cyc3co2  33768  isfxp  33796  cntrval2  33799  inftmrel  33808  isinftm  33809  isslmd  33830  urpropd  33858  elrgspn  33874  erlval  33886  rlocval  33887  rloccring  33899  rloc1r  33901  rlocisunit  33904  domnprodeq0  33907  domnpropd  33908  fracfld  33937  resv1r  33967  ellspds  33991  ellpi  33995  lbslsp  33999  rhmimaidl  34049  ismxidl  34054  crngmxidl  34061  drng0mxidl  34067  opprqus0g  34081  qsfld  34089  isrprm  34116  rsprprmprmidlb  34122  ressply1evls1  34164  ply1mulrtss  34181  ply1coedeg  34188  psrmonmul  34249  dimpropd  34308  lbslsat  34315  extdg1id  34365  fldextrspunlsplem  34372  fldextrspunlsp  34373  elirng  34385  ply1annidllem  34400  constrsuc  34437  constrconj  34444  constrllcllem  34451  constrlccllem  34452  constrcccllem  34453  nn0constr  34460  smatrcl  34495  smatcl  34501  ist0cld  34532  txomap  34533  locfinreflem  34539  zarclsiin  34570  zart0  34578  rhmpreimacnlem  34583  metidval  34589  cnre2csqima  34610  ordtrest2NEW  34622  fmcncfil  34630  fsumcvg4  34649  ofcfval  34797  measvuni  34914  meascnbl  34919  faeval  34946  ismbfm  34951  elunirnmbfm  34952  imambfm  34961  elcarsg  35004  itgeq12dv  35025  issibf  35032  eulerpartlems  35059  eulerpartlemgc  35061  eulerpartlemgvv  35075  eulerpartlemgu  35076  eulerpart  35081  rrvmbfm  35141  elorvc  35159  elorrvc  35163  dstfrvunirn  35174  ballotlemfc0  35192  ballotlemfcc  35193  ballotlemsima  35215  ballotlemrv  35219  fzssfzo  35238  signstfvn  35265  signstfvneq0  35268  signstres  35271  repr0  35307  reprinrn  35314  reprdifc  35323  hgt750lemg  35350  hgt750lemb  35352  istrkg2d  35362  axtgupdim2ALTV  35364  afsval  35370  brafs  35371  bnj945  35471  bnj1400  35532  bnj18eq1  35624  bnj916  35630  bnj1014  35658  bnj1015  35659  bnj1110  35679  bnj1417  35738  r1ssel  35813  ecscottd  35843  acnum  35846  onvf1odlem3  36032  vonf1wev  36035  vonf1owevOLD  36037  vonf1osev  36039  cplgredgex  36061  srepdflem2  36085  srepdf  36086  subfacp1lem2b  36112  subfacp1lem4  36114  subfacp1lem5  36115  subfacp1lem6  36116  ptpconn  36164  cvmscbv  36189  iscvm  36190  cvmsi  36196  cvmsval  36197  cvmliftmolem1  36212  cvmlift2lem12  36245  cvmlift2lem13  36246  cvmlift3lem7  36256  snmlval  36262  satfv1  36294  satfvsucsuc  36296  satfrnmapom  36301  satf0op  36308  satf0n0  36309  sat1el2xp  36310  fmlafvel  36316  isfmlasuc  36319  fmlaomn0  36321  gonan0  36323  goaln0  36324  gonar  36326  goalr  36328  satffunlem1lem2  36334  satffunlem2lem2  36337  satfv0fvfmla0  36344  satef  36347  satefvfmla0  36349  sategoelfvb  36350  satfv1fvfmla1  36354  mrsubfval  36439  mrsubvrs  36453  mclsrcl  36492  mclsval  36494  mppsval  36503  mclsppslem  36514  opelco3  36716  wsuclem  36764  funtransport  36973  fvtransport  36974  brcolinear  37001  colineardim1  37003  funray  37082  fvray  37083  funline  37084  fvline  37086  lineelsb2  37090  fwddifval  37104  fwddifnval  37105  rankeq1o  37109  nmulprop  37116  nmulr0  37121  nmuladdel  37138  ltnmul  37142  ltnadd  37144  rmoeqbidv  37179  disjeq12dv  37181  ixpeq12dv  37182  prodeq12sdv  37184  itgeq12sdv  37185  cbvralvw2  37192  cbvrexvw2  37193  cbvrmovw2  37194  cbvreuvw2  37195  cbvcsbvw2  37197  cbviunvw2  37198  cbviinvw2  37199  cbvmptvw2  37200  cbvdisjvw2  37201  cbvmpo1vw2  37209  cbvmpo2vw2  37210  cbvsbcdavw  37223  cbvcsbdavw  37225  cbvcsbdavw2  37226  cbviundavw  37228  cbviindavw  37229  cbvdisjdavw  37234  cbvrabdavw2  37251  cbviundavw2  37252  cbviindavw2  37253  cbvmptdavw2  37254  cbvdisjdavw2  37255  cbvriotadavw2  37256  cbvmpo1davw2  37258  cbvmpo2davw2  37259  cbvsumdavw2  37261  neibastop2lem  37325  neibastop3  37327  eltail  37339  ttctr  37458  dfttc2g  37471  mh-infprim2bi  37512  bj-projeq  38082  bj-projval  38086  bj-restsn  38193  opelopabbv  38255  brabd0  38259  bj-eldiag  38288  bj-eldiag2  38289  mptsnunlem  38452  dissneqlem  38454  iooelexlt  38476  relowlssretop  38477  rdgellim  38490  exrecfnlem  38493  finxpeq1  38500  finxpreclem6  38510  pibp21  38529  curunc  38716  unccur  38717  fin2so  38721  lindsadd  38727  ptrest  38728  ptrecube  38729  poimirlem2  38731  poimirlem8  38737  poimirlem17  38746  poimirlem18  38747  poimirlem20  38749  poimirlem21  38750  poimirlem22  38751  poimirlem24  38753  poimirlem26  38755  poimirlem29  38758  heicant  38764  mblfinlem1  38766  mblfinlem2  38767  volsupnfl  38774  itg2addnclem  38780  itg2gt0cn  38784  indexdom  38859  incsequz  38873  istotbnd  38894  istotbnd3  38896  0totbnd  38898  sstotbnd  38900  sstotbnd3  38901  isbnd  38905  prdstotbnd  38919  cntotbnd  38921  isismty  38926  heibor1lem  38934  heiborlem2  38937  heiborlem3  38938  heibor  38946  isass  38971  exidcl  39001  exidreslem  39002  elghomlem2OLD  39011  rngoidmlem  39061  rngo1cl  39064  divrngcl  39082  isdrngo2  39083  isrngohom  39090  isrngoiso  39103  isriscg  39109  iscom2  39120  iscringd  39123  isidl  39139  ispridl  39159  ismaxidl  39165  ac6s6  39295  dmecd  39433  dfpre4  39603  releldmqs  39866  releldmqscoss  39868  erimeq2  39886  qmapeldisjsim  39983  eldisjlem19  40036  membpartlem19  40037  prter3  40130  islshp  40227  islsat  40239  lcvfbr  40268  islfl  40308  ellkr  40337  islshpkrN  40368  ldual1dim  40414  isopos  40428  cmtfvalN  40458  cvrfval  40516  isat  40534  islln  40754  islpln  40778  islvol  40821  isline  40987  ispointN  40990  ispsubsp  40993  elpmap  41006  elpmapat  41012  elpadd  41047  paddclN  41090  elpclN  41140  elpcliN  41141  pclfinN  41148  pclcmpatN  41149  ispsubclN  41185  iswatN  41242  islhp  41244  islaut  41331  ispautN  41347  isldil  41358  isltrn  41367  isdilN  41402  istrnN  41405  istendo  42008  dvhb1dimN  42234  erng1lem  42235  erngdvlem4-rN  42247  diaelval  42281  diaeldm  42284  dia1dimid  42311  cdlemm10N  42366  dibopelvalN  42391  dibopelval2  42393  dibelval3  42395  dibelval1st  42397  dibelval2nd  42400  dibeldmN  42406  dibvalrel  42411  dibglbN  42414  dicffval  42422  dicfval  42423  dicopelval  42425  dicelvalN  42426  dicelval3  42428  dicvalrelN  42433  dicelval1sta  42435  diclspsn  42442  dihopelvalbN  42486  dihopelvalcqat  42494  dihopelvalcpre  42496  dihvalrel  42527  dih1  42534  dihmeetlem4preN  42554  dihmeetlem13N  42567  dih1dimatlem  42577  dochnel2  42640  dihjatcclem4  42669  dvh2dim  42693  dvh3dim  42694  dvh4dimN  42695  dochfln0  42725  lpolsetN  42730  islpolN  42731  lcfrvalsnN  42789  lcfrlem21  42811  lcfrlem27  42817  lcfrlem37  42827  lcfr  42833  lcdlss  42867  mapdcv  42908  hdmap1fval  43044  hdmapffval  43074  hdmapfval  43075  hdmapval  43076  hgmapffval  43133  hgmapfval  43134  hdmapellkr  43162  hlhilhillem  43208  fzsplitnd  43223  isprimroot  43334  primrootsunit1  43338  primrootscoprmpow  43340  primrootscoprbij  43343  aks6d1c1p2  43350  aks6d1c1p3  43351  aks6d1c1p4  43352  aks6d1c1p5  43353  aks6d1c1p6  43355  aks6d1c1  43357  evl1gprodd  43358  sticksstones11  43397  sticksstones12a  43398  rhmqusspan  43426  grpods  43435  fzosumm1  43492  frlmfielbas  43758  frlmsnic  43795  psrmnd  43798  prjspnnorm  43852  isnacs  43906  mrefg2  43909  elmzpcl  43928  mzpcompact2  43954  eldiophb  43959  elpell1qr  44045  elpell14qr  44047  elpell1234qr  44049  pw2f1ocnv  44235  pw2f1o2val2  44238  aomclem4  44250  aomclem6  44252  islssfg2  44264  lnr2i  44308  elmnc  44328  rngunsnply  44361  onexomgt  44433  onexlimgt  44435  onexoegt  44436  oaordnr  44488  omnord1  44497  oenord1  44508  cantnfresb  44516  tfsconcatun  44529  tfsconcat0i  44537  ofoaf  44547  naddcnff  44554  naddcnffo  44556  naddcnfcom  44558  naddcnfid1  44559  naddcnfid2  44560  naddcnfass  44561  naddwordnexlem4  44593  fiinfi  44764  sqrtcvallem1  44821  elintima  44843  eliunov2  44869  ov2ssiunov2  44890  brtrclfv2  44917  rfovcnvf1od  45194  rfovcnvfvd  45197  fsovrfovd  45199  fsovfvd  45200  fsovcnvlem  45203  ntrclsfv1  45245  ntrclselnel1  45247  ntrclsneine0lem  45254  ntrneifv1  45269  ntrneifv2  45270  ntrneiel  45271  gneispace2  45322  gneispacess2  45336  extoimad  45354  mnringelbased  45405  dvconstbi  45508  bccbc  45519  wfac8prim  46185  permaxrep  46189  permac8prim  46197  eliin2f  46322  iineq12dv  46324  rabbida2  46350  disjinfi  46410  unirnmap  46424  elmptima  46473  iuneqfzuzlem  46549  iooiinioc  46771  fsumiunss  46790  fsumsupp0  46793  lptre2pt  46853  icccncfext  47100  cncfiooicclem1  47106  dvnprodlem2  47160  stoweidlem27  47240  stoweidlem29  47242  stoweidlem31  47244  stoweidlem34  47247  stoweidlem48  47261  stoweidlem59  47272  dirkercncflem2  47317  dirkercncflem4  47319  fourierdlem2  47322  fourierdlem3  47323  fourierdlem25  47345  fourierdlem32  47352  fourierdlem33  47353  fourierdlem41  47361  fourierdlem48  47367  fourierdlem49  47368  fourierdlem62  47381  fourierdlem70  47389  fourierdlem80  47399  fourierdlem92  47411  fourierdlem93  47412  fourierdlem101  47420  etransclem37  47484  sge0val  47579  sge0f1o  47595  sge0iunmptlemre  47628  sge0iunmpt  47631  iundjiun  47673  caragenel  47708  ovncvrrp  47777  ovnsubaddlem1  47783  ovnsubadd  47785  hoidmvlelem2  47809  hoidmvlelem3  47810  hoidmvlelem4  47811  hoidmvle  47813  ovncvr2  47824  hspdifhsp  47829  hoiqssbl  47838  hspmbllem2  47840  hspmbl  47842  opnvonmbllem1  47845  isvonmbl  47851  ovnovollem1  47869  issmflem  47940  smflimlem3  47986  smflimlem4  47987  smflim  47990  smfmullem2  48005  smflimmpt  48023  smfsuplem1  48024  smflimsuplem1  48033  smflimsuplem3  48035  smflimsuplem4  48036  smflimsuplem7  48039  smflimsup  48041  chnsubseq  48093  tmachlem-agreeprod  48150  tmachlem-tpopen  48154  tmachlem-agreesn  48160  fcores  48340  fcoresf1  48342  afvelrnb  48436  afvelrnb0  48437  afv2co2  48530  el1fzopredsuc  48599  muldvdsfacm1  48660  iccpart  48701  iccpartgtprec  48705  iccpartiltu  48707  iccpartigtl  48708  iccpartltu  48710  iccpartgtl  48711  iccpartgt  48712  iccpartleu  48713  iccpartgel  48714  iccelpart  48718  iccpartiun  48719  icceuelpart  48721  fargshiftfv  48724  fargshiftfo  48727  sprel  48769  prprelb  48801  prprelprb  48802  nprmdvdsfacm1lem4  48911  fpprel  49029  sbgoldbo  49088  wtgoldbnnsum4prm  49103  bgoldbnnsum3prm  49105  bgoldbtbndlem3  49108  bgoldbtbnd  49110  clnbgrval  49123  elclnbgrelnbgr  49126  clnbgrel  49129  clnbupgrel  49135  vopnbgrel  49155  isubgredg  49167  upgrimwlklem3  49200  upgrimwlklem5  49202  upgrimpths  49210  grtriprop  49242  isgrtri  49244  grtriclwlk3  49246  stgredgel  49258  gpgvtxel  49348  gpgiedgdmel  49350  gpgedgel  49351  opgpgvtx  49356  gpg5nbgrvtx13starlem1  49372  gpg5nbgrvtx13starlem2  49373  gpg5nbgrvtx13starlem3  49374  gpg3kgrtriex  49390  grlimedgnedg  49432  upwlksfval  49436  isupwlk  49437  intop  49503  isclintop  49507  assintop  49509  isassintop  49510  assintopcllaw  49512  uzlidlring  49535  elrngchomALTV  49569  rngccatidALTV  49572  rngcsectALTV  49575  rngcisoALTV  49577  rhmsubcALTVlem3  49583  rhmsubcALTVlem4  49584  funcringcsetcALTV2lem7  49596  funcringcsetcALTV2lem9  49598  elringchomALTV  49603  ringccatidALTV  49606  ringcsectALTV  49609  ringcisoALTV  49611  ringcbasbasALTV  49612  funcringcsetclem7ALTV  49619  funcringcsetclem9ALTV  49621  srhmsubcALTV  49625  smprngprmrng  49639  cbvmpox2  49651  ply1sclrmsm  49699  dmatALTbasel  49717  lcoval  49727  lindslinindsimp1  49772  lindslinindsimp2  49778  lmod1  49807  elbigo  49866  elbigo2  49867  elbigolo1  49872  dig2nn0ld  49919  naryfvalel  49945  rrxlines  50049  rrxlinesc  50051  rrxlinec  50052  elrrx2linest2  50060  rrxsphere  50063  itsclc0  50086  itsclc0b  50087  itsclinecirc0  50088  itsclinecirc0b  50089  itscnhlinecirc02p  50100  brab2dd  50142  f1omo  50210  f1omoOLD  50211  lubeldm2d  50275  glbeldm2d  50276  catprs  50328  sectpropdlem  50353  nelsubc3lem  50387  initc  50409  imaid  50473  upfval  50495  upfval2  50496  upfval3  50497  uppropd  50500  oppcinito  50560  oppctermo  50561  oppczeroo  50562  initopropd  50568  termopropd  50569  isthinc  50757  isthincd2lem1  50763  thincmoALT  50767  thincmod  50768  isthincd  50774  thincpropd  50780  indcthing  50798  discthing  50799  prsthinc  50802  termcterm  50851  termc2  50856  isinito4  50888  2arwcatlem1  50936  setc1onsubc  50943  cnelsubcw  50944  parhomel  50947  ranval3  51017  lmdfval2  51041  cmdfval2  51042  termolmd  51056  elsetrecslem  51070