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 1866	. . 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 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  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  3624  sbcbid  3793  sbcbi2  3797  csbeq2d  3853  csbeq2dv  3854  cbvcsbw  3857  cbvcsb  3858  cbvcsbv  3859  csbie  3882  csbied  3883  csbie2g  3887  cbvralcsf  3889  cbvreucsf  3891  cbvrabcsf  3892  sbcel12  4369  sbcel1g  4374  sbcel2  4376  prel12g  4824  eliuni  4957  iuneqconst  4963  iuneq12df  4978  iuneq12d  4980  cbviun  4993  cbviin  4994  cbviung  4995  cbviing  4996  cbviunv  4997  cbviinv  4998  iinxsng  5048  iinxprg  5049  iunxsng  5050  iunxsngf  5052  cbvdisj  5080  cbvdisjv  5081  disjor  5085  disjiund  5094  mpteq12da  5188  mpteq12f  5190  mpteq12dva  5191  axpweq  5315  rabxfrd  5382  brab2d  5516  rbropapd  5541  opeliunxp  5722  opeliun2xp  5723  opeliunxp2  5819  iunxpf  5830  elimampt  6041  elrelimasn  6084  elimasni  6089  xpdifid  6162  xpdifcnvepel  6163  imadifssranOLD  6200  ressn  6285  funfni  6641  fnbr  6643  dffv3  6877  elfv2ex  6924  fvelrnb  6941  foelcdmi  6942  fvun1  6972  fvco2  6978  funcnvmpt  6991  elfvmptrab1w  7017  elfvmptrab1  7018  elfvmptrab  7019  elpreima  7053  dff3  7096  fmptco  7126  fnelfp  7176  fnelnfp  7178  tpres  7203  fnprb  7210  fntpb  7211  funfvima3  7238  eluniima  7250  dff13  7254  f1ounsn  7276  f1eqcocnv  7305  isoini  7342  riotaeqdv  7374  mpoeq123dva  7490  cbvmpox  7509  elimampo  7553  ovelrn  7593  elovmpod  7661  elovmpo  7662  elovmporab  7663  elovmporab1w  7664  elovmporab1  7665  elovmpt3rab1  7677  fiun  7946  f1iun  7947  zfrep6OLD  7958  fmpox  8069  el2mpocsbcl  8087  el2mpocl  8088  bropopvvv  8092  bropfvvvv  8094  xpord2indlem  8150  xpord3inddlem  8157  elsuppfng  8172  elsuppfn  8173  suppfnss  8192  opeliunxp2f  8213  mpoxopn0yelv  8216  mpoxopovel  8223  rntpos  8242  mpocurryd  8272  fpr2  8308  wfr2  8331  onoviun  8337  smoel  8354  smoiso  8356  smoel2  8357  smo11  8358  tfrlem9  8379  oalimcl  8554  oaass  8555  omordi  8560  omordlim  8571  omlimcl  8572  odi  8573  omeulem1  8576  omeulem2  8577  oen0  8581  oeordi  8582  oeordsuc  8589  oelimcl  8595  oeeulem  8596  oeeui  8597  nnmordi  8626  oaabs2  8644  omabs  8646  omsmolem  8652  ereldm  8757  iiner  8796  elmapg  8845  elpmg  8849  curf  8876  uncf  8877  elixpsn  8951  ixpsnf1o  8952  boxriin  8954  omxpenlem  9083  pw2f1olem  9086  phplem2  9206  php3  9210  infn0  9279  elfi  9390  dffi3  9408  marypha2lem2  9413  ordiso2  9494  wemapsolem  9529  elharval  9540  inf3lemd  9613  inf3lem1  9614  inf3lem2  9615  inf3lem3  9616  cantnfs  9652  cantnfp1lem3  9666  cantnflem1b  9672  cantnflem1  9675  ttrclselem2  9712  trcl  9714  frr2  9749  r1sdom  9763  r1ordg  9767  r1pwss  9773  tz9.12lem3  9778  tz9.12  9779  r1elwf  9785  rankr1ai  9787  rankidb  9789  rankr1bg  9792  rankval2  9807  rankelg  9829  rankunb  9841  tcrank  9877  elhf2  9882  0hf  9885  acni  10073  acni2  10074  acndom  10079  infpwfien  10090  alephnbtwn  10099  cardaleph  10117  cardinfima  10125  iunfictbso  10142  dfac3  10149  dfac5lem5  10155  dfac5  10156  dfac9  10164  dfac12r  10174  kmlem2  10179  kmlem12  10189  kmlem13  10190  kmlem14  10191  ackbij2lem3  10267  ackbij2  10269  cofsmo  10296  alephsing  10303  fin23lem30  10369  isf32lem9  10388  itunisuc  10446  axcc2lem  10463  axcc3  10465  domtriomlem  10469  axdc2lem  10475  axdc2  10476  axdc3lem2  10478  axdc3lem4  10480  axdc4lem  10482  ac6c4  10508  zorn2lem1  10523  ttukeylem6  10541  pwcfsdom  10617  axregndlem2  10637  axinfndlem1  10639  axacndlem4  10644  axacnd  10646  pwfseqlem1  10692  inar1  10809  inatsk  10812  gruurn  10832  grur1  10854  eltskm  10877  genpelv  11034  eluz1  12916  elixx1  13432  elixx3g  13436  elioo2  13464  elfz1  13591  elfz2  13593  elfzp1  13654  fzpr  13659  fzsuc2  13662  fzrev3  13670  elfzp12  13683  fzm1  13687  elfzo  13741  fz0add1fz1  13816  elfzo0l  13837  elfzom1b  13847  fzosplitsni  13860  elfzr  13862  elfzlmr  13863  zmodidfzo  13986  seqp1  14105  seqf1o  14132  bcval  14393  bcpasc  14410  hashf1lem1  14545  fundmge2nop0  14592  wrdmap  14636  elovmpowrd  14648  ccatfval  14663  elfzelfzccat  14670  ccatlid  14677  ccatass  14679  ccatrn  14680  ccatf1  14681  ccatalpha  14685  swrdrn3  14747  swrdfv2  14756  ccatswrd  14763  swrdccat2  14764  pfxfv  14777  pfxeq  14790  ccatpfx  14795  swrdswrd  14799  swrdpfx  14801  pfxpfx  14802  cats1un  14815  swrdccatfn  14818  swrdccatin1  14819  pfxccatin12lem4  14820  pfxccatin12lem1  14822  swrdccatin2  14823  pfxccatin12lem2c  14824  pfxccatin12lem2  14825  swrdccat3blem  14833  swrdccatin1d  14837  swrdccatin2d  14838  pfxccatin12d  14839  revccat  14860  revrev  14861  revpfxsfxrev  14862  repswpfx  14881  repswccat  14882  cshwidxmod  14899  2cshw  14909  cshwcshid  14923  cshwcsh2id  14924  cshimadifsn  14925  cshimadifsn0  14926  revco  14930  ccatco  14931  cshco  14932  swrdco  14933  ofccat  15067  shftfn  15171  shftval  15172  limsupgle  15589  ello12  15628  elo12  15639  isercolllem3  15779  sumeq1  15801  fsumsplit  15852  sumsplit  15879  fsum2dlem  15881  fsumcom2  15885  fsumparts  15918  explecnv  15979  pwdif  15982  fprodser  16061  fprodsplit  16078  fprod2dlem  16092  fprodcom2  16096  eftlub  16222  divalgmod  16521  bitsval  16539  bitsp1e  16547  bitsp1o  16548  sadfval  16567  sadcp1  16570  sadval  16571  sadcadd  16573  sadadd2  16575  saddisjlem  16579  sadadd  16582  sadass  16586  smufval  16592  smuval  16596  smuval2  16597  smupvallem  16598  smu01lem  16600  smueqlem  16605  smumul  16608  bezoutlem2  16655  bezoutlem4  16657  algfx  16695  eucalgcvga  16701  reumodprminv  16921  nnnn0modprm0  16923  unbenlem  17025  prmreclem5  17037  vdwapval  17090  vdwapun  17091  vdwnnlem1  17112  vdwnn  17115  ramval  17125  0ram  17137  ramub1lem2  17144  prmgaplem7  17174  prmlem0  17222  elrest  17537  prdsbasmpt  17580  prdsleval  17587  prdsbasmpt2  17592  pwselbasb  17598  imasaddfnlem  17639  imasvscafn  17648  divsfval  17658  ismre  17699  mreunirn  17710  mrisval  17743  ismri  17744  isacs  17764  catidd  17793  iscatd2  17794  ismon  17847  isepi  17854  sectffval  17864  sectfval  17865  dfiso2  17886  cicsym  17918  issubc  17949  catsubcat  17953  isfunc  17978  funcres  18010  funcpropd  18016  ffthiso  18045  isnat  18064  isnat2  18065  fuciso  18092  initoval  18107  termoval  18108  isinito  18110  istermo  18111  iszeroo  18112  isinitoi  18113  istermoi  18114  initoid  18115  termoid  18116  iszeroi  18123  2initoinv  18124  initoeu1  18125  initoeu2  18130  2termoinv  18131  termoeu1  18132  arwhoma  18159  elsetchom  18195  setcmon  18201  setcepi  18202  setciso  18205  catciso  18225  elestrchom  18241  estrcbasbas  18244  funcestrcsetclem7  18259  funcestrcsetclem8  18260  funcestrcsetclem9  18261  fthestrcsetc  18263  fullestrcsetc  18264  equivestrcsetc  18265  setc1strwun  18266  funcsetcestrclem7  18274  funcsetcestrclem8  18275  funcsetcestrclem9  18276  fthsetcestrc  18278  fullsetcestrc  18279  hofcl  18372  hofpropd  18380  yonedalem4c  18390  yonedainv  18394  yonffthlem  18395  lubeldm  18464  glbeldm  18477  joindef  18487  meetdef  18501  poslubdg  18525  acsficl2d  18665  acsmapd  18667  psref  18687  psss  18693  dirge  18716  chnccats1  18738  chnccat  18739  chnrev  18740  mgmpropd  18768  issstrmgm  18770  grpidval  18779  grpidpropd  18781  grpidd  18791  imasmgm2  18802  ismgmhm  18824  issubmgm  18830  issgrpd  18858  sgrppropd  18859  ismndd  18885  mndpropd  18890  imasmnd2  18907  imasmnd  18908  xpsmnd0  18911  ismhm  18919  issubm  18937  gsumsgrpccat  18975  elefmndbas2  19009  smndex1mndlem  19047  imasgrp2  19204  imasgrp  19205  issubg  19275  subginv  19282  isnsg  19304  eqg0el  19337  quselbas  19338  isghm  19369  resghm2b  19387  conjnmzb  19406  conjnsg  19407  ghmpropd  19409  isga  19444  elcntz  19475  elcntzsn  19478  cntzrcl  19480  resscntz  19486  symgextf1  19574  gsmsymgreqlem2  19584  f1otrspeq  19600  pmtrfrn  19611  pmtrdifellem3  19631  pmtrdifellem4  19632  psgnunilem1  19646  psgnunilem5  19647  psgnunilem2  19648  psgnunilem3  19649  psgneldm2  19657  psgnfitr  19670  psgnsn  19673  gexdvds  19737  gex1  19744  isslw  19761  sylow3lem2  19781  lsmelvalx  19793  pj1ghm  19856  efgtlen  19879  efgsfo  19892  efgredlemc  19898  frgp0  19913  frgpmhm  19918  qusabl  20018  frgpnabllem1  20026  imasabl  20029  cycsubmcmn  20042  0cyg  20046  cycsubgcyg  20054  gsumval3  20060  gsumcllem  20061  gsumzaddlem  20074  gsumzsplit  20080  gsummptfzcl  20122  eldprd  20159  dprdcntz2  20193  dprd2d2  20199  dmdprdsplit2lem  20200  dmdprdsplit2  20201  dprdsplit  20203  ablfac2  20244  isrngd  20334  rngpropd  20335  imasrng  20338  qusrng  20341  ringurd  20350  isringd  20461  imasring  20499  xpsring1d  20502  dvdsrval  20530  isunit  20542  dvdsrpropd  20585  isirred  20588  isrnghm  20610  isrngim  20614  c0ghm  20630  c0snghm  20633  isrhm0  20645  isrhm  20648  isrim0  20652  crngrhmfo  20665  islring  20731  issubrng  20738  opprsubrng  20750  issubrg  20762  opprsubrg  20784  resrhm2b  20793  rhmpropd  20800  rnghmresel  20811  elrngchom  20815  rnghmsubcsetclem1  20822  rnghmsubcsetclem2  20823  rngcid  20826  rngcsect  20827  rngciso  20829  funcrngcsetcALT  20832  zrinitorngc  20833  zrtermorngc  20834  rhmresel  20840  elringchom  20844  rhmsubcsetclem1  20851  rhmsubcsetclem2  20852  ringcid  20855  rhmsscrnghm  20856  rhmsubcrngclem1  20857  rhmsubcrngclem2  20858  ringcsect  20861  ringciso  20863  ringcbasbas  20864  zrtermoringc  20866  srhmsubc  20871  rhmsubclem3  20878  rhmsubclem4  20879  drngunit  20924  isdrng4  20931  isdrngd  20961  isdrngdOLD  20963  issdrg  20984  sdrgunit  20992  isabv  21007  issrngd  21051  islmod  21078  lmodprop2d  21138  islss  21148  islssd  21149  lssats2  21214  ellspsn  21217  islmhm  21241  lmhmf1o  21260  lmhmima  21261  lmhmpreima  21262  reslmhm  21266  pwssplit3  21275  lmhmpropd  21287  islbs  21290  lspprel  21308  lspfixed  21345  lbsacsbs  21373  lbsextlem1  21375  lbsextlem2  21376  lbsextlem3  21377  lbsextlem4  21378  ixpsnbasval  21422  isridlrng  21437  rnglidlmmgm  21472  isridl  21484  quscrng  21518  rngqiprngimfolem  21525  rngqiprngimf1lem  21529  rngqiprngimfo  21536  isprmidl  21558  qsidomlem1  21575  qsidomlem2  21576  islpidl  21588  lidldvgen  21597  irinitoringc  21724  pzriprnglem13  21738  pzriprnglem14  21739  zrhrhmb  21755  znf1o  21796  frgpcyg  21818  psgnevpmb  21832  isphld  21899  phlssphl  21904  elocv  21913  iscss  21928  isobs  21965  obs2ss  21974  dsmmfi  21983  dsmmelbas  21984  dsmmlss  21989  frlmelbas  22001  frlmlbs  22042  frlmup1  22043  ellspd  22047  islinds  22054  islindf2  22059  f1lindf  22067  islindf4  22083  lindsdom  22095  lindsenlbs  22096  assamulgscmlem2  22147  psrgrp  22203  mplsubglem  22245  mpllsslem  22246  mplmonmul  22284  subrgascl  22314  subrgasclcl  22315  mpfind  22363  ismhp  22400  gsumply1subr  22490  lply1binomsc  22568  matbas2d  22677  matecl  22679  matvscl  22685  mat1  22701  mat0dim0  22721  mat0dimid  22722  mat0dimscm  22723  mat1dimelbas  22725  dmatel  22747  scmatel  22759  scmateALT  22766  scmataddcl  22770  scmatsubcl  22771  smatvscl  22778  scmatghm  22787  mat1scmat  22793  mdetunilem7  22872  mdetunilem9  22874  smadiadetr  22929  matunitlindflem1  22933  matunitlindflem2  22934  matunitlindf  22935  cramerimplem2  22941  cramer0  22947  pmatcoe1fsupp  22958  cpmatpmat  22967  cpmatel  22968  cpmatacl  22973  cpmatinvcl  22974  mat2pmatghm  22987  mat2pmatmul  22988  decpmatmullem  23028  pmatcollpwlem  23037  pmatcollpw3fi1lem1  23043  pmatcollpwscmatlem1  23046  monmat2matmon  23081  chfacfscmul0  23115  chfacfscmulgsum  23117  chfacfpmmulgsum  23121  cayhamlem1  23123  cpmadugsumlemB  23131  cpmadugsumlemC  23132  cpmadugsumlemF  23133  cayhamlem2  23141  istopon  23169  eltg  23214  eltg2  23215  eltop  23231  eltop2  23232  eltop3  23233  pptbas  23265  iscld  23284  neiss2  23358  isnei  23360  neiptopnei  23389  neiptopreu  23390  lpfval  23395  lpval  23396  islp  23397  maxlp  23404  islpi  23406  neitr  23437  restlp  23440  ordtbas2  23448  ordtrest2  23461  lmfval  23489  cnfval  23490  iscn  23492  iscnp  23494  tgcn  23509  tgcnp  23510  lmbrf  23517  cnpresti  23545  ist1  23578  ist1-2  23604  cnt1  23607  haust1  23609  cmpfi  23665  cmpfii  23666  1stcfb  23702  2ndc1stc  23708  1stcrest  23710  2ndcdisj  23714  1stcelcls  23719  nllyi  23733  subislly  23739  islocfin  23775  lfinpfin  23782  locfindis  23788  locfincf  23789  comppfsc  23790  kgenval  23793  elkgen  23794  kgencn2  23815  txbas  23825  eltx  23826  ptval  23828  ptpjpre1  23829  ptopn2  23842  ptpjopn  23870  ptclsg  23873  xkoccn  23877  txdis  23890  txdis1cn  23893  ptrescn  23897  hausdiag  23903  hauseqlcld  23904  txhaus  23905  xkohaus  23911  elqtop  23955  qtopeu  23974  kqcldsat  23991  hmeofval  24016  ptuncnv  24065  ptunhmeo  24066  elmptrab  24085  fbdmn0  24092  elfg  24129  elfilss  24134  filunirn  24140  fixufil  24180  elfm  24205  rnelfmlem  24210  rnelfm  24211  fmfnfmlem4  24215  elflim2  24222  flimtopon  24228  elflim  24229  hausflim  24239  flimcls  24243  flfnei  24249  isflf  24251  hausflf  24255  cnpflf  24259  cnflf  24260  txflf  24264  isfcls  24267  fclstopon  24270  isfcls2  24271  fclssscls  24276  fclsnei  24277  fclsfnflim  24285  flimfnfcls  24286  isfcf  24292  fcfelbas  24294  cnpfcf  24299  cnfcf  24300  flfcntr  24301  alexsublem  24302  alexsubALTlem3  24307  cnextfun  24322  cnextfvval  24323  cnextf  24324  cnextcn  24325  tmdgsum2  24354  tgpconncomp  24371  ghmcnp  24373  qustgplem  24379  eltsms  24391  haustsms  24394  tsmsgsum  24397  tsmssubm  24401  tsmssplit  24410  isust  24462  ustbas  24485  elutop  24491  ustuqtoplem  24497  ustuqtop4  24502  ustuqtop  24504  utopsnneiplem  24505  utopsnneip  24506  utopsnnei  24507  isusp  24519  isucn  24535  ucncn  24542  iscfilu  24545  neipcfilu  24553  iscusp  24556  cnextucn  24560  ispsmet  24562  ismet  24581  isxmet  24582  elblps  24645  elbl  24646  elmopn  24700  prdsbl  24749  neibl  24759  met1stc  24779  metrest  24782  prdsxmslem2  24787  txmetcnp  24805  txmetcn  24806  metustsym  24813  cfilucfil2  24819  elbl4  24821  metuel  24822  psmetutop  24825  restmetu  24828  metucn  24829  tngngp  24912  isnmhm  25004  zcld  25072  metnrmlem1a  25117  elcncf  25149  cncfcnvcn  25185  cnheibor  25215  lebnumlem1  25221  ishtpy  25232  isphtpy  25241  om1elbas  25292  elpi1  25305  pi1xfr  25315  pi1coghm  25321  tcphcph  25497  lmmbrf  25522  iscfil  25525  iscau  25536  iscauf  25540  caucfil  25543  iscmet  25544  cmetcaulem  25548  iscmet3lem1  25551  iscmet3lem2  25552  iscmet3  25553  bcthlem1  25584  cmsss  25611  cmetcusp1  25613  cmetcusp  25614  cmscsscms  25633  rrxcph  25652  minveclem3b  25688  ovolfioo  25727  ovolficc  25728  ovolctb  25750  ovoliunnul  25767  ovolshftlem1  25769  sca2rab  25772  ovolscalem1  25773  ovolicc2lem1  25777  ovolicc2lem2  25778  ovolicc2lem4  25780  ovolicc2lem5  25781  iundisj  25808  iunmbl2  25817  uniioombllem3  25845  vitalilem2  25869  vitalilem3  25870  mbfss  25906  i1faddlem  25953  i1fmullem  25954  mbfi1fseqlem2  25976  mbfi1fseqlem4  25978  mbfi1fseq  25981  itg2splitlem  26008  itg2split  26009  itg2monolem1  26010  itg2gt0  26020  isibl  26025  iblss2  26065  itgss3  26074  itgsplit  26095  ellimc  26132  limcmo  26141  cnlimc  26147  limciun  26153  limcun  26154  eldv  26157  dvbsss  26161  dvreslem  26168  elcpn  26193  dvaddf  26201  dvmulf  26202  dvcof  26207  rolle  26249  dvlip2  26254  dvivthlem1  26267  lhop1  26273  lhop2  26274  ftc1cn  26302  fta1glem2  26426  plyco0  26449  elply  26452  ply1termlem  26460  eltayl  26628  tayl0  26630  taylplem1  26631  taylplem2  26632  dvtaylp  26638  taylthlem1  26641  taylthlem2  26642  abelth  26709  cxpcn3  27017  rlimcnp  27234  fsumharmonic  27280  dchrelbas  27504  pntrsumbnd2  27835  ostth2lem2  27902  nolesgn2ores  27940  nogesgn1ores  27942  nosupprefixmo  27968  noinfprefixmo  27969  nosupcbv  27970  nosupdm  27972  nosupfv  27974  nosupres  27975  nosupbnd1lem1  27976  nosupbnd1lem3  27978  nosupbnd1lem5  27980  nosupbnd2lem1  27983  noinfcbv  27985  noinfdm  27987  noinffv  27989  noinfres  27990  noinfbnd1lem1  27991  noinfbnd1lem3  27993  noinfbnd1lem5  27995  noinfbnd2lem1  27998  elmade  28154  elold  28156  sltsleft  28157  sltsright  28158  oldlim  28184  madebday  28197  newbday  28199  ltslpss  28205  bdayiun  28212  cofcutr  28221  cofcutrtime  28224  lrrecval  28236  lrrecval2  28237  addsval  28259  precsexlem9  28512  precsexlem11  28514  ltonold  28558  onnolt  28563  onlts  28564  noseqrdgfn  28603  istrkgb  28828  istrkgcb  28829  istrkge  28830  istrkgl  28831  istrkgld  28832  axtgsegcon  28837  axtg5seg  28838  axtgbtwnid  28839  axtgpasch  28840  axtgupdim2  28844  axtgeucl  28845  tgsegconeu  28860  tgdim01  28881  iscgrg  28886  isismt  28908  tglnunirn  28922  tglngval  28925  tgellng  28927  legval  28958  legov  28959  legov2  28960  ishlg2  28976  ishlg  28979  mirreu3  29037  mirval  29038  mirfv  29039  mircgr  29040  mirbtwn  29041  ismir  29042  mireq  29048  symquadlem  29072  israg  29083  perpln1  29096  perpln2  29097  isperp  29098  islnopp  29126  outpasch  29144  ishpg  29148  tgplnfn  29164  plngval  29166  isplng  29167  elplng  29169  elplngid  29171  lnincplng  29173  plngcplem  29174  plngcp  29175  plngrot  29179  nhpmirhp  29187  lnperpexs  29221  iscgra  29227  dfcgra2  29249  ragraghl  29257  tgaaddcpbllem2  29261  tgaaddcpbl2  29264  isinag  29268  isleag  29277  cgrabasimass  29289  angmgmaddeu1  29290  angmgmval  29305  iseqlg  29323  brprlng  29327  prlnghpg  29335  prlngmo  29343  f1otrgitv  29358  f1otrg  29359  f1otrge  29360  ttgval  29363  ttgelitv  29371  elee  29382  brbtwn  29388  brcgr  29389  axlowdimlem16  29446  ebtwntg  29471  elntg2  29474  upgrex  29581  edgupgr  29623  upgredg  29626  edglnl  29632  numedglnl  29633  uhgr2edg  29700  umgr2edg1  29703  usgredg2vlem1  29717  usgredg2vlem2  29718  ushgredgedg  29721  ushgredgedgloop  29723  uhgrspansubgrlem  29782  fusgrfisstep  29821  nbgrval  29828  nbgrel  29832  nbupgrel  29837  nbgr2vtx1edg  29842  nbuhgr2vtx1edgblem  29843  nbuhgr2vtx1edgb  29844  nbusgreledg  29845  usgrnbcnvfv  29857  uvtxval  29879  uvtxel  29880  uvtx01vtx  29889  uvtxusgrel  29895  nbcplgr  29926  cplgr3v  29927  cusgrexi  29935  structtocusgr  29938  vtxdgfval  29959  vtxdg0v  29965  vtxdeqd  29969  vtxdun  29973  1loopgrnb0  29994  1loopgrvd0  29996  1hevtxdg0  29997  1hevtxdg1  29998  1egrvtxdg1  30001  umgr2v2evtxel  30014  umgr2v2enb1  30018  umgr2v2evd2  30019  vtxdginducedm1lem4  30034  vtxdginducedm1  30035  finsumvtxdg2sstep  30041  ewlksfval  30093  isewlk  30094  wksfval  30101  iswlk  30102  uspgr2wlkeq  30137  wlkres  30160  pfxwlk  30177  revwlk  30178  dfpth2  30225  usgr2pthlem  30260  clwlkcompim  30278  uspgrn2crct  30308  wwlks  30335  iswwlksn  30338  wwlknvtx  30345  wlkiswwlks2  30375  wwlksm1edg  30381  wwlksnred  30392  wwlksnext  30393  wwlksnredwwlkn  30395  wwlksnredwwlkn0  30396  wwlksnwwlksnon  30415  wspn0  30424  usgr2wspthons3  30467  rusgrnumwwlkb0  30474  clwwlk  30485  clwwlkccatlem  30491  clwlkclwwlklem2a4  30499  clwlkclwwlk  30504  clwwisshclwwslem  30516  clwwlkinwwlk  30542  clwwlkel  30548  clwwlkf  30549  clwwlkext2edg  30558  wwlksext2clwwlk  30559  wwlksubclwwlk  30560  clwwnisshclwwsn  30561  eleclclwwlknlem2  30563  erclwwlknsym  30572  erclwwlkntr  30573  umgrhashecclwwlk  30580  clwwlkvbij  30615  eupth2lem3lem3  30742  eupth2lem3lem4  30743  eupth2lem3lem6  30745  eupth2lemb  30749  eucrct2eupth  30757  fusgreg2wsplem  30845  2clwwlklem  30855  2clwwlk2clwwlklem  30858  2clwwlkel  30861  2clwwlk2clwwlk  30862  extwwlkfabel  30865  clwwlknonclwlknonf1o  30874  dlwwlknondlwlknonf1olem1  30876  numclwwlk2lem1  30888  numclwlk2lem2f  30889  numclwlk2lem2f1o  30891  ex-res  30953  isssp  31237  sspn  31249  islno  31266  isblo  31295  nmlno0  31308  ishmo  31324  dipdir  31355  dipass  31358  ubthlem1  31383  ubthlem2  31384  htthlem  31430  htth  31431  ocel  31794  ocnel  31811  shsel  31827  shsel2  31835  shmodsi  31902  pjhtheu  31907  pjeq  31912  axpjpj  31933  pjoc2  31952  elspani  32056  h1de2ctlem  32068  elspansn  32079  elspansn2  32080  elnlfn  32441  eleigvec  32470  riesz3i  32575  cbviunf  33061  iuneq12daf  33062  iunrdx  33069  iunrnmptss  33070  cbvdisjf  33076  disjorf  33084  disjabrex  33087  disjabrexf  33088  iundisjf  33094  disjrdx  33096  fresunsn  33130  2ndresdju  33154  abfmpunirn  33157  abfmpeld  33159  abfmpel  33160  fmptcof2  33162  acunirnmpt2  33165  acunirnmpt2f  33166  aciunf1lem  33167  suppss3  33226  fpwrelmap  33236  xrofsup  33270  iundisjfi  33299  eliccioo  33408  s3f1  33422  ccatws1f1o  33425  ismnt  33455  mgcoval  33458  gsummpt2co  33520  gsumpart  33535  gsumhashmul  33539  gsummulsubdishift1  33540  xrge0tsmsbi  33546  gsumwrd2dccatlem  33549  gsumwrd2dccat  33550  cycpmco2  33605  cyc3co2  33612  isfxp  33640  cntrval2  33643  inftmrel  33652  isinftm  33653  isslmd  33674  urpropd  33702  elrgspn  33718  erlval  33730  rlocval  33731  rloccring  33743  rloc1r  33745  rlocisunit  33748  domnprodeq0  33751  domnpropd  33752  fracfld  33781  resv1r  33811  ellspds  33835  ellpi  33839  lbslsp  33843  rhmimaidl  33893  ismxidl  33898  crngmxidl  33905  drng0mxidl  33911  opprqus0g  33925  qsfld  33933  isrprm  33960  rsprprmprmidlb  33966  ressply1evls1  34008  ply1mulrtss  34025  ply1coedeg  34032  psrmonmul  34093  dimpropd  34152  lbslsat  34159  extdg1id  34209  fldextrspunlsplem  34216  fldextrspunlsp  34217  elirng  34229  ply1annidllem  34244  constrsuc  34281  constrconj  34288  constrllcllem  34295  constrlccllem  34296  constrcccllem  34297  nn0constr  34304  smatrcl  34339  smatcl  34345  ist0cld  34376  txomap  34377  locfinreflem  34383  zarclsiin  34414  zart0  34422  rhmpreimacnlem  34427  metidval  34433  cnre2csqima  34454  ordtrest2NEW  34466  fmcncfil  34474  fsumcvg4  34493  ofcfval  34641  measvuni  34758  meascnbl  34763  faeval  34790  ismbfm  34795  elunirnmbfm  34796  imambfm  34806  elcarsg  34849  itgeq12dv  34870  issibf  34877  eulerpartlems  34904  eulerpartlemgc  34906  eulerpartlemgvv  34920  eulerpartlemgu  34921  eulerpart  34926  rrvmbfm  34986  elorvc  35004  elorrvc  35008  dstfrvunirn  35019  ballotlemfc0  35037  ballotlemfcc  35038  ballotlemsima  35060  ballotlemrv  35064  fzssfzo  35083  signstfvn  35110  signstfvneq0  35113  signstres  35116  repr0  35152  reprinrn  35159  reprdifc  35168  hgt750lemg  35195  hgt750lemb  35197  istrkg2d  35207  axtgupdim2ALTV  35209  afsval  35215  brafs  35216  bnj945  35316  bnj1400  35377  bnj18eq1  35469  bnj916  35475  bnj1014  35503  bnj1015  35504  bnj1110  35524  bnj1417  35583  rankval2b  35639  r1filimi  35644  r1ssel  35648  acnum  35671  onvf1odlem3  35785  vonf1wev  35788  vonf1owevOLD  35790  vonf1osev  35792  cplgredgex  35802  subfacp1lem2b  35843  subfacp1lem4  35845  subfacp1lem5  35846  subfacp1lem6  35847  ptpconn  35895  cvmscbv  35920  iscvm  35921  cvmsi  35927  cvmsval  35928  cvmliftmolem1  35943  cvmlift2lem12  35976  cvmlift2lem13  35977  cvmlift3lem7  35987  snmlval  35993  satfv1  36025  satfvsucsuc  36027  satfrnmapom  36032  satf0op  36039  satf0n0  36040  sat1el2xp  36041  fmlafvel  36047  isfmlasuc  36050  fmlaomn0  36052  gonan0  36054  goaln0  36055  gonar  36057  goalr  36059  satffunlem1lem2  36065  satffunlem2lem2  36068  satfv0fvfmla0  36075  satef  36078  satefvfmla0  36080  sategoelfvb  36081  satfv1fvfmla1  36085  mrsubfval  36170  mrsubvrs  36184  mclsrcl  36223  mclsval  36225  mppsval  36234  mclsppslem  36245  opelco3  36437  wsuclem  36485  funtransport  36694  fvtransport  36695  brcolinear  36722  colineardim1  36724  funray  36803  fvray  36804  funline  36805  fvline  36807  lineelsb2  36811  fwddifval  36825  fwddifnval  36826  rankeq1o  36830  nmulprop  36837  nmulr0  36842  nmuladdel  36859  ltnmul  36863  ltnadd  36865  rmoeqbidv  36900  disjeq12dv  36902  ixpeq12dv  36903  prodeq12sdv  36905  itgeq12sdv  36906  cbvralvw2  36913  cbvrexvw2  36914  cbvrmovw2  36915  cbvreuvw2  36916  cbvcsbvw2  36918  cbviunvw2  36919  cbviinvw2  36920  cbvmptvw2  36921  cbvdisjvw2  36922  cbvmpo1vw2  36930  cbvmpo2vw2  36931  cbvsbcdavw  36944  cbvcsbdavw  36946  cbvcsbdavw2  36947  cbviundavw  36949  cbviindavw  36950  cbvdisjdavw  36955  cbvrabdavw2  36972  cbviundavw2  36973  cbviindavw2  36974  cbvmptdavw2  36975  cbvdisjdavw2  36976  cbvriotadavw2  36977  cbvmpo1davw2  36979  cbvmpo2davw2  36980  cbvsumdavw2  36982  neibastop2lem  37046  neibastop3  37048  eltail  37060  ttctr  37179  dfttc2g  37192  mh-infprim2bi  37233  bj-projeq  37803  bj-projval  37807  bj-restsn  37899  opelopabbv  37960  brabd0  37964  bj-eldiag  37993  bj-eldiag2  37994  mptsnunlem  38157  dissneqlem  38159  iooelexlt  38181  relowlssretop  38182  rdgellim  38195  exrecfnlem  38198  finxpeq1  38205  finxpreclem6  38215  pibp21  38234  curunc  38421  unccur  38422  fin2so  38426  lindsadd  38432  ptrest  38433  ptrecube  38434  poimirlem2  38436  poimirlem8  38442  poimirlem17  38451  poimirlem18  38452  poimirlem20  38454  poimirlem21  38455  poimirlem22  38456  poimirlem24  38458  poimirlem26  38460  poimirlem29  38463  heicant  38469  mblfinlem1  38471  mblfinlem2  38472  volsupnfl  38479  itg2addnclem  38485  itg2gt0cn  38489  indexdom  38549  incsequz  38563  istotbnd  38584  istotbnd3  38586  0totbnd  38588  sstotbnd  38590  sstotbnd3  38591  isbnd  38595  prdstotbnd  38609  cntotbnd  38611  isismty  38616  heibor1lem  38624  heiborlem2  38627  heiborlem3  38628  heibor  38636  isass  38661  exidcl  38691  exidreslem  38692  elghomlem2OLD  38701  rngoidmlem  38751  rngo1cl  38754  divrngcl  38772  isdrngo2  38773  isrngohom  38780  isrngoiso  38793  isriscg  38799  iscom2  38810  iscringd  38813  isidl  38829  ispridl  38849  ismaxidl  38855  ac6s6  38985  dmecd  39123  dfpre4  39293  releldmqs  39556  releldmqscoss  39558  erimeq2  39576  qmapeldisjsim  39673  eldisjlem19  39726  membpartlem19  39727  prter3  39820  islshp  39917  islsat  39929  lcvfbr  39958  islfl  39998  ellkr  40027  islshpkrN  40058  ldual1dim  40104  isopos  40118  cmtfvalN  40148  cvrfval  40206  isat  40224  islln  40444  islpln  40468  islvol  40511  isline  40677  ispointN  40680  ispsubsp  40683  elpmap  40696  elpmapat  40702  elpadd  40737  paddclN  40780  elpclN  40830  elpcliN  40831  pclfinN  40838  pclcmpatN  40839  ispsubclN  40875  iswatN  40932  islhp  40934  islaut  41021  ispautN  41037  isldil  41048  isltrn  41057  isdilN  41092  istrnN  41095  istendo  41698  dvhb1dimN  41924  erng1lem  41925  erngdvlem4-rN  41937  diaelval  41971  diaeldm  41974  dia1dimid  42001  cdlemm10N  42056  dibopelvalN  42081  dibopelval2  42083  dibelval3  42085  dibelval1st  42087  dibelval2nd  42090  dibeldmN  42096  dibvalrel  42101  dibglbN  42104  dicffval  42112  dicfval  42113  dicopelval  42115  dicelvalN  42116  dicelval3  42118  dicvalrelN  42123  dicelval1sta  42125  diclspsn  42132  dihopelvalbN  42176  dihopelvalcqat  42184  dihopelvalcpre  42186  dihvalrel  42217  dih1  42224  dihmeetlem4preN  42244  dihmeetlem13N  42257  dih1dimatlem  42267  dochnel2  42330  dihjatcclem4  42359  dvh2dim  42383  dvh3dim  42384  dvh4dimN  42385  dochfln0  42415  lpolsetN  42420  islpolN  42421  lcfrvalsnN  42479  lcfrlem21  42501  lcfrlem27  42507  lcfrlem37  42517  lcfr  42523  lcdlss  42557  mapdcv  42598  hdmap1fval  42734  hdmapffval  42764  hdmapfval  42765  hdmapval  42766  hgmapffval  42823  hgmapfval  42824  hdmapellkr  42852  hlhilhillem  42898  fzsplitnd  42913  isprimroot  43024  primrootsunit1  43028  primrootscoprmpow  43030  primrootscoprbij  43033  aks6d1c1p2  43040  aks6d1c1p3  43041  aks6d1c1p4  43042  aks6d1c1p5  43043  aks6d1c1p6  43045  aks6d1c1  43047  evl1gprodd  43048  sticksstones11  43087  sticksstones12a  43088  rhmqusspan  43116  grpods  43125  fzosumm1  43182  frlmfielbas  43453  frlmsnic  43487  psrmnd  43490  isnacs  43614  mrefg2  43617  elmzpcl  43636  mzpcompact2  43662  eldiophb  43667  elpell1qr  43753  elpell14qr  43755  elpell1234qr  43757  pw2f1ocnv  43943  pw2f1o2val2  43946  aomclem4  43963  aomclem6  43965  islssfg2  43977  imasgim  44006  lnr2i  44022  elmnc  44042  rngunsnply  44075  onexomgt  44147  onexlimgt  44149  onexoegt  44150  oaordnr  44202  omnord1  44211  oenord1  44222  cantnfresb  44230  tfsconcatun  44243  tfsconcat0i  44251  ofoaf  44261  naddcnff  44268  naddcnffo  44270  naddcnfcom  44272  naddcnfid1  44273  naddcnfid2  44274  naddcnfass  44275  naddwordnexlem4  44307  fiinfi  44478  sqrtcvallem1  44536  elintima  44558  eliunov2  44584  ov2ssiunov2  44605  brtrclfv2  44632  rfovcnvf1od  44909  rfovcnvfvd  44912  fsovrfovd  44914  fsovfvd  44915  fsovcnvlem  44918  ntrclsfv1  44960  ntrclselnel1  44962  ntrclsneine0lem  44969  ntrneifv1  44984  ntrneifv2  44985  ntrneiel  44986  gneispace2  45037  gneispacess2  45051  extoimad  45069  mnringelbased  45120  dvconstbi  45223  bccbc  45234  wfac8prim  45890  permaxrep  45894  permac8prim  45902  eliin2f  46001  iineq12dv  46003  rabbida2  46029  disjinfi  46089  unirnmap  46103  elmptima  46152  iuneqfzuzlem  46229  iooiinioc  46451  fsumiunss  46470  fsumsupp0  46473  lptre2pt  46533  icccncfext  46780  cncfiooicclem1  46786  dvnprodlem2  46840  stoweidlem27  46920  stoweidlem29  46922  stoweidlem31  46924  stoweidlem34  46927  stoweidlem48  46941  stoweidlem59  46952  dirkercncflem2  46997  dirkercncflem4  46999  fourierdlem2  47002  fourierdlem3  47003  fourierdlem25  47025  fourierdlem32  47032  fourierdlem33  47033  fourierdlem41  47041  fourierdlem48  47047  fourierdlem49  47048  fourierdlem62  47061  fourierdlem70  47069  fourierdlem80  47079  fourierdlem92  47091  fourierdlem93  47092  fourierdlem101  47100  etransclem37  47164  sge0val  47259  sge0f1o  47275  sge0iunmptlemre  47308  sge0iunmpt  47311  iundjiun  47353  caragenel  47388  ovncvrrp  47457  ovnsubaddlem1  47463  ovnsubadd  47465  hoidmvlelem2  47489  hoidmvlelem3  47490  hoidmvlelem4  47491  hoidmvle  47493  ovncvr2  47504  hspdifhsp  47509  hoiqssbl  47518  hspmbllem2  47520  hspmbl  47522  opnvonmbllem1  47525  isvonmbl  47531  ovnovollem1  47549  issmflem  47620  smflimlem3  47666  smflimlem4  47667  smflim  47670  smfmullem2  47685  smflimmpt  47703  smfsuplem1  47704  smflimsuplem1  47713  smflimsuplem3  47715  smflimsuplem4  47716  smflimsuplem7  47719  smflimsup  47721  chnsubseq  47773  tmachlem-agreeprod  47830  tmachlem-tpopen  47834  tmachlem-agreesn  47840  fcores  48020  fcoresf1  48022  afvelrnb  48116  afvelrnb0  48117  afv2co2  48210  el1fzopredsuc  48279  muldvdsfacm1  48340  iccpart  48381  iccpartgtprec  48385  iccpartiltu  48387  iccpartigtl  48388  iccpartltu  48390  iccpartgtl  48391  iccpartgt  48392  iccpartleu  48393  iccpartgel  48394  iccelpart  48398  iccpartiun  48399  icceuelpart  48401  fargshiftfv  48404  fargshiftfo  48407  sprel  48449  prprelb  48481  prprelprb  48482  nprmdvdsfacm1lem4  48591  fpprel  48709  sbgoldbo  48768  wtgoldbnnsum4prm  48783  bgoldbnnsum3prm  48785  bgoldbtbndlem3  48788  bgoldbtbnd  48790  clnbgrval  48803  elclnbgrelnbgr  48806  clnbgrel  48809  clnbupgrel  48815  vopnbgrel  48835  isubgredg  48847  upgrimwlklem3  48880  upgrimwlklem5  48882  upgrimpths  48890  grtriprop  48922  isgrtri  48924  grtriclwlk3  48926  stgredgel  48938  gpgvtxel  49028  gpgiedgdmel  49030  gpgedgel  49031  opgpgvtx  49036  gpg5nbgrvtx13starlem1  49052  gpg5nbgrvtx13starlem2  49053  gpg5nbgrvtx13starlem3  49054  gpg3kgrtriex  49070  grlimedgnedg  49112  upwlksfval  49116  isupwlk  49117  intop  49183  isclintop  49187  assintop  49189  isassintop  49190  assintopcllaw  49192  uzlidlring  49215  elrngchomALTV  49249  rngccatidALTV  49252  rngcsectALTV  49255  rngcisoALTV  49257  rhmsubcALTVlem3  49263  rhmsubcALTVlem4  49264  funcringcsetcALTV2lem7  49276  funcringcsetcALTV2lem9  49278  elringchomALTV  49283  ringccatidALTV  49286  ringcsectALTV  49289  ringcisoALTV  49291  ringcbasbasALTV  49292  funcringcsetclem7ALTV  49299  funcringcsetclem9ALTV  49301  srhmsubcALTV  49305  smprngprmrng  49319  cbvmpox2  49331  ply1sclrmsm  49379  dmatALTbasel  49397  lcoval  49407  lindslinindsimp1  49452  lindslinindsimp2  49458  lmod1  49487  elbigo  49546  elbigo2  49547  elbigolo1  49552  dig2nn0ld  49599  naryfvalel  49625  rrxlines  49728  rrxlinesc  49730  rrxlinec  49731  eenglngeehlnm  49734  elrrx2linest2  49740  rrxsphere  49743  itsclc0  49766  itsclc0b  49767  itsclinecirc0  49768  itsclinecirc0b  49769  itscnhlinecirc02p  49780  brab2dd  49821  f1omo  49884  f1omoOLD  49885  lubeldm2d  49949  glbeldm2d  49950  catprs  50002  sectpropdlem  50027  nelsubc3lem  50061  initc  50082  imaid  50145  upfval  50167  upfval2  50168  upfval3  50169  uppropd  50172  oppcinito  50226  oppctermo  50227  oppczeroo  50228  initopropd  50234  termopropd  50235  isthinc  50410  isthincd2lem1  50416  thincmoALT  50420  thincmod  50421  isthincd  50427  thincpropd  50433  indcthing  50451  discthing  50452  prsthinc  50455  termcterm  50504  termc2  50509  isinito4  50538  2arwcatlem1  50586  setc1onsubc  50593  cnelsubclem  50594  ranval3  50622  lmdfval2  50646  cmdfval2  50647  termolmd  50661  elsetrecslem  50690