Theorem eleq2d 2846

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  eleq2  2849  eleq12d  2854  eleqtrd  2862  neleqtrd  2882  eqabrd  2901  raleqbidv  3334  rexeqbidv  3335  reueqbidv  3401  rabeqbidva  3428  elabd2  3623  sbcbid  3792  sbcbi2  3796  csbeq2d  3852  csbeq2dv  3853  cbvcsbw  3856  cbvcsb  3857  cbvcsbv  3858  csbie  3881  csbied  3882  csbie2g  3886  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  sbcel12  4368  sbcel1g  4373  sbcel2  4375  prel12g  4823  eliuni  4956  iuneqconst  4962  iuneq12df  4977  iuneq12d  4979  cbviun  4992  cbviin  4993  cbviung  4994  cbviing  4995  cbviunv  4996  cbviinv  4997  iinxsng  5047  iinxprg  5048  iunxsng  5049  iunxsngf  5051  cbvdisj  5079  cbvdisjv  5080  disjor  5084  disjiund  5093  mpteq12da  5187  mpteq12f  5189  mpteq12dva  5190  axpweq  5311  rabxfrd  5378  brab2d  5511  rbropapd  5536  opeliunxp  5717  opeliun2xp  5718  opeliunxp2  5814  iunxpf  5825  elimampt  6034  elrelimasn  6083  elimasni  6088  xpdifid  6158  xpdifcnvepel  6159  imadifssranOLDOLD  6203  ressn  6288  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  7100  fmptco  7130  fnelfp  7180  fnelnfp  7182  tpres  7207  fnprb  7214  fntpb  7215  funfvima3  7242  eluniima  7254  dff13  7258  f1ounsn  7280  f1eqcocnv  7309  isoini  7346  riotaeqdv  7378  mpoeq123dva  7494  cbvmpox  7513  elimampo  7557  ovelrn  7597  elovmpod  7665  elovmpo  7666  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  elovmpt3rab1  7681  fiun  7955  f1iun  7956  zfrep6OLD  7967  fmpox  8078  el2mpocsbcl  8096  el2mpocl  8097  bropopvvv  8101  bropfvvvv  8103  xpord2indlem  8164  xpord3inddlem  8171  elsuppfng  8186  elsuppfn  8187  suppfnss  8206  opeliunxp2f  8227  mpoxopn0yelv  8230  mpoxopovel  8237  rntpos  8256  mpocurryd  8286  fpr2  8322  wfr2  8345  onoviun  8351  smoel  8368  smoiso  8370  smoel2  8371  smo11  8372  tfrlem9  8393  oalimcl  8568  oaass  8569  omordi  8574  omordlim  8585  omlimcl  8586  odi  8587  omeulem1  8590  omeulem2  8591  oen0  8595  oeordi  8596  oeordsuc  8603  oelimcl  8609  oeeulem  8610  oeeui  8611  nnmordi  8640  oaabs2  8658  omabs  8660  omsmolem  8666  ereldm  8771  iiner  8810  elmapg  8859  elpmg  8863  curf  8890  uncf  8891  elixpsn  8965  ixpsnf1o  8966  boxriin  8968  omxpenlem  9097  pw2f1olem  9100  phplem2  9220  php3  9224  infn0  9294  elfi  9405  dffi3  9423  marypha2lem2  9428  ordiso2  9509  wemapsolem  9544  elharval  9555  inf3lemd  9628  inf3lem1  9629  inf3lem2  9630  inf3lem3  9631  cantnfs  9667  cantnfp1lem3  9681  cantnflem1b  9687  cantnflem1  9690  ttrclselem2  9727  trcl  9729  frr2  9764  r1sdom  9781  r1ordg  9785  r1pwss  9791  tz9.12lem3  9796  tz9.12  9797  r1elwf  9804  rankr1ai  9806  rankidb  9808  rankr1bg  9811  rankval2  9827  rankval2b  9835  rankelg  9852  rankunb  9864  tcrank  9901  r1filimi  9903  elhf2  9910  0hf  9917  acni  10124  acni2  10125  acndom  10130  infpwfien  10141  alephnbtwn  10150  cardaleph  10168  cardinfima  10176  iunfictbso  10193  dfac3  10200  dfac5lem5  10206  dfac5  10207  dfac9  10215  dfac12r  10225  kmlem2  10230  kmlem12  10240  kmlem13  10241  kmlem14  10242  ackbij2lem3  10318  ackbij2  10320  cofsmo  10347  alephsing  10354  fin23lem30  10420  isf32lem9  10439  itunisuc  10497  axcc2lem  10514  axcc3  10516  domtriomlem  10520  axdc2lem  10526  axdc2  10527  axdc3lem2  10529  axdc3lem4  10531  axdc4lem  10533  ac6c4  10559  zorn2lem1  10574  ttukeylem6  10592  pwcfsdom  10668  axregndlem2  10688  axinfndlem1  10690  axacndlem4  10695  axacnd  10697  pwfseqlem1  10743  inar1  10860  inatsk  10863  gruurn  10883  grur1  10905  eltskm  10928  genpelv  11085  eluz1  12969  elixx1  13485  elixx3g  13489  elioo2  13517  elfz1  13644  elfz2  13646  elfzp1  13708  fzpr  13713  fzsuc2  13716  fzrev3  13724  elfzp12  13737  fzm1  13741  elfzo  13795  fz0add1fz1  13870  elfzo0l  13891  elfzom1b  13901  fzosplitsni  13914  elfzr  13916  elfzlmr  13917  zmodidfzo  14040  seqp1  14159  seqf1o  14186  bcval  14448  bcpasc  14465  hashf1lem1  14600  fundmge2nop0  14647  wrdmap  14691  elovmpowrd  14703  ccatfval  14718  elfzelfzccat  14725  ccatlid  14732  ccatass  14734  ccatrn  14735  ccatf1  14736  ccatalpha  14740  swrdrn3  14802  swrdfv2  14811  ccatswrd  14818  swrdccat2  14819  pfxfv  14832  pfxeq  14845  ccatpfx  14850  swrdswrd  14854  swrdpfx  14856  pfxpfx  14857  cats1un  14870  swrdccatfn  14873  swrdccatin1  14874  pfxccatin12lem4  14875  pfxccatin12lem1  14877  swrdccatin2  14878  pfxccatin12lem2c  14879  pfxccatin12lem2  14880  swrdccat3blem  14888  swrdccatin1d  14892  swrdccatin2d  14893  pfxccatin12d  14894  revccat  14915  revrev  14916  revpfxsfxrev  14917  repswpfx  14936  repswccat  14937  cshwidxmod  14954  2cshw  14964  cshwcshid  14978  cshwcsh2id  14979  cshimadifsn  14980  cshimadifsn0  14981  revco  14985  ccatco  14986  cshco  14987  swrdco  14988  ofccat  15122  shftfn  15226  shftval  15227  limsupgle  15644  ello12  15683  elo12  15694  isercolllem3  15834  sumeq1  15856  fsumsplit  15907  sumsplit  15934  fsum2dlem  15936  fsumcom2  15940  fsumparts  15973  explecnv  16034  pwdif  16037  fprodser  16116  fprodsplit  16133  fprod2dlem  16147  fprodcom2  16151  eftlub  16277  divalgmod  16576  bitsval  16594  bitsp1e  16602  bitsp1o  16603  sadfval  16622  sadcp1  16625  sadval  16626  sadcadd  16628  sadadd2  16630  saddisjlem  16634  sadadd  16637  sadass  16641  smufval  16647  smuval  16651  smuval2  16652  smupvallem  16653  smu01lem  16655  smueqlem  16660  smumul  16663  bezoutlem2  16713  bezoutlem4  16715  algfx  16755  eucalgcvga  16761  reumodprminv  16982  nnnn0modprm0  16984  unbenlem  17086  prmreclem5  17098  vdwapval  17151  vdwapun  17152  vdwnnlem1  17173  vdwnn  17176  ramval  17186  0ram  17198  ramub1lem2  17205  prmgaplem7  17235  prmlem0  17283  elrest  17598  prdsbasmpt  17641  prdsleval  17648  prdsbasmpt2  17653  pwselbasb  17659  imasaddfnlem  17700  imasvscafn  17709  divsfval  17719  ismre  17760  mreunirn  17771  mrisval  17804  ismri  17805  isacs  17825  catidd  17854  iscatd2  17855  ismon  17908  isepi  17915  sectffval  17925  sectfval  17926  dfiso2  17947  cicsym  17979  issubc  18010  catsubcat  18014  isfunc  18039  funcres  18071  funcpropd  18077  ffthiso  18106  isnat  18125  isnat2  18126  fuciso  18153  initoval  18168  termoval  18169  isinito  18171  istermo  18172  iszeroo  18173  isinitoi  18174  istermoi  18175  initoid  18176  termoid  18177  iszeroi  18184  2initoinv  18185  initoeu1  18186  initoeu2  18191  2termoinv  18192  termoeu1  18193  arwhoma  18220  elsetchom  18256  setcmon  18262  setcepi  18263  setciso  18266  catciso  18286  elestrchom  18302  estrcbasbas  18305  funcestrcsetclem7  18320  funcestrcsetclem8  18321  funcestrcsetclem9  18322  fthestrcsetc  18324  fullestrcsetc  18325  equivestrcsetc  18326  setc1strwun  18327  funcsetcestrclem7  18335  funcsetcestrclem8  18336  funcsetcestrclem9  18337  fthsetcestrc  18339  fullsetcestrc  18340  hofcl  18433  hofpropd  18441  yonedalem4c  18451  yonedainv  18455  yonffthlem  18456  lubeldm  18525  glbeldm  18538  joindef  18548  meetdef  18562  poslubdg  18586  acsficl2d  18726  acsmapd  18728  psref  18748  psss  18754  dirge  18777  chnccats1  18799  chnccat  18800  chnrev  18801  mgmpropd  18829  issstrmgm  18831  grpidval  18840  grpidpropd  18842  grpidd  18852  imasmgm2  18863  ismgmhm  18885  issubmgm  18891  issgrpd  18919  sgrppropd  18920  ismndd  18946  mndpropd  18951  imasmnd2  18968  imasmnd  18969  xpsmnd0  18972  ismhm  18980  issubm  18998  gsumsgrpccat  19036  elefmndbas2  19070  smndex1mndlem  19108  imasgrp2  19265  imasgrp  19266  issubg  19336  subginv  19343  isnsg  19365  eqg0el  19398  quselbas  19399  isghm  19430  resghm2b  19448  conjnmzb  19467  conjnsg  19468  ghmpropd  19470  isga  19505  elcntz  19536  elcntzsn  19539  cntzrcl  19541  resscntz  19547  symgextf1  19635  gsmsymgreqlem2  19645  f1otrspeq  19661  pmtrfrn  19672  pmtrdifellem3  19692  pmtrdifellem4  19693  psgnunilem1  19707  psgnunilem5  19708  psgnunilem2  19709  psgnunilem3  19710  psgneldm2  19718  psgnfitr  19731  psgnsn  19734  gexdvds  19798  gex1  19805  isslw  19822  sylow3lem2  19842  lsmelvalx  19854  pj1ghm  19917  efgtlen  19940  efgsfo  19953  efgredlemc  19959  frgp0  19974  frgpmhm  19979  qusabl  20079  frgpnabllem1  20087  imasabl  20090  cycsubmcmn  20103  0cyg  20107  cycsubgcyg  20115  gsumval3  20121  gsumcllem  20122  gsumzaddlem  20135  gsumzsplit  20141  gsummptfzcl  20183  eldprd  20220  dprdcntz2  20254  dprd2d2  20260  dmdprdsplit2lem  20261  dmdprdsplit2  20262  dprdsplit  20264  ablfac2  20305  isrngd  20395  rngpropd  20396  imasrng  20399  qusrng  20402  ringurd  20411  isringd  20522  imasring  20560  xpsring1d  20563  dvdsrval  20591  isunit  20603  dvdsrpropd  20646  isirred  20649  isrnghm  20671  isrngim  20675  c0ghm  20691  c0snghm  20694  isrhm0  20706  isrhm  20709  isrim0  20713  crngrhmfo  20726  islring  20792  issubrng  20799  opprsubrng  20811  issubrg  20823  opprsubrg  20845  resrhm2b  20854  rhmpropd  20861  rnghmresel  20872  elrngchom  20876  rnghmsubcsetclem1  20883  rnghmsubcsetclem2  20884  rngcid  20887  rngcsect  20888  rngciso  20890  funcrngcsetcALT  20893  zrinitorngc  20894  zrtermorngc  20895  rhmresel  20901  elringchom  20905  rhmsubcsetclem1  20912  rhmsubcsetclem2  20913  ringcid  20916  rhmsscrnghm  20917  rhmsubcrngclem1  20918  rhmsubcrngclem2  20919  ringcsect  20922  ringciso  20924  ringcbasbas  20925  zrtermoringc  20927  srhmsubc  20932  rhmsubclem3  20939  rhmsubclem4  20940  drngunit  20985  isdrng4  20992  isdrngd  21022  isdrngdOLD  21024  issdrg  21045  sdrgunit  21053  isabv  21068  issrngd  21112  islmod  21139  lmodprop2d  21199  islss  21209  islssd  21210  lssats2  21275  ellspsn  21278  islmhm  21302  lmhmf1o  21321  lmhmima  21322  lmhmpreima  21323  reslmhm  21327  pwssplit3  21336  lmhmpropd  21348  islbs  21351  lspprel  21369  lspfixed  21406  lbsacsbs  21434  lbsextlem1  21436  lbsextlem2  21437  lbsextlem3  21438  lbsextlem4  21439  ixpsnbasval  21483  isridlrng  21498  rnglidlmmgm  21533  isridl  21545  quscrng  21579  rngqiprngimfolem  21586  rngqiprngimf1lem  21590  rngqiprngimfo  21597  isprmidl  21619  qsidomlem1  21636  qsidomlem2  21637  islpidl  21649  lidldvgen  21658  irinitoringc  21785  pzriprnglem13  21799  pzriprnglem14  21800  zrhrhmb  21816  znf1o  21857  frgpcyg  21879  psgnevpmb  21893  isphld  21960  phlssphl  21965  elocv  21974  iscss  21989  isobs  22026  obs2ss  22035  dsmmfi  22044  dsmmelbas  22045  dsmmlss  22050  frlmelbas  22062  frlmlbs  22103  frlmup1  22104  ellspd  22108  islinds  22115  islindf2  22120  f1lindf  22128  islindf4  22144  lindsdom  22156  lindsenlbs  22157  assamulgscmlem2  22208  psrgrp  22264  mplsubglem  22306  mpllsslem  22307  mplmonmul  22345  subrgascl  22375  subrgasclcl  22376  mpfind  22424  ismhp  22461  gsumply1subr  22551  lply1binomsc  22629  matbas2d  22738  matecl  22740  matvscl  22746  mat1  22762  mat0dim0  22782  mat0dimid  22783  mat0dimscm  22784  mat1dimelbas  22786  dmatel  22808  scmatel  22820  scmateALT  22827  scmataddcl  22831  scmatsubcl  22832  smatvscl  22839  scmatghm  22848  mat1scmat  22854  mdetunilem7  22933  mdetunilem9  22935  smadiadetr  22990  matunitlindflem1  22994  matunitlindflem2  22995  matunitlindf  22996  cramerimplem2  23002  cramer0  23008  pmatcoe1fsupp  23019  cpmatpmat  23028  cpmatel  23029  cpmatacl  23034  cpmatinvcl  23035  mat2pmatghm  23048  mat2pmatmul  23049  decpmatmullem  23089  pmatcollpwlem  23098  pmatcollpw3fi1lem1  23104  pmatcollpwscmatlem1  23107  monmat2matmon  23142  chfacfscmul0  23176  chfacfscmulgsum  23178  chfacfpmmulgsum  23182  cayhamlem1  23184  cpmadugsumlemB  23192  cpmadugsumlemC  23193  cpmadugsumlemF  23194  cayhamlem2  23202  istopon  23230  eltg  23275  eltg2  23276  eltop  23292  eltop2  23293  eltop3  23294  pptbas  23326  iscld  23345  neiss2  23419  isnei  23421  neiptopnei  23450  neiptopreu  23451  lpfval  23456  lpval  23457  islp  23458  maxlp  23465  islpi  23467  neitr  23498  restlp  23501  ordtbas2  23509  ordtrest2  23522  lmfval  23550  cnfval  23551  iscn  23553  iscnp  23555  tgcn  23570  tgcnp  23571  lmbrf  23578  cnpresti  23606  ist1  23639  ist1-2  23665  cnt1  23668  haust1  23670  cmpfi  23726  cmpfii  23727  1stcfb  23763  2ndc1stc  23769  1stcrest  23771  2ndcdisj  23775  1stcelcls  23780  nllyi  23794  subislly  23800  islocfin  23836  lfinpfin  23843  locfindis  23849  locfincf  23850  comppfsc  23851  kgenval  23854  elkgen  23855  kgencn2  23876  txbas  23886  eltx  23887  ptval  23889  ptpjpre1  23890  ptopn2  23903  ptpjopn  23931  ptclsg  23934  xkoccn  23938  txdis  23951  txdis1cn  23954  ptrescn  23958  hausdiag  23964  hauseqlcld  23965  txhaus  23966  xkohaus  23972  elqtop  24016  qtopeu  24035  kqcldsat  24052  hmeofval  24077  ptuncnv  24126  ptunhmeo  24127  elmptrab  24146  fbdmn0  24153  elfg  24190  elfilss  24195  filunirn  24201  fixufil  24241  elfm  24266  rnelfmlem  24271  rnelfm  24272  fmfnfmlem4  24276  elflim2  24283  flimtopon  24289  elflim  24290  hausflim  24300  flimcls  24304  flfnei  24310  isflf  24312  hausflf  24316  cnpflf  24320  cnflf  24321  txflf  24325  isfcls  24328  fclstopon  24331  isfcls2  24332  fclssscls  24337  fclsnei  24338  fclsfnflim  24346  flimfnfcls  24347  isfcf  24353  fcfelbas  24355  cnpfcf  24360  cnfcf  24361  flfcntr  24362  alexsublem  24363  alexsubALTlem3  24368  cnextfun  24383  cnextfvval  24384  cnextf  24385  cnextcn  24386  tmdgsum2  24415  tgpconncomp  24432  ghmcnp  24434  qustgplem  24440  eltsms  24452  haustsms  24455  tsmsgsum  24458  tsmssubm  24462  tsmssplit  24471  isust  24523  ustbas  24546  elutop  24552  ustuqtoplem  24558  ustuqtop4  24563  ustuqtop  24565  utopsnneiplem  24566  utopsnneip  24567  utopsnnei  24568  isusp  24580  isucn  24596  ucncn  24603  iscfilu  24606  neipcfilu  24614  iscusp  24617  cnextucn  24621  ispsmet  24623  ismet  24642  isxmet  24643  elblps  24706  elbl  24707  elmopn  24761  prdsbl  24810  neibl  24820  met1stc  24840  metrest  24843  prdsxmslem2  24848  txmetcnp  24866  txmetcn  24867  metustsym  24874  cfilucfil2  24880  elbl4  24882  metuel  24883  psmetutop  24886  restmetu  24889  metucn  24890  tngngp  24973  isnmhm  25065  zcld  25133  metnrmlem1a  25178  elcncf  25210  cncfcnvcn  25246  cnheibor  25276  lebnumlem1  25282  ishtpy  25293  isphtpy  25302  om1elbas  25353  elpi1  25366  pi1xfr  25376  pi1coghm  25382  tcphcph  25558  lmmbrf  25583  iscfil  25586  iscau  25597  iscauf  25601  caucfil  25604  iscmet  25605  cmetcaulem  25609  iscmet3lem1  25612  iscmet3lem2  25613  iscmet3  25614  bcthlem1  25645  cmsss  25672  cmetcusp1  25674  cmetcusp  25675  cmscsscms  25694  rrxcph  25713  minveclem3b  25749  ovolfioo  25788  ovolficc  25789  ovolctb  25811  ovoliunnul  25828  ovolshftlem1  25830  sca2rab  25833  ovolscalem1  25834  ovolicc2lem1  25838  ovolicc2lem2  25839  ovolicc2lem4  25841  ovolicc2lem5  25842  iundisj  25869  iunmbl2  25878  uniioombllem3  25906  vitalilem2  25930  vitalilem3  25931  mbfss  25967  i1faddlem  26014  i1fmullem  26015  mbfi1fseqlem2  26037  mbfi1fseqlem4  26039  mbfi1fseq  26042  itg2splitlem  26069  itg2split  26070  itg2monolem1  26071  itg2gt0  26081  isibl  26086  iblss2  26126  itgss3  26135  itgsplit  26156  ellimc  26193  limcmo  26202  cnlimc  26208  limciun  26214  limcun  26215  eldv  26218  dvbsss  26222  dvreslem  26229  elcpn  26254  dvaddf  26262  dvmulf  26263  dvcof  26268  rolle  26310  dvlip2  26315  dvivthlem1  26328  lhop1  26334  lhop2  26335  ftc1cn  26363  fta1glem2  26487  plyco0  26510  elply  26513  ply1termlem  26521  eltayl  26687  tayl0  26689  taylplem1  26690  taylplem2  26691  dvtaylp  26697  taylthlem1  26700  taylthlem2  26701  abelth  26768  cxpcn3  27076  rlimcnp  27293  fsumharmonic  27339  dchrelbas  27563  pntrsumbnd2  27894  ostth2lem2  27961  nolesgn2ores  28029  nogesgn1ores  28031  nosupprefixmo  28057  noinfprefixmo  28058  nosupcbv  28059  nosupdm  28061  nosupfv  28063  nosupres  28064  nosupbnd1lem1  28065  nosupbnd1lem3  28067  nosupbnd1lem5  28069  nosupbnd2lem1  28072  noinfcbv  28074  noinfdm  28076  noinffv  28078  noinfres  28079  noinfbnd1lem1  28080  noinfbnd1lem3  28082  noinfbnd1lem5  28084  noinfbnd2lem1  28087  elmade  28243  elold  28245  sltsleft  28246  sltsright  28247  oldlim  28273  madebday  28286  newbday  28288  ltslpss  28294  bdayiun  28301  cofcutr  28310  cofcutrtime  28313  lrrecval  28325  lrrecval2  28326  addsval  28348  precsexlem9  28601  precsexlem11  28603  ltonold  28647  onnolt  28652  onlts  28653  noseqrdgfn  28692  istrkgb  28917  istrkgcb  28918  istrkge  28919  istrkgl  28920  istrkgld  28921  axtgsegcon  28926  axtg5seg  28927  axtgbtwnid  28928  axtgpasch  28929  axtgupdim2  28933  axtgeucl  28934  tgsegconeu  28949  tgdim01  28970  iscgrg  28975  isismt  28997  tglnunirn  29011  tglngval  29014  tgellng  29016  legval  29047  legov  29048  legov2  29049  ishlg2  29065  ishlg  29068  mirreu3  29126  mirval  29127  mirfv  29128  mircgr  29129  mirbtwn  29130  ismir  29131  mireq  29137  symquadlem  29161  israg  29172  perpln1  29185  perpln2  29186  isperp  29187  islnopp  29215  outpasch  29233  ishpg  29237  tgplnfn  29253  plngval  29255  isplng  29256  elplng  29258  elplngid  29260  lnincplng  29262  plngcplem  29263  plngcp  29264  plngrot  29268  nhpmirhp  29276  lnperpexs  29310  iscgra  29316  dfcgra2  29338  ragraghl  29346  tgaaddcpbllem2  29350  tgaaddcpbl2  29353  isinag  29357  isleag  29366  cgrabasimass  29378  angmgmaddeu1  29379  angmgmval  29394  iseqlg  29412  brprlng  29416  prlnghpg  29424  prlngmo  29432  f1otrgitv  29447  f1otrg  29448  f1otrge  29449  ttgval  29452  ttgelitv  29460  elee  29471  brbtwn  29477  brcgr  29478  axlowdimlem16  29535  ebtwntg  29560  elntg2  29563  upgrex  29670  edgupgr  29712  upgredg  29715  edglnl  29721  numedglnl  29722  uhgr2edg  29789  umgr2edg1  29792  usgredg2vlem1  29806  usgredg2vlem2  29807  ushgredgedg  29810  ushgredgedgloop  29812  uhgrspansubgrlem  29871  fusgrfisstep  29910  nbgrval  29917  nbgrel  29921  nbupgrel  29926  nbgr2vtx1edg  29931  nbuhgr2vtx1edgblem  29932  nbuhgr2vtx1edgb  29933  nbusgreledg  29934  usgrnbcnvfv  29946  uvtxval  29968  uvtxel  29969  uvtx01vtx  29978  uvtxusgrel  29984  nbcplgr  30015  cplgr3v  30016  cusgrexi  30024  structtocusgr  30027  vtxdgfval  30048  vtxdg0v  30054  vtxdeqd  30058  vtxdun  30062  1loopgrnb0  30083  1loopgrvd0  30085  1hevtxdg0  30086  1hevtxdg1  30087  1egrvtxdg1  30090  umgr2v2evtxel  30103  umgr2v2enb1  30107  umgr2v2evd2  30108  vtxdginducedm1lem4  30123  vtxdginducedm1  30124  finsumvtxdg2sstep  30130  ewlksfval  30182  isewlk  30183  wksfval  30190  iswlk  30191  uspgr2wlkeq  30226  wlkres  30249  pfxwlk  30266  revwlk  30267  dfpth2  30314  usgr2pthlem  30349  clwlkcompim  30367  uspgrn2crct  30397  wwlks  30424  iswwlksn  30427  wwlknvtx  30434  wlkiswwlks2  30464  wwlksm1edg  30470  wwlksnred  30481  wwlksnext  30482  wwlksnredwwlkn  30484  wwlksnredwwlkn0  30485  wwlksnwwlksnon  30504  wspn0  30513  usgr2wspthons3  30556  rusgrnumwwlkb0  30563  clwwlk  30574  clwwlkccatlem  30580  clwlkclwwlklem2a4  30588  clwlkclwwlk  30593  clwwisshclwwslem  30605  clwwlkinwwlk  30631  clwwlkel  30637  clwwlkf  30638  clwwlkext2edg  30647  wwlksext2clwwlk  30648  wwlksubclwwlk  30649  clwwnisshclwwsn  30650  eleclclwwlknlem2  30652  erclwwlknsym  30661  erclwwlkntr  30662  umgrhashecclwwlk  30669  clwwlkvbij  30704  eupth2lem3lem3  30831  eupth2lem3lem4  30832  eupth2lem3lem6  30834  eupth2lemb  30838  eucrct2eupth  30846  fusgreg2wsplem  30934  2clwwlklem  30944  2clwwlk2clwwlklem  30947  2clwwlkel  30950  2clwwlk2clwwlk  30951  extwwlkfabel  30954  clwwlknonclwlknonf1o  30963  dlwwlknondlwlknonf1olem1  30965  numclwwlk2lem1  30977  numclwlk2lem2f  30978  numclwlk2lem2f1o  30980  ex-res  31042  isssp  31326  sspn  31338  islno  31355  isblo  31384  nmlno0  31397  ishmo  31413  dipdir  31444  dipass  31447  ubthlem1  31472  ubthlem2  31473  htthlem  31519  htth  31520  ocel  31883  ocnel  31900  shsel  31916  shsel2  31924  shmodsi  31991  pjhtheu  31996  pjeq  32001  axpjpj  32022  pjoc2  32041  elspani  32145  h1de2ctlem  32157  elspansn  32168  elspansn2  32169  elnlfn  32530  eleigvec  32559  riesz3i  32664  cbviunf  33150  iuneq12daf  33151  iunrdx  33158  iunrnmptss  33159  cbvdisjf  33165  disjorf  33173  disjabrex  33176  disjabrexf  33177  iundisjf  33183  disjrdx  33185  fresunsn  33219  2ndresdju  33243  abfmpunirn  33246  abfmpeld  33248  abfmpel  33249  fmptcof2  33251  acunirnmpt2  33254  acunirnmpt2f  33255  aciunf1lem  33256  suppss3  33315  fpwrelmap  33325  xrofsup  33359  iundisjfi  33388  eliccioo  33497  s3f1  33511  ccatws1f1o  33514  ismnt  33544  mgcoval  33547  gsummpt2co  33609  gsumpart  33624  gsumhashmul  33628  gsummulsubdishift1  33629  xrge0tsmsbi  33635  gsumwrd2dccatlem  33638  gsumwrd2dccat  33639  cycpmco2  33694  cyc3co2  33701  isfxp  33729  cntrval2  33732  inftmrel  33741  isinftm  33742  isslmd  33763  urpropd  33791  elrgspn  33807  erlval  33819  rlocval  33820  rloccring  33832  rloc1r  33834  rlocisunit  33837  domnprodeq0  33840  domnpropd  33841  fracfld  33870  resv1r  33900  ellspds  33924  ellpi  33928  lbslsp  33932  rhmimaidl  33982  ismxidl  33987  crngmxidl  33994  drng0mxidl  34000  opprqus0g  34014  qsfld  34022  isrprm  34049  rsprprmprmidlb  34055  ressply1evls1  34097  ply1mulrtss  34114  ply1coedeg  34121  psrmonmul  34182  dimpropd  34241  lbslsat  34248  extdg1id  34298  fldextrspunlsplem  34305  fldextrspunlsp  34306  elirng  34318  ply1annidllem  34333  constrsuc  34370  constrconj  34377  constrllcllem  34384  constrlccllem  34385  constrcccllem  34386  nn0constr  34393  smatrcl  34428  smatcl  34434  ist0cld  34465  txomap  34466  locfinreflem  34472  zarclsiin  34503  zart0  34511  rhmpreimacnlem  34516  metidval  34522  cnre2csqima  34543  ordtrest2NEW  34555  fmcncfil  34563  fsumcvg4  34582  ofcfval  34730  measvuni  34847  meascnbl  34852  faeval  34879  ismbfm  34884  elunirnmbfm  34885  imambfm  34894  elcarsg  34937  itgeq12dv  34958  issibf  34965  eulerpartlems  34992  eulerpartlemgc  34994  eulerpartlemgvv  35008  eulerpartlemgu  35009  eulerpart  35014  rrvmbfm  35074  elorvc  35092  elorrvc  35096  dstfrvunirn  35107  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemsima  35148  ballotlemrv  35152  fzssfzo  35171  signstfvn  35198  signstfvneq0  35201  signstres  35204  repr0  35240  reprinrn  35247  reprdifc  35256  hgt750lemg  35283  hgt750lemb  35285  istrkg2d  35295  axtgupdim2ALTV  35297  afsval  35303  brafs  35304  bnj945  35404  bnj1400  35465  bnj18eq1  35557  bnj916  35563  bnj1014  35591  bnj1015  35592  bnj1110  35612  bnj1417  35671  r1ssel  35732  acnum  35755  onvf1odlem3  35884  vonf1wev  35887  vonf1owevOLD  35889  vonf1osev  35891  cplgredgex  35905  subfacp1lem2b  35946  subfacp1lem4  35948  subfacp1lem5  35949  subfacp1lem6  35950  ptpconn  35998  cvmscbv  36023  iscvm  36024  cvmsi  36030  cvmsval  36031  cvmliftmolem1  36046  cvmlift2lem12  36079  cvmlift2lem13  36080  cvmlift3lem7  36090  snmlval  36096  satfv1  36128  satfvsucsuc  36130  satfrnmapom  36135  satf0op  36142  satf0n0  36143  sat1el2xp  36144  fmlafvel  36150  isfmlasuc  36153  fmlaomn0  36155  gonan0  36157  goaln0  36158  gonar  36160  goalr  36162  satffunlem1lem2  36168  satffunlem2lem2  36171  satfv0fvfmla0  36178  satef  36181  satefvfmla0  36183  sategoelfvb  36184  satfv1fvfmla1  36188  mrsubfval  36273  mrsubvrs  36287  mclsrcl  36326  mclsval  36328  mppsval  36337  mclsppslem  36348  opelco3  36539  wsuclem  36587  funtransport  36796  fvtransport  36797  brcolinear  36824  colineardim1  36826  funray  36905  fvray  36906  funline  36907  fvline  36909  lineelsb2  36913  fwddifval  36927  fwddifnval  36928  rankeq1o  36932  nmulprop  36939  nmulr0  36944  nmuladdel  36961  ltnmul  36965  ltnadd  36967  rmoeqbidv  37002  disjeq12dv  37004  ixpeq12dv  37005  prodeq12sdv  37007  itgeq12sdv  37008  cbvralvw2  37015  cbvrexvw2  37016  cbvrmovw2  37017  cbvreuvw2  37018  cbvcsbvw2  37020  cbviunvw2  37021  cbviinvw2  37022  cbvmptvw2  37023  cbvdisjvw2  37024  cbvmpo1vw2  37032  cbvmpo2vw2  37033  cbvsbcdavw  37046  cbvcsbdavw  37048  cbvcsbdavw2  37049  cbviundavw  37051  cbviindavw  37052  cbvdisjdavw  37057  cbvrabdavw2  37074  cbviundavw2  37075  cbviindavw2  37076  cbvmptdavw2  37077  cbvdisjdavw2  37078  cbvriotadavw2  37079  cbvmpo1davw2  37081  cbvmpo2davw2  37082  cbvsumdavw2  37084  neibastop2lem  37148  neibastop3  37150  eltail  37162  ttctr  37281  dfttc2g  37294  mh-infprim2bi  37335  bj-projeq  37905  bj-projval  37909  bj-restsn  38003  opelopabbv  38065  brabd0  38069  bj-eldiag  38098  bj-eldiag2  38099  mptsnunlem  38262  dissneqlem  38264  iooelexlt  38286  relowlssretop  38287  rdgellim  38300  exrecfnlem  38303  finxpeq1  38310  finxpreclem6  38320  pibp21  38339  curunc  38526  unccur  38527  fin2so  38531  lindsadd  38537  ptrest  38538  ptrecube  38539  poimirlem2  38541  poimirlem8  38547  poimirlem17  38556  poimirlem18  38557  poimirlem20  38559  poimirlem21  38560  poimirlem22  38561  poimirlem24  38563  poimirlem26  38565  poimirlem29  38568  heicant  38574  mblfinlem1  38576  mblfinlem2  38577  volsupnfl  38584  itg2addnclem  38590  itg2gt0cn  38594  indexdom  38669  incsequz  38683  istotbnd  38704  istotbnd3  38706  0totbnd  38708  sstotbnd  38710  sstotbnd3  38711  isbnd  38715  prdstotbnd  38729  cntotbnd  38731  isismty  38736  heibor1lem  38744  heiborlem2  38747  heiborlem3  38748  heibor  38756  isass  38781  exidcl  38811  exidreslem  38812  elghomlem2OLD  38821  rngoidmlem  38871  rngo1cl  38874  divrngcl  38892  isdrngo2  38893  isrngohom  38900  isrngoiso  38913  isriscg  38919  iscom2  38930  iscringd  38933  isidl  38949  ispridl  38969  ismaxidl  38975  ac6s6  39105  dmecd  39243  dfpre4  39413  releldmqs  39676  releldmqscoss  39678  erimeq2  39696  qmapeldisjsim  39793  eldisjlem19  39846  membpartlem19  39847  prter3  39940  islshp  40037  islsat  40049  lcvfbr  40078  islfl  40118  ellkr  40147  islshpkrN  40178  ldual1dim  40224  isopos  40238  cmtfvalN  40268  cvrfval  40326  isat  40344  islln  40564  islpln  40588  islvol  40631  isline  40797  ispointN  40800  ispsubsp  40803  elpmap  40816  elpmapat  40822  elpadd  40857  paddclN  40900  elpclN  40950  elpcliN  40951  pclfinN  40958  pclcmpatN  40959  ispsubclN  40995  iswatN  41052  islhp  41054  islaut  41141  ispautN  41157  isldil  41168  isltrn  41177  isdilN  41212  istrnN  41215  istendo  41818  dvhb1dimN  42044  erng1lem  42045  erngdvlem4-rN  42057  diaelval  42091  diaeldm  42094  dia1dimid  42121  cdlemm10N  42176  dibopelvalN  42201  dibopelval2  42203  dibelval3  42205  dibelval1st  42207  dibelval2nd  42210  dibeldmN  42216  dibvalrel  42221  dibglbN  42224  dicffval  42232  dicfval  42233  dicopelval  42235  dicelvalN  42236  dicelval3  42238  dicvalrelN  42243  dicelval1sta  42245  diclspsn  42252  dihopelvalbN  42296  dihopelvalcqat  42304  dihopelvalcpre  42306  dihvalrel  42337  dih1  42344  dihmeetlem4preN  42364  dihmeetlem13N  42377  dih1dimatlem  42387  dochnel2  42450  dihjatcclem4  42479  dvh2dim  42503  dvh3dim  42504  dvh4dimN  42505  dochfln0  42535  lpolsetN  42540  islpolN  42541  lcfrvalsnN  42599  lcfrlem21  42621  lcfrlem27  42627  lcfrlem37  42637  lcfr  42643  lcdlss  42677  mapdcv  42718  hdmap1fval  42854  hdmapffval  42884  hdmapfval  42885  hdmapval  42886  hgmapffval  42943  hgmapfval  42944  hdmapellkr  42972  hlhilhillem  43018  fzsplitnd  43033  isprimroot  43144  primrootsunit1  43148  primrootscoprmpow  43150  primrootscoprbij  43153  aks6d1c1p2  43160  aks6d1c1p3  43161  aks6d1c1p4  43162  aks6d1c1p5  43163  aks6d1c1p6  43165  aks6d1c1  43167  evl1gprodd  43168  sticksstones11  43207  sticksstones12a  43208  rhmqusspan  43236  grpods  43245  fzosumm1  43302  frlmfielbas  43568  frlmsnic  43605  psrmnd  43608  prjspnnorm  43662  isnacs  43715  mrefg2  43718  elmzpcl  43737  mzpcompact2  43763  eldiophb  43768  elpell1qr  43854  elpell14qr  43856  elpell1234qr  43858  pw2f1ocnv  44044  pw2f1o2val2  44047  aomclem4  44059  aomclem6  44061  islssfg2  44073  imasgim  44102  lnr2i  44118  elmnc  44138  rngunsnply  44171  onexomgt  44243  onexlimgt  44245  onexoegt  44246  oaordnr  44298  omnord1  44307  oenord1  44318  cantnfresb  44326  tfsconcatun  44339  tfsconcat0i  44347  ofoaf  44357  naddcnff  44364  naddcnffo  44366  naddcnfcom  44368  naddcnfid1  44369  naddcnfid2  44370  naddcnfass  44371  naddwordnexlem4  44403  fiinfi  44574  sqrtcvallem1  44631  elintima  44653  eliunov2  44679  ov2ssiunov2  44700  brtrclfv2  44727  rfovcnvf1od  45004  rfovcnvfvd  45007  fsovrfovd  45009  fsovfvd  45010  fsovcnvlem  45013  ntrclsfv1  45055  ntrclselnel1  45057  ntrclsneine0lem  45064  ntrneifv1  45079  ntrneifv2  45080  ntrneiel  45081  gneispace2  45132  gneispacess2  45146  extoimad  45164  mnringelbased  45215  dvconstbi  45318  bccbc  45329  wfac8prim  45992  permaxrep  45996  permac8prim  46004  eliin2f  46119  iineq12dv  46121  rabbida2  46147  disjinfi  46207  unirnmap  46221  elmptima  46270  iuneqfzuzlem  46346  iooiinioc  46568  fsumiunss  46587  fsumsupp0  46590  lptre2pt  46650  icccncfext  46897  cncfiooicclem1  46903  dvnprodlem2  46957  stoweidlem27  47037  stoweidlem29  47039  stoweidlem31  47041  stoweidlem34  47044  stoweidlem48  47058  stoweidlem59  47069  dirkercncflem2  47114  dirkercncflem4  47116  fourierdlem2  47119  fourierdlem3  47120  fourierdlem25  47142  fourierdlem32  47149  fourierdlem33  47150  fourierdlem41  47158  fourierdlem48  47164  fourierdlem49  47165  fourierdlem62  47178  fourierdlem70  47186  fourierdlem80  47196  fourierdlem92  47208  fourierdlem93  47209  fourierdlem101  47217  etransclem37  47281  sge0val  47376  sge0f1o  47392  sge0iunmptlemre  47425  sge0iunmpt  47428  iundjiun  47470  caragenel  47505  ovncvrrp  47574  ovnsubaddlem1  47580  ovnsubadd  47582  hoidmvlelem2  47606  hoidmvlelem3  47607  hoidmvlelem4  47608  hoidmvle  47610  ovncvr2  47621  hspdifhsp  47626  hoiqssbl  47635  hspmbllem2  47637  hspmbl  47639  opnvonmbllem1  47642  isvonmbl  47648  ovnovollem1  47666  issmflem  47737  smflimlem3  47783  smflimlem4  47784  smflim  47787  smfmullem2  47802  smflimmpt  47820  smfsuplem1  47821  smflimsuplem1  47830  smflimsuplem3  47832  smflimsuplem4  47833  smflimsuplem7  47836  smflimsup  47838  chnsubseq  47890  tmachlem-agreeprod  47947  tmachlem-tpopen  47951  tmachlem-agreesn  47957  fcores  48137  fcoresf1  48139  afvelrnb  48233  afvelrnb0  48234  afv2co2  48327  el1fzopredsuc  48396  muldvdsfacm1  48457  iccpart  48498  iccpartgtprec  48502  iccpartiltu  48504  iccpartigtl  48505  iccpartltu  48507  iccpartgtl  48508  iccpartgt  48509  iccpartleu  48510  iccpartgel  48511  iccelpart  48515  iccpartiun  48516  icceuelpart  48518  fargshiftfv  48521  fargshiftfo  48524  sprel  48566  prprelb  48598  prprelprb  48599  nprmdvdsfacm1lem4  48708  fpprel  48826  sbgoldbo  48885  wtgoldbnnsum4prm  48900  bgoldbnnsum3prm  48902  bgoldbtbndlem3  48905  bgoldbtbnd  48907  clnbgrval  48920  elclnbgrelnbgr  48923  clnbgrel  48926  clnbupgrel  48932  vopnbgrel  48952  isubgredg  48964  upgrimwlklem3  48997  upgrimwlklem5  48999  upgrimpths  49007  grtriprop  49039  isgrtri  49041  grtriclwlk3  49043  stgredgel  49055  gpgvtxel  49145  gpgiedgdmel  49147  gpgedgel  49148  opgpgvtx  49153  gpg5nbgrvtx13starlem1  49169  gpg5nbgrvtx13starlem2  49170  gpg5nbgrvtx13starlem3  49171  gpg3kgrtriex  49187  grlimedgnedg  49229  upwlksfval  49233  isupwlk  49234  intop  49300  isclintop  49304  assintop  49306  isassintop  49307  assintopcllaw  49309  uzlidlring  49332  elrngchomALTV  49366  rngccatidALTV  49369  rngcsectALTV  49372  rngcisoALTV  49374  rhmsubcALTVlem3  49380  rhmsubcALTVlem4  49381  funcringcsetcALTV2lem7  49393  funcringcsetcALTV2lem9  49395  elringchomALTV  49400  ringccatidALTV  49403  ringcsectALTV  49406  ringcisoALTV  49408  ringcbasbasALTV  49409  funcringcsetclem7ALTV  49416  funcringcsetclem9ALTV  49418  srhmsubcALTV  49422  smprngprmrng  49436  cbvmpox2  49448  ply1sclrmsm  49496  dmatALTbasel  49514  lcoval  49524  lindslinindsimp1  49569  lindslinindsimp2  49575  lmod1  49604  elbigo  49663  elbigo2  49664  elbigolo1  49669  dig2nn0ld  49716  naryfvalel  49742  rrxlines  49845  rrxlinesc  49847  rrxlinec  49848  eenglngeehlnm  49851  elrrx2linest2  49857  rrxsphere  49860  itsclc0  49883  itsclc0b  49884  itsclinecirc0  49885  itsclinecirc0b  49886  itscnhlinecirc02p  49897  brab2dd  49938  f1omo  50001  f1omoOLD  50002  lubeldm2d  50066  glbeldm2d  50067  catprs  50119  sectpropdlem  50144  nelsubc3lem  50178  initc  50199  imaid  50262  upfval  50284  upfval2  50285  upfval3  50286  uppropd  50289  oppcinito  50343  oppctermo  50344  oppczeroo  50345  initopropd  50351  termopropd  50352  isthinc  50527  isthincd2lem1  50533  thincmoALT  50537  thincmod  50538  isthincd  50544  thincpropd  50550  indcthing  50568  discthing  50569  prsthinc  50572  termcterm  50621  termc2  50626  isinito4  50655  2arwcatlem1  50703  setc1onsubc  50710  cnelsubclem  50711  ranval3  50739  lmdfval2  50763  cmdfval2  50764  termolmd  50778  elsetrecslem  50792