Theorem eleq2d 2851

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 2758	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	sylib 221	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		anbi2 646	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1866	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 18	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		dfclel 2841	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		dfclel 2841	. 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 2146

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-8 2148  ax-9 2156  ax-ext 2737

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

This theorem is used by:  eleq2  2854  eleq12d  2859  eleqtrd  2867  neleqtrd  2887  eqabrd  2906  raleqbidv  3340  rexeqbidv  3341  reueqbidv  3407  rabeqbidva  3434  elabd2  3631  sbcbid  3800  sbcbi2  3804  csbeq2d  3860  csbeq2dv  3861  cbvcsbw  3864  cbvcsb  3865  cbvcsbv  3866  csbie  3889  csbied  3890  csbie2g  3894  cbvralcsf  3896  cbvreucsf  3898  cbvrabcsf  3899  sbcel12  4376  sbcel1g  4381  sbcel2  4383  prel12g  4831  eliuni  4964  iuneqconst  4970  iuneq12df  4985  iuneq12d  4988  cbviun  5001  cbviin  5002  cbviung  5003  cbviing  5004  cbviunv  5005  cbviinv  5006  iinxsng  5056  iinxprg  5057  iunxsng  5058  iunxsngf  5060  cbvdisj  5088  cbvdisjv  5089  disjor  5093  disjiund  5102  mpteq12da  5196  mpteq12f  5198  mpteq12dva  5199  axpweq  5323  rabxfrd  5390  brab2d  5524  rbropapd  5549  opeliunxp  5730  opeliun2xp  5731  opeliunxp2  5826  iunxpf  5836  elimampt  6047  elrelimasn  6090  elimasni  6095  xpdifid  6167  xpdifcnvepel  6168  imadifssranOLD  6205  ressn  6290  funfni  6645  fnbr  6647  dffv3  6881  elfv2ex  6928  fvelrnb  6945  foelcdmi  6946  fvun1  6976  fvco2  6982  funcnvmpt  6995  elfvmptrab1w  7021  elfvmptrab1  7022  elfvmptrab  7023  elpreima  7057  dff3  7099  fmptco  7129  fnelfp  7179  fnelnfp  7181  tpres  7206  fnprb  7213  fntpb  7214  funfvima3  7241  eluniima  7253  dff13  7257  f1ounsn  7279  f1eqcocnv  7308  isoini  7345  riotaeqdv  7377  mpoeq123dva  7493  cbvmpox  7512  elimampo  7556  ovelrn  7596  elovmpod  7664  elovmpo  7665  elovmporab  7666  elovmporab1w  7667  elovmporab1  7668  elovmpt3rab1  7680  fiun  7946  f1iun  7947  zfrep6OLD  7958  fmpox  8070  el2mpocsbcl  8086  el2mpocl  8087  bropopvvv  8091  bropfvvvv  8093  xpord2indlem  8149  xpord3inddlem  8156  elsuppfng  8171  elsuppfn  8172  suppfnss  8191  opeliunxp2f  8212  mpoxopn0yelv  8215  mpoxopovel  8222  rntpos  8241  mpocurryd  8271  fpr2  8307  wfr2  8330  onoviun  8336  smoel  8353  smoiso  8355  smoel2  8356  smo11  8357  tfrlem9  8378  oalimcl  8551  oaass  8552  omordi  8557  omordlim  8568  omlimcl  8569  odi  8570  omeulem1  8573  omeulem2  8574  oen0  8578  oeordi  8579  oeordsuc  8586  oelimcl  8592  oeeulem  8593  oeeui  8594  nnmordi  8623  oaabs2  8641  omabs  8643  omsmolem  8649  ereldm  8754  iiner  8793  elmapg  8842  elpmg  8846  elixpsn  8941  ixpsnf1o  8942  boxriin  8944  omxpenlem  9073  pw2f1olem  9076  phplem2  9196  php3  9200  infn0  9269  elfi  9380  dffi3  9398  marypha2lem2  9403  ordiso2  9484  wemapsolem  9519  elharval  9530  inf3lemd  9603  inf3lem1  9604  inf3lem2  9605  inf3lem3  9606  cantnfs  9642  cantnfp1lem3  9656  cantnflem1b  9662  cantnflem1  9665  ttrclselem2  9702  trcl  9704  frr2  9739  r1sdom  9753  r1ordg  9757  r1pwss  9763  tz9.12lem3  9768  tz9.12  9769  r1elwf  9775  rankr1ai  9777  rankidb  9779  rankr1bg  9782  rankval2  9797  rankunb  9829  tcrank  9863  acni  10045  acni2  10046  acndom  10051  infpwfien  10062  alephnbtwn  10071  cardaleph  10089  cardinfima  10097  iunfictbso  10114  dfac3  10121  dfac5lem5  10127  dfac5  10128  dfac9  10136  dfac12r  10146  kmlem2  10151  kmlem12  10161  kmlem13  10162  kmlem14  10163  ackbij2lem3  10239  ackbij2  10241  cofsmo  10268  alephsing  10275  fin23lem30  10341  isf32lem9  10360  itunisuc  10418  axcc2lem  10435  axcc3  10437  domtriomlem  10441  axdc2lem  10447  axdc2  10448  axdc3lem2  10450  axdc3lem4  10452  axdc4lem  10454  ac6c4  10480  zorn2lem1  10495  ttukeylem6  10513  pwcfsdom  10587  axregndlem2  10607  axinfndlem1  10609  axacndlem4  10614  axacnd  10616  pwfseqlem1  10662  inar1  10779  inatsk  10782  gruurn  10802  grur1  10824  eltskm  10847  genpelv  11004  eluz1  12886  elixx1  13401  elixx3g  13405  elioo2  13433  elfz1  13560  elfz2  13562  elfzp1  13623  fzpr  13628  fzsuc2  13631  fzrev3  13639  elfzp12  13652  fzm1  13656  elfzo  13710  fz0add1fz1  13785  elfzo0l  13806  elfzom1b  13816  fzosplitsni  13829  elfzr  13831  elfzlmr  13832  zmodidfzo  13955  seqp1  14074  seqf1o  14101  bcval  14362  bcpasc  14379  hashf1lem1  14514  fundmge2nop0  14561  wrdmap  14605  elovmpowrd  14617  ccatfval  14632  elfzelfzccat  14639  ccatlid  14646  ccatass  14648  ccatrn  14649  ccatf1  14650  ccatalpha  14654  swrdrn3  14716  swrdfv2  14725  ccatswrd  14732  swrdccat2  14733  pfxfv  14746  pfxeq  14759  ccatpfx  14764  swrdswrd  14768  swrdpfx  14770  pfxpfx  14771  cats1un  14784  swrdccatfn  14787  swrdccatin1  14788  pfxccatin12lem4  14789  pfxccatin12lem1  14791  swrdccatin2  14792  pfxccatin12lem2c  14793  pfxccatin12lem2  14794  swrdccat3blem  14802  swrdccatin1d  14806  swrdccatin2d  14807  pfxccatin12d  14808  revccat  14829  revrev  14830  revpfxsfxrev  14831  repswpfx  14850  repswccat  14851  cshwidxmod  14868  2cshw  14878  cshwcshid  14892  cshwcsh2id  14893  cshimadifsn  14894  cshimadifsn0  14895  revco  14899  ccatco  14900  cshco  14901  swrdco  14902  ofccat  15034  shftfn  15138  shftval  15139  limsupgle  15556  ello12  15595  elo12  15606  isercolllem3  15746  sumeq1  15768  fsumsplit  15819  sumsplit  15846  fsum2dlem  15848  fsumcom2  15852  fsumparts  15885  explecnv  15946  pwdif  15949  fprodser  16030  fprodsplit  16047  fprod2dlem  16061  fprodcom2  16065  eftlub  16191  divalgmod  16490  bitsval  16508  bitsp1e  16516  bitsp1o  16517  sadfval  16536  sadcp1  16539  sadval  16540  sadcadd  16542  sadadd2  16544  saddisjlem  16548  sadadd  16551  sadass  16555  smufval  16561  smuval  16565  smuval2  16566  smupvallem  16567  smu01lem  16569  smueqlem  16574  smumul  16577  bezoutlem2  16624  bezoutlem4  16626  algfx  16664  eucalgcvga  16670  reumodprminv  16890  nnnn0modprm0  16892  unbenlem  16994  prmreclem5  17006  vdwapval  17059  vdwapun  17060  vdwnnlem1  17081  vdwnn  17084  ramval  17094  0ram  17106  ramub1lem2  17113  prmgaplem7  17143  prmlem0  17191  elrest  17506  prdsbasmpt  17549  prdsleval  17556  prdsbasmpt2  17561  pwselbasb  17567  imasaddfnlem  17608  imasvscafn  17617  divsfval  17627  ismre  17668  mreunirn  17679  mrisval  17712  ismri  17713  isacs  17733  catidd  17762  iscatd2  17763  ismon  17816  isepi  17823  sectffval  17833  sectfval  17834  dfiso2  17855  cicsym  17887  issubc  17918  catsubcat  17922  isfunc  17947  funcres  17979  funcpropd  17985  ffthiso  18014  isnat  18033  isnat2  18034  fuciso  18061  initoval  18076  termoval  18077  isinito  18079  istermo  18080  iszeroo  18081  isinitoi  18082  istermoi  18083  initoid  18084  termoid  18085  iszeroi  18092  2initoinv  18093  initoeu1  18094  initoeu2  18099  2termoinv  18100  termoeu1  18101  arwhoma  18128  elsetchom  18164  setcmon  18170  setcepi  18171  setciso  18174  catciso  18194  elestrchom  18210  estrcbasbas  18213  funcestrcsetclem7  18228  funcestrcsetclem8  18229  funcestrcsetclem9  18230  fthestrcsetc  18232  fullestrcsetc  18233  equivestrcsetc  18234  setc1strwun  18235  funcsetcestrclem7  18243  funcsetcestrclem8  18244  funcsetcestrclem9  18245  fthsetcestrc  18247  fullsetcestrc  18248  hofcl  18341  hofpropd  18349  yonedalem4c  18359  yonedainv  18363  yonffthlem  18364  lubeldm  18433  glbeldm  18446  joindef  18456  meetdef  18470  poslubdg  18494  acsficl2d  18634  acsmapd  18636  psref  18656  psss  18662  dirge  18685  chnccats1  18707  chnccat  18708  chnrev  18709  mgmpropd  18737  issstrmgm  18739  grpidval  18748  grpidpropd  18749  grpidd  18759  ismgmhm  18790  issubmgm  18796  issgrpd  18824  sgrppropd  18825  ismndd  18851  mndpropd  18856  imasmnd2  18873  imasmnd  18874  xpsmnd0  18877  ismhm  18884  issubm  18902  gsumsgrpccat  18940  elefmndbas2  18974  smndex1mndlem  19012  imasgrp2  19169  imasgrp  19170  issubg  19240  subginv  19247  isnsg  19269  eqg0el  19302  quselbas  19303  isghm  19334  resghm2b  19352  conjnmzb  19371  conjnsg  19372  ghmpropd  19374  isga  19409  elcntz  19440  elcntzsn  19443  cntzrcl  19445  resscntz  19451  symgextf1  19539  gsmsymgreqlem2  19549  f1otrspeq  19565  pmtrfrn  19576  pmtrdifellem3  19596  pmtrdifellem4  19597  psgnunilem1  19611  psgnunilem5  19612  psgnunilem2  19613  psgnunilem3  19614  psgneldm2  19622  psgnfitr  19635  psgnsn  19638  gexdvds  19702  gex1  19709  isslw  19726  sylow3lem2  19746  lsmelvalx  19758  pj1ghm  19821  efgtlen  19844  efgsfo  19857  efgredlemc  19863  frgp0  19878  frgpmhm  19883  qusabl  19983  frgpnabllem1  19991  imasabl  19994  cycsubmcmn  20007  0cyg  20011  cycsubgcyg  20019  gsumval3  20025  gsumcllem  20026  gsumzaddlem  20039  gsumzsplit  20045  gsummptfzcl  20087  eldprd  20124  dprdcntz2  20158  dprd2d2  20164  dmdprdsplit2lem  20165  dmdprdsplit2  20166  dprdsplit  20168  ablfac2  20209  isrngd  20299  rngpropd  20300  imasrng  20303  qusrng  20306  ringurd  20315  isringd  20424  imasring  20462  xpsring1d  20465  dvdsrval  20493  isunit  20505  dvdsrpropd  20548  isirred  20551  isrnghm  20573  isrngim  20577  c0ghm  20593  c0snghm  20596  isrhm0  20608  isrhm  20611  isrim0  20615  crngrhmfo  20628  islring  20693  issubrng  20700  opprsubrng  20712  issubrg  20724  opprsubrg  20746  resrhm2b  20755  rhmpropd  20762  rnghmresel  20773  elrngchom  20777  rnghmsubcsetclem1  20784  rnghmsubcsetclem2  20785  rngcid  20788  rngcsect  20789  rngciso  20791  funcrngcsetcALT  20794  zrinitorngc  20795  zrtermorngc  20796  rhmresel  20802  elringchom  20806  rhmsubcsetclem1  20813  rhmsubcsetclem2  20814  ringcid  20817  rhmsscrnghm  20818  rhmsubcrngclem1  20819  rhmsubcrngclem2  20820  ringcsect  20823  ringciso  20825  ringcbasbas  20826  zrtermoringc  20828  srhmsubc  20833  rhmsubclem3  20840  rhmsubclem4  20841  drngunit  20886  isdrng4  20893  isdrngd  20922  isdrngdOLD  20924  issdrg  20945  sdrgunit  20953  isabv  20968  issrngd  21012  islmod  21039  lmodprop2d  21099  islss  21109  islssd  21110  lssats2  21175  ellspsn  21178  islmhm  21202  lmhmf1o  21221  lmhmima  21222  lmhmpreima  21223  reslmhm  21227  pwssplit3  21236  lmhmpropd  21248  islbs  21251  lspprel  21269  lspfixed  21306  lbsacsbs  21334  lbsextlem1  21336  lbsextlem2  21337  lbsextlem3  21338  lbsextlem4  21339  ixpsnbasval  21383  isridlrng  21398  rnglidlmmgm  21433  isridl  21445  quscrng  21477  rngqiprngimfolem  21484  rngqiprngimf1lem  21488  rngqiprngimfo  21495  isprmidl  21517  qsidomlem1  21534  qsidomlem2  21535  islpidl  21547  lidldvgen  21556  irinitoringc  21683  pzriprnglem13  21697  pzriprnglem14  21698  zrhrhmb  21714  znf1o  21755  frgpcyg  21777  psgnevpmb  21791  isphld  21858  phlssphl  21863  elocv  21872  iscss  21887  isobs  21924  obs2ss  21933  dsmmfi  21942  dsmmelbas  21943  dsmmlss  21948  frlmelbas  21960  frlmlbs  22001  frlmup1  22002  ellspd  22006  islinds  22013  islindf2  22018  f1lindf  22026  islindf4  22042  assamulgscmlem2  22104  psrgrp  22160  mplsubglem  22202  mpllsslem  22203  mplmonmul  22241  subrgascl  22271  subrgasclcl  22272  mpfind  22320  ismhp  22357  gsumply1subr  22447  lply1binomsc  22525  matbas2d  22634  matecl  22636  matvscl  22642  mat1  22658  mat0dim0  22678  mat0dimid  22679  mat0dimscm  22680  mat1dimelbas  22682  dmatel  22704  scmatel  22716  scmateALT  22723  scmataddcl  22727  scmatsubcl  22728  smatvscl  22735  scmatghm  22744  mat1scmat  22750  mdetunilem7  22829  mdetunilem9  22831  smadiadetr  22886  cramerimplem2  22895  cramer0  22901  pmatcoe1fsupp  22912  cpmatpmat  22921  cpmatel  22922  cpmatacl  22927  cpmatinvcl  22928  mat2pmatghm  22941  mat2pmatmul  22942  decpmatmullem  22982  pmatcollpwlem  22991  pmatcollpw3fi1lem1  22997  pmatcollpwscmatlem1  23000  monmat2matmon  23035  chfacfscmul0  23069  chfacfscmulgsum  23071  chfacfpmmulgsum  23075  cayhamlem1  23077  cpmadugsumlemB  23085  cpmadugsumlemC  23086  cpmadugsumlemF  23087  cayhamlem2  23095  istopon  23123  eltg  23168  eltg2  23169  eltop  23185  eltop2  23186  eltop3  23187  pptbas  23219  iscld  23238  neiss2  23312  isnei  23314  neiptopnei  23343  neiptopreu  23344  lpfval  23349  lpval  23350  islp  23351  maxlp  23358  islpi  23360  neitr  23391  restlp  23394  ordtbas2  23402  ordtrest2  23415  lmfval  23443  cnfval  23444  iscn  23446  iscnp  23448  tgcn  23463  tgcnp  23464  lmbrf  23471  cnpresti  23499  ist1  23532  ist1-2  23558  cnt1  23561  haust1  23563  cmpfi  23619  cmpfii  23620  1stcfb  23656  2ndc1stc  23662  1stcrest  23664  2ndcdisj  23668  1stcelcls  23673  nllyi  23687  subislly  23693  islocfin  23729  lfinpfin  23736  locfindis  23742  locfincf  23743  comppfsc  23744  kgenval  23747  elkgen  23748  kgencn2  23769  txbas  23779  eltx  23780  ptval  23782  ptpjpre1  23783  ptopn2  23796  ptpjopn  23824  ptclsg  23827  xkoccn  23831  txdis  23844  txdis1cn  23847  ptrescn  23851  hausdiag  23857  hauseqlcld  23858  txhaus  23859  xkohaus  23865  elqtop  23909  qtopeu  23928  kqcldsat  23945  hmeofval  23970  ptuncnv  24019  ptunhmeo  24020  elmptrab  24039  fbdmn0  24046  elfg  24083  elfilss  24088  filunirn  24094  fixufil  24134  elfm  24159  rnelfmlem  24164  rnelfm  24165  fmfnfmlem4  24169  elflim2  24176  flimtopon  24182  elflim  24183  hausflim  24193  flimcls  24197  flfnei  24203  isflf  24205  hausflf  24209  cnpflf  24213  cnflf  24214  txflf  24218  isfcls  24221  fclstopon  24224  isfcls2  24225  fclssscls  24230  fclsnei  24231  fclsfnflim  24239  flimfnfcls  24240  isfcf  24246  fcfelbas  24248  cnpfcf  24253  cnfcf  24254  flfcntr  24255  alexsublem  24256  alexsubALTlem3  24261  cnextfun  24276  cnextfvval  24277  cnextf  24278  cnextcn  24279  tmdgsum2  24308  tgpconncomp  24325  ghmcnp  24327  qustgplem  24333  eltsms  24345  haustsms  24348  tsmsgsum  24351  tsmssubm  24355  tsmssplit  24364  isust  24416  ustbas  24439  elutop  24445  ustuqtoplem  24451  ustuqtop4  24456  ustuqtop  24458  utopsnneiplem  24459  utopsnneip  24460  utopsnnei  24461  isusp  24473  isucn  24489  ucncn  24496  iscfilu  24499  neipcfilu  24507  iscusp  24510  cnextucn  24514  ispsmet  24516  ismet  24535  isxmet  24536  elblps  24599  elbl  24600  elmopn  24654  prdsbl  24703  neibl  24713  met1stc  24733  metrest  24736  prdsxmslem2  24741  txmetcnp  24759  txmetcn  24760  metustsym  24767  cfilucfil2  24773  elbl4  24775  metuel  24776  psmetutop  24779  restmetu  24782  metucn  24783  tngngp  24866  isnmhm  24958  zcld  25026  metnrmlem1a  25071  elcncf  25103  cncfcnvcn  25139  cnheibor  25169  lebnumlem1  25175  ishtpy  25186  isphtpy  25195  om1elbas  25246  elpi1  25259  pi1xfr  25269  pi1coghm  25275  tcphcph  25451  lmmbrf  25476  iscfil  25479  iscau  25490  iscauf  25494  caucfil  25497  iscmet  25498  cmetcaulem  25502  iscmet3lem1  25505  iscmet3lem2  25506  iscmet3  25507  bcthlem1  25538  cmsss  25565  cmetcusp1  25567  cmetcusp  25568  cmscsscms  25587  rrxcph  25606  minveclem3b  25642  ovolfioo  25681  ovolficc  25682  ovolctb  25704  ovoliunnul  25721  ovolshftlem1  25723  sca2rab  25726  ovolscalem1  25727  ovolicc2lem1  25731  ovolicc2lem2  25732  ovolicc2lem4  25734  ovolicc2lem5  25735  iundisj  25762  iunmbl2  25771  uniioombllem3  25799  vitalilem2  25823  vitalilem3  25824  mbfss  25860  i1faddlem  25907  i1fmullem  25908  mbfi1fseqlem2  25930  mbfi1fseqlem4  25932  mbfi1fseq  25935  itg2splitlem  25962  itg2split  25963  itg2monolem1  25964  itg2gt0  25974  isibl  25979  iblss2  26020  itgss3  26029  itgsplit  26050  ellimc  26087  limcmo  26096  cnlimc  26102  limciun  26108  limcun  26109  eldv  26112  dvbsss  26116  dvreslem  26123  elcpn  26148  dvaddf  26156  dvmulf  26157  dvcof  26162  rolle  26204  dvlip2  26209  dvivthlem1  26222  lhop1  26228  lhop2  26229  ftc1cn  26257  fta1glem2  26381  plyco0  26404  elply  26407  ply1termlem  26415  eltayl  26578  tayl0  26580  taylplem1  26581  taylplem2  26582  dvtaylp  26588  taylthlem1  26591  taylthlem2  26592  abelth  26659  cxpcn3  26968  rlimcnp  27185  fsumharmonic  27231  dchrelbas  27455  pntrsumbnd2  27786  ostth2lem2  27853  nolesgn2ores  27891  nogesgn1ores  27893  nosupprefixmo  27919  noinfprefixmo  27920  nosupcbv  27921  nosupdm  27923  nosupfv  27925  nosupres  27926  nosupbnd1lem1  27927  nosupbnd1lem3  27929  nosupbnd1lem5  27931  nosupbnd2lem1  27934  noinfcbv  27936  noinfdm  27938  noinffv  27940  noinfres  27941  noinfbnd1lem1  27942  noinfbnd1lem3  27944  noinfbnd1lem5  27946  noinfbnd2lem1  27949  elmade  28105  elold  28107  sltsleft  28108  sltsright  28109  oldlim  28135  madebday  28148  newbday  28150  ltslpss  28156  bdayiun  28163  cofcutr  28172  cofcutrtime  28175  lrrecval  28187  lrrecval2  28188  addsval  28210  precsexlem9  28463  precsexlem11  28465  ltonold  28509  onnolt  28514  onlts  28515  noseqrdgfn  28554  istrkgb  28779  istrkgcb  28780  istrkge  28781  istrkgl  28782  istrkgld  28783  axtgsegcon  28788  axtg5seg  28789  axtgbtwnid  28790  axtgpasch  28791  axtgupdim2  28795  axtgeucl  28796  tgdim01  28831  iscgrg  28836  isismt  28858  tglnunirn  28872  tglngval  28875  tgellng  28877  legval  28908  legov  28909  legov2  28910  ishlg2  28926  ishlg  28929  mirreu3  28986  mirval  28987  mirfv  28988  mircgr  28989  mirbtwn  28990  ismir  28991  mireq  28997  symquadlem  29021  israg  29032  perpln1  29045  perpln2  29046  isperp  29047  islnopp  29075  outpasch  29092  ishpg  29096  tgplnfn  29112  plngval  29114  isplng  29115  elplng  29117  elplngid  29119  lnincplng  29121  plngcplem  29122  plngcp  29123  plngrot  29127  nhpmirhp  29135  lnperpexs  29169  iscgra  29175  dfcgra2  29196  ragraghl  29204  tgaaddcpbllem2  29208  isinag  29214  isleag  29223  iseqlg  29243  brprlng  29247  prlnghpg  29255  prlngmo  29263  f1otrgitv  29278  f1otrg  29279  f1otrge  29280  ttgval  29283  ttgelitv  29291  elee  29302  brbtwn  29308  brcgr  29309  axlowdimlem16  29366  ebtwntg  29391  elntg2  29394  upgrex  29501  edgupgr  29543  upgredg  29546  edglnl  29552  numedglnl  29553  uhgr2edg  29620  umgr2edg1  29623  usgredg2vlem1  29637  usgredg2vlem2  29638  ushgredgedg  29641  ushgredgedgloop  29643  uhgrspansubgrlem  29702  fusgrfisstep  29741  nbgrval  29748  nbgrel  29752  nbupgrel  29757  nbgr2vtx1edg  29762  nbuhgr2vtx1edgblem  29763  nbuhgr2vtx1edgb  29764  nbusgreledg  29765  usgrnbcnvfv  29777  uvtxval  29799  uvtxel  29800  uvtx01vtx  29809  uvtxusgrel  29815  nbcplgr  29846  cplgr3v  29847  cusgrexi  29855  structtocusgr  29858  vtxdgfval  29879  vtxdg0v  29885  vtxdeqd  29889  vtxdun  29893  1loopgrnb0  29914  1loopgrvd0  29916  1hevtxdg0  29917  1hevtxdg1  29918  1egrvtxdg1  29921  umgr2v2evtxel  29934  umgr2v2enb1  29938  umgr2v2evd2  29939  vtxdginducedm1lem4  29954  vtxdginducedm1  29955  finsumvtxdg2sstep  29961  ewlksfval  30013  isewlk  30014  wksfval  30021  iswlk  30022  uspgr2wlkeq  30057  wlkres  30080  pfxwlk  30097  revwlk  30098  dfpth2  30145  usgr2pthlem  30180  clwlkcompim  30198  uspgrn2crct  30228  wwlks  30255  iswwlksn  30258  wwlknvtx  30265  wlkiswwlks2  30295  wwlksm1edg  30301  wwlksnred  30312  wwlksnext  30313  wwlksnredwwlkn  30315  wwlksnredwwlkn0  30316  wwlksnwwlksnon  30335  wspn0  30344  usgr2wspthons3  30387  rusgrnumwwlkb0  30394  clwwlk  30405  clwwlkccatlem  30411  clwlkclwwlklem2a4  30419  clwlkclwwlk  30424  clwwisshclwwslem  30436  clwwlkinwwlk  30462  clwwlkel  30468  clwwlkf  30469  clwwlkext2edg  30478  wwlksext2clwwlk  30479  wwlksubclwwlk  30480  clwwnisshclwwsn  30481  eleclclwwlknlem2  30483  erclwwlknsym  30492  erclwwlkntr  30493  umgrhashecclwwlk  30500  clwwlkvbij  30535  eupth2lem3lem3  30656  eupth2lem3lem4  30657  eupth2lem3lem6  30659  eupth2lemb  30663  eucrct2eupth  30671  fusgreg2wsplem  30759  2clwwlklem  30769  2clwwlk2clwwlklem  30772  2clwwlkel  30775  2clwwlk2clwwlk  30776  extwwlkfabel  30779  clwwlknonclwlknonf1o  30788  dlwwlknondlwlknonf1olem1  30790  numclwwlk2lem1  30802  numclwlk2lem2f  30803  numclwlk2lem2f1o  30805  ex-res  30867  isssp  31151  sspn  31163  islno  31180  isblo  31209  nmlno0  31222  ishmo  31238  dipdir  31269  dipass  31272  ubthlem1  31297  ubthlem2  31298  htthlem  31344  htth  31345  ocel  31708  ocnel  31725  shsel  31741  shsel2  31749  shmodsi  31816  pjhtheu  31821  pjeq  31826  axpjpj  31847  pjoc2  31866  elspani  31970  h1de2ctlem  31982  elspansn  31993  elspansn2  31994  elnlfn  32355  eleigvec  32384  riesz3i  32489  cbviunf  32975  iuneq12daf  32976  iunrdx  32983  iunrnmptss  32985  cbvdisjf  32991  disjorf  32999  disjabrex  33002  disjabrexf  33003  iundisjf  33009  disjrdx  33011  fresunsn  33045  2ndresdju  33069  abfmpunirn  33072  abfmpeld  33074  abfmpel  33075  fmptcof2  33077  acunirnmpt2  33080  acunirnmpt2f  33081  aciunf1lem  33082  suppss3  33142  fpwrelmap  33152  xrofsup  33186  iundisjfi  33215  eliccioo  33324  s3f1  33338  ccatws1f1o  33341  ismnt  33371  mgcoval  33374  gsummpt2co  33436  gsumpart  33451  gsumhashmul  33455  gsummulsubdishift1  33456  xrge0tsmsbi  33462  gsumwrd2dccatlem  33465  gsumwrd2dccat  33466  cycpmco2  33521  cyc3co2  33528  isfxp  33556  cntrval2  33559  inftmrel  33568  isinftm  33569  isslmd  33590  urpropd  33618  elrgspn  33634  erlval  33646  rlocval  33647  rloccring  33659  rloc1r  33661  rlocisunit  33664  domnprodeq0  33667  domnpropd  33668  fracfld  33697  resv1r  33727  ellspds  33751  ellpi  33755  lbslsp  33758  rhmimaidl  33808  ismxidl  33813  crngmxidl  33820  drng0mxidl  33826  opprqus0g  33840  qsfld  33848  isrprm  33875  rsprprmprmidlb  33881  ressply1evls1  33923  ply1mulrtss  33940  ply1coedeg  33947  psrmonmul  34008  dimpropd  34067  lbslsat  34074  extdg1id  34124  fldextrspunlsplem  34131  fldextrspunlsp  34132  elirng  34144  ply1annidllem  34159  constrsuc  34196  constrconj  34203  constrllcllem  34210  constrlccllem  34211  constrcccllem  34212  nn0constr  34219  smatrcl  34254  smatcl  34260  ist0cld  34291  txomap  34292  locfinreflem  34298  zarclsiin  34329  zart0  34337  rhmpreimacnlem  34342  metidval  34348  cnre2csqima  34369  ordtrest2NEW  34381  fmcncfil  34389  fsumcvg4  34408  ofcfval  34556  measvuni  34673  meascnbl  34678  faeval  34705  ismbfm  34710  elunirnmbfm  34711  imambfm  34721  elcarsg  34764  itgeq12dv  34785  issibf  34792  eulerpartlems  34819  eulerpartlemgc  34821  eulerpartlemgvv  34835  eulerpartlemgu  34836  eulerpart  34841  rrvmbfm  34901  elorvc  34919  elorrvc  34923  dstfrvunirn  34934  ballotlemfc0  34952  ballotlemfcc  34953  ballotlemsima  34975  ballotlemrv  34979  fzssfzo  34998  signstfvn  35025  signstfvneq0  35028  signstres  35031  repr0  35067  reprinrn  35074  reprdifc  35083  hgt750lemg  35110  hgt750lemb  35112  istrkg2d  35122  axtgupdim2ALTV  35124  afsval  35130  brafs  35131  bnj945  35231  bnj1400  35292  bnj18eq1  35384  bnj916  35390  bnj1014  35418  bnj1015  35419  bnj1110  35439  bnj1417  35498  rankval2b  35554  r1filimi  35559  r1ssel  35563  acnum  35586  onvf1odlem3  35650  vonf1wev  35653  vonf1owevOLD  35655  vonf1osev  35657  cplgredgex  35667  subfacp1lem2b  35714  subfacp1lem4  35716  subfacp1lem5  35717  subfacp1lem6  35718  ptpconn  35766  cvmscbv  35791  iscvm  35792  cvmsi  35798  cvmsval  35799  cvmliftmolem1  35814  cvmlift2lem12  35847  cvmlift2lem13  35848  cvmlift3lem7  35858  snmlval  35864  satfv1  35896  satfvsucsuc  35898  satfrnmapom  35903  satf0op  35910  satf0n0  35911  sat1el2xp  35912  fmlafvel  35918  isfmlasuc  35921  fmlaomn0  35923  gonan0  35925  goaln0  35926  gonar  35928  goalr  35930  satffunlem1lem2  35936  satffunlem2lem2  35939  satfv0fvfmla0  35946  satef  35949  satefvfmla0  35951  sategoelfvb  35952  satfv1fvfmla1  35956  mrsubfval  36041  mrsubvrs  36055  mclsrcl  36094  mclsval  36096  mppsval  36105  mclsppslem  36116  opelco3  36308  wsuclem  36356  funtransport  36564  fvtransport  36565  brcolinear  36592  colineardim1  36594  funray  36673  fvray  36674  funline  36675  fvline  36677  lineelsb2  36681  fwddifval  36695  fwddifnval  36696  rankelg  36701  rankeq1o  36704  elhf2  36708  0hf  36710  nmulprop  36723  nmulr0  36728  nmuladdel  36745  ltnmul  36749  ltnadd  36751  rmoeqbidv  36786  disjeq12dv  36788  ixpeq12dv  36789  prodeq12sdv  36791  itgeq12sdv  36792  cbvralvw2  36799  cbvrexvw2  36800  cbvrmovw2  36801  cbvreuvw2  36802  cbvcsbvw2  36804  cbviunvw2  36805  cbviinvw2  36806  cbvmptvw2  36807  cbvdisjvw2  36808  cbvmpo1vw2  36816  cbvmpo2vw2  36817  cbvsbcdavw  36830  cbvcsbdavw  36832  cbvcsbdavw2  36833  cbviundavw  36835  cbviindavw  36836  cbvdisjdavw  36841  cbvrabdavw2  36858  cbviundavw2  36859  cbviindavw2  36860  cbvmptdavw2  36861  cbvdisjdavw2  36862  cbvriotadavw2  36863  cbvmpo1davw2  36865  cbvmpo2davw2  36866  cbvsumdavw2  36868  neibastop2lem  36932  neibastop3  36934  eltail  36946  ttctr  37065  dfttc2g  37078  mh-infprim2bi  37119  bj-projeq  37689  bj-projval  37693  bj-restsn  37785  opelopabbv  37848  brabd0  37852  bj-eldiag  37881  bj-eldiag2  37882  mptsnunlem  38045  dissneqlem  38047  iooelexlt  38069  relowlssretop  38070  rdgellim  38083  exrecfnlem  38086  finxpeq1  38093  finxpreclem6  38103  pibp21  38122  curf  38310  uncf  38311  curunc  38314  unccur  38315  fin2so  38319  lindsadd  38325  lindsdom  38326  lindsenlbs  38327  matunitlindflem1  38328  matunitlindflem2  38329  matunitlindf  38330  ptrest  38331  ptrecube  38332  poimirlem2  38334  poimirlem8  38340  poimirlem17  38349  poimirlem18  38350  poimirlem20  38352  poimirlem21  38353  poimirlem22  38354  poimirlem24  38356  poimirlem26  38358  poimirlem29  38361  heicant  38367  mblfinlem1  38369  mblfinlem2  38370  volsupnfl  38377  itg2addnclem  38383  itg2gt0cn  38387  indexdom  38447  incsequz  38461  istotbnd  38482  istotbnd3  38484  0totbnd  38486  sstotbnd  38488  sstotbnd3  38489  isbnd  38493  prdstotbnd  38507  cntotbnd  38509  isismty  38514  heibor1lem  38522  heiborlem2  38525  heiborlem3  38526  heibor  38534  isass  38559  exidcl  38589  exidreslem  38590  elghomlem2OLD  38599  rngoidmlem  38649  rngo1cl  38652  divrngcl  38670  isdrngo2  38671  isrngohom  38678  isrngoiso  38691  isriscg  38697  iscom2  38708  iscringd  38711  isidl  38727  ispridl  38747  ismaxidl  38753  ac6s6  38883  dmecd  39021  dfpre4  39191  releldmqs  39454  releldmqscoss  39456  erimeq2  39474  qmapeldisjsim  39571  eldisjlem19  39624  membpartlem19  39625  prter3  39718  islshp  39815  islsat  39827  lcvfbr  39856  islfl  39896  ellkr  39925  islshpkrN  39956  ldual1dim  40002  isopos  40016  cmtfvalN  40046  cvrfval  40104  isat  40122  islln  40342  islpln  40366  islvol  40409  isline  40575  ispointN  40578  ispsubsp  40581  elpmap  40594  elpmapat  40600  elpadd  40635  paddclN  40678  elpclN  40728  elpcliN  40729  pclfinN  40736  pclcmpatN  40737  ispsubclN  40773  iswatN  40830  islhp  40832  islaut  40919  ispautN  40935  isldil  40946  isltrn  40955  isdilN  40990  istrnN  40993  istendo  41596  dvhb1dimN  41822  erng1lem  41823  erngdvlem4-rN  41835  diaelval  41869  diaeldm  41872  dia1dimid  41899  cdlemm10N  41954  dibopelvalN  41979  dibopelval2  41981  dibelval3  41983  dibelval1st  41985  dibelval2nd  41988  dibeldmN  41994  dibvalrel  41999  dibglbN  42002  dicffval  42010  dicfval  42011  dicopelval  42013  dicelvalN  42014  dicelval3  42016  dicvalrelN  42021  dicelval1sta  42023  diclspsn  42030  dihopelvalbN  42074  dihopelvalcqat  42082  dihopelvalcpre  42084  dihvalrel  42115  dih1  42122  dihmeetlem4preN  42142  dihmeetlem13N  42155  dih1dimatlem  42165  dochnel2  42228  dihjatcclem4  42257  dvh2dim  42281  dvh3dim  42282  dvh4dimN  42283  dochfln0  42313  lpolsetN  42318  islpolN  42319  lcfrvalsnN  42377  lcfrlem21  42399  lcfrlem27  42405  lcfrlem37  42415  lcfr  42421  lcdlss  42455  mapdcv  42496  hdmap1fval  42632  hdmapffval  42662  hdmapfval  42663  hdmapval  42664  hgmapffval  42721  hgmapfval  42722  hdmapellkr  42750  hlhilhillem  42796  fzsplitnd  42811  isprimroot  42922  primrootsunit1  42926  primrootscoprmpow  42928  primrootscoprbij  42931  aks6d1c1p2  42938  aks6d1c1p3  42939  aks6d1c1p4  42940  aks6d1c1p5  42941  aks6d1c1p6  42943  aks6d1c1  42945  evl1gprodd  42946  sticksstones11  42985  sticksstones12a  42986  rhmqusspan  43014  grpods  43023  fzosumm1  43080  frlmfielbas  43351  frlmsnic  43385  psrmnd  43388  isnacs  43512  mrefg2  43515  elmzpcl  43534  mzpcompact2  43560  eldiophb  43565  elpell1qr  43651  elpell14qr  43653  elpell1234qr  43655  pw2f1ocnv  43841  pw2f1o2val2  43844  aomclem4  43861  aomclem6  43863  islssfg2  43875  imasgim  43904  lnr2i  43920  elmnc  43940  rngunsnply  43973  onexomgt  44045  onexlimgt  44047  onexoegt  44048  oaordnr  44100  omnord1  44109  oenord1  44120  cantnfresb  44128  tfsconcatun  44141  tfsconcat0i  44149  ofoaf  44159  naddcnff  44166  naddcnffo  44168  naddcnfcom  44170  naddcnfid1  44171  naddcnfid2  44172  naddcnfass  44173  naddwordnexlem4  44205  fiinfi  44376  sqrtcvallem1  44434  elintima  44456  eliunov2  44482  ov2ssiunov2  44503  brtrclfv2  44530  rfovcnvf1od  44807  rfovcnvfvd  44810  fsovrfovd  44812  fsovfvd  44813  fsovcnvlem  44816  ntrclsfv1  44858  ntrclselnel1  44860  ntrclsneine0lem  44867  ntrneifv1  44882  ntrneifv2  44883  ntrneiel  44884  gneispace2  44935  gneispacess2  44949  extoimad  44967  mnringelbased  45018  dvconstbi  45121  bccbc  45132  wfac8prim  45788  permaxrep  45792  permac8prim  45800  eliin2f  45899  iineq12dv  45901  rabbida2  45927  disjinfi  45987  unirnmap  46001  elmptima  46050  iuneqfzuzlem  46127  iooiinioc  46349  fsumiunss  46368  fsumsupp0  46371  lptre2pt  46431  icccncfext  46678  cncfiooicclem1  46684  dvnprodlem2  46738  stoweidlem27  46818  stoweidlem29  46820  stoweidlem31  46822  stoweidlem34  46825  stoweidlem48  46839  stoweidlem59  46850  dirkercncflem2  46895  dirkercncflem4  46897  fourierdlem2  46900  fourierdlem3  46901  fourierdlem25  46923  fourierdlem32  46930  fourierdlem33  46931  fourierdlem41  46939  fourierdlem48  46945  fourierdlem49  46946  fourierdlem62  46959  fourierdlem70  46967  fourierdlem80  46977  fourierdlem92  46989  fourierdlem93  46990  fourierdlem101  46998  etransclem37  47062  sge0val  47157  sge0f1o  47173  sge0iunmptlemre  47206  sge0iunmpt  47209  iundjiun  47251  caragenel  47286  ovncvrrp  47355  ovnsubaddlem1  47361  ovnsubadd  47363  hoidmvlelem2  47387  hoidmvlelem3  47388  hoidmvlelem4  47389  hoidmvle  47391  ovncvr2  47402  hspdifhsp  47407  hoiqssbl  47416  hspmbllem2  47418  hspmbl  47420  opnvonmbllem1  47423  isvonmbl  47429  ovnovollem1  47447  issmflem  47518  smflimlem3  47564  smflimlem4  47565  smflim  47568  smfmullem2  47583  smflimmpt  47601  smfsuplem1  47602  smflimsuplem1  47611  smflimsuplem3  47613  smflimsuplem4  47614  smflimsuplem7  47617  smflimsup  47619  chnsubseq  47673  fcores  47881  fcoresf1  47883  afvelrnb  47977  afvelrnb0  47978  afv2co2  48071  el1fzopredsuc  48140  muldvdsfacm1  48201  iccpart  48242  iccpartgtprec  48246  iccpartiltu  48248  iccpartigtl  48249  iccpartltu  48251  iccpartgtl  48252  iccpartgt  48253  iccpartleu  48254  iccpartgel  48255  iccelpart  48259  iccpartiun  48260  icceuelpart  48262  fargshiftfv  48265  fargshiftfo  48268  sprel  48310  prprelb  48342  prprelprb  48343  nprmdvdsfacm1lem4  48452  fpprel  48570  sbgoldbo  48629  wtgoldbnnsum4prm  48644  bgoldbnnsum3prm  48646  bgoldbtbndlem3  48649  bgoldbtbnd  48651  clnbgrval  48664  elclnbgrelnbgr  48667  clnbgrel  48670  clnbupgrel  48676  vopnbgrel  48696  isubgredg  48708  upgrimwlklem3  48741  upgrimwlklem5  48743  upgrimpths  48751  grtriprop  48783  isgrtri  48785  grtriclwlk3  48787  stgredgel  48799  gpgvtxel  48889  gpgiedgdmel  48891  gpgedgel  48892  opgpgvtx  48897  gpg5nbgrvtx13starlem1  48913  gpg5nbgrvtx13starlem2  48914  gpg5nbgrvtx13starlem3  48915  gpg3kgrtriex  48931  grlimedgnedg  48973  upwlksfval  48977  isupwlk  48978  intop  49044  isclintop  49048  assintop  49050  isassintop  49051  assintopcllaw  49053  uzlidlring  49076  elrngchomALTV  49110  rngccatidALTV  49113  rngcsectALTV  49116  rngcisoALTV  49118  rhmsubcALTVlem3  49124  rhmsubcALTVlem4  49125  funcringcsetcALTV2lem7  49137  funcringcsetcALTV2lem9  49139  elringchomALTV  49144  ringccatidALTV  49147  ringcsectALTV  49150  ringcisoALTV  49152  ringcbasbasALTV  49153  funcringcsetclem7ALTV  49160  funcringcsetclem9ALTV  49162  srhmsubcALTV  49166  smprngprmrng  49180  cbvmpox2  49192  ply1sclrmsm  49240  dmatALTbasel  49258  lcoval  49268  lindslinindsimp1  49313  lindslinindsimp2  49319  lmod1  49348  elbigo  49407  elbigo2  49408  elbigolo1  49413  dig2nn0ld  49460  naryfvalel  49486  rrxlines  49589  rrxlinesc  49591  rrxlinec  49592  eenglngeehlnm  49595  elrrx2linest2  49601  rrxsphere  49604  itsclc0  49627  itsclc0b  49628  itsclinecirc0  49629  itsclinecirc0b  49630  itscnhlinecirc02p  49641  brab2dd  49682  f1omo  49747  f1omoOLD  49748  lubeldm2d  49812  glbeldm2d  49813  catprs  49865  sectpropdlem  49890  nelsubc3lem  49924  initc  49945  imaid  50008  upfval  50030  upfval2  50031  upfval3  50032  uppropd  50035  oppcinito  50089  oppctermo  50090  oppczeroo  50091  initopropd  50097  termopropd  50098  isthinc  50273  isthincd2lem1  50279  thincmoALT  50283  thincmod  50284  isthincd  50290  thincpropd  50296  indcthing  50314  discthing  50315  prsthinc  50318  termcterm  50367  termc2  50372  isinito4  50401  2arwcatlem1  50449  setc1onsubc  50456  cnelsubclem  50457  ranval3  50485  lmdfval2  50509  cmdfval2  50510  termolmd  50524  elsetrecslem  50553