Theorem eleq2d 2849

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

Hypothesis

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

Assertion

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

Proof of Theorem eleq2d

Dummy variable 𝑥 is distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  eleq2  2852  eleq12d  2857  eleqtrd  2865  neleqtrd  2885  eqabrd  2904  raleqbidv  3338  rexeqbidv  3339  reueqbidv  3405  rabeqbidva  3432  elabd2  3629  sbcbid  3798  sbcbi2  3802  csbeq2d  3859  csbeq2dv  3860  cbvcsbw  3863  cbvcsb  3864  cbvcsbv  3865  csbie  3888  csbied  3889  csbie2g  3893  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  sbcel12  4376  sbcel1g  4381  sbcel2  4383  prel12g  4829  eliuni  4962  iuneqconst  4968  iuneq12df  4983  iuneq12d  4986  cbviun  4999  cbviin  5000  cbviung  5001  cbviing  5002  cbviunv  5003  cbviinv  5004  iinxsng  5054  iinxprg  5055  iunxsng  5056  iunxsngf  5058  cbvdisj  5086  cbvdisjv  5087  disjor  5091  disjiund  5100  mpteq12da  5194  mpteq12f  5196  mpteq12dva  5197  axpweq  5321  rabxfrd  5388  brab2d  5522  rbropapd  5547  opeliunxp  5728  opeliun2xp  5729  opeliunxp2  5824  iunxpf  5834  elimampt  6045  elrelimasn  6088  elimasni  6093  xpdifid  6165  xpdifcnvepel  6166  imadifssranOLD  6203  ressn  6286  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  7095  fmptco  7125  fnelfp  7173  fnelnfp  7175  tpres  7199  fnprb  7206  fntpb  7207  funfvima3  7234  eluniima  7248  dff13  7252  f1ounsn  7270  f1eqcocnv  7299  isoini  7336  riotaeqdv  7368  mpoeq123dva  7484  cbvmpox  7503  elimampo  7547  ovelrn  7586  elovmpod  7654  elovmpo  7655  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  elovmpt3rab1  7670  fiun  7936  f1iun  7937  zfrep6OLD  7948  fmpox  8060  el2mpocsbcl  8076  el2mpocl  8077  bropopvvv  8081  bropfvvvv  8083  xpord2indlem  8139  xpord3inddlem  8146  elsuppfng  8161  elsuppfn  8162  suppfnss  8181  opeliunxp2f  8202  mpoxopn0yelv  8205  mpoxopovel  8212  rntpos  8231  mpocurryd  8261  fpr2  8297  wfr2  8320  onoviun  8326  smoel  8343  smoiso  8345  smoel2  8346  smo11  8347  tfrlem9  8368  oalimcl  8541  oaass  8542  omordi  8547  omordlim  8558  omlimcl  8559  odi  8560  omeulem1  8563  omeulem2  8564  oen0  8568  oeordi  8569  oeordsuc  8576  oelimcl  8582  oeeulem  8583  oeeui  8584  nnmordi  8613  oaabs2  8631  omabs  8633  omsmolem  8639  ereldm  8744  iiner  8783  elmapg  8832  elpmg  8836  elixpsn  8931  ixpsnf1o  8932  boxriin  8934  omxpenlem  9062  pw2f1olem  9065  phplem2  9185  php3  9189  infn0  9258  elfi  9369  dffi3  9387  marypha2lem2  9392  ordiso2  9473  wemapsolem  9508  elharval  9519  inf3lemd  9592  inf3lem1  9593  inf3lem2  9594  inf3lem3  9595  cantnfs  9631  cantnfp1lem3  9645  cantnflem1b  9651  cantnflem1  9654  ttrclselem2  9691  trcl  9693  frr2  9728  r1sdom  9742  r1ordg  9746  r1pwss  9752  tz9.12lem3  9757  tz9.12  9758  r1elwf  9764  rankr1ai  9766  rankidb  9768  rankr1bg  9771  rankval2  9786  rankunb  9818  tcrank  9852  acni  10025  acni2  10026  acndom  10031  infpwfien  10042  alephnbtwn  10051  cardaleph  10069  cardinfima  10077  iunfictbso  10094  dfac3  10101  dfac5lem5  10107  dfac5  10108  dfac9  10116  dfac12r  10126  kmlem2  10131  kmlem12  10141  kmlem13  10142  kmlem14  10143  ackbij2lem3  10219  ackbij2  10221  cofsmo  10248  alephsing  10255  fin23lem30  10321  isf32lem9  10340  itunisuc  10398  axcc2lem  10415  axcc3  10417  domtriomlem  10421  axdc2lem  10427  axdc2  10428  axdc3lem2  10430  axdc3lem4  10432  axdc4lem  10434  ac6c4  10460  zorn2lem1  10475  ttukeylem6  10493  pwcfsdom  10563  axregndlem2  10583  axinfndlem1  10585  axacndlem4  10590  axacnd  10592  pwfseqlem1  10638  inar1  10755  inatsk  10758  gruurn  10778  grur1  10800  eltskm  10823  genpelv  10980  eluz1  12861  elixx1  13376  elixx3g  13380  elioo2  13408  elfz1  13535  elfz2  13537  elfzp1  13598  fzpr  13603  fzsuc2  13606  fzrev3  13614  elfzp12  13627  fzm1  13631  elfzo  13685  fz0add1fz1  13760  elfzo0l  13781  elfzom1b  13791  fzosplitsni  13804  elfzr  13806  elfzlmr  13807  zmodidfzo  13929  seqp1  14048  seqf1o  14075  bcval  14336  bcpasc  14353  hashf1lem1  14488  fundmge2nop0  14535  wrdmap  14579  elovmpowrd  14591  ccatfval  14606  elfzelfzccat  14613  ccatlid  14620  ccatass  14622  ccatrn  14623  ccatalpha  14627  swrdfv2  14695  ccatswrd  14702  swrdccat2  14703  pfxfv  14716  pfxeq  14729  ccatpfx  14734  swrdswrd  14738  swrdpfx  14740  pfxpfx  14741  cats1un  14754  swrdccatfn  14757  swrdccatin1  14758  pfxccatin12lem4  14759  pfxccatin12lem1  14761  swrdccatin2  14762  pfxccatin12lem2c  14763  pfxccatin12lem2  14764  swrdccat3blem  14772  swrdccatin1d  14776  swrdccatin2d  14777  pfxccatin12d  14778  revccat  14799  revrev  14800  repswpfx  14818  repswccat  14819  cshwidxmod  14836  2cshw  14846  cshwcshid  14860  cshwcsh2id  14861  cshimadifsn  14862  cshimadifsn0  14863  revco  14867  ccatco  14868  cshco  14869  swrdco  14870  ofccat  15002  shftfn  15106  shftval  15107  limsupgle  15524  ello12  15563  elo12  15574  isercolllem3  15714  sumeq1  15736  fsumsplit  15788  sumsplit  15815  fsum2dlem  15817  fsumcom2  15821  fsumparts  15854  explecnv  15915  pwdif  15918  fprodser  15999  fprodsplit  16016  fprod2dlem  16030  fprodcom2  16034  eftlub  16160  divalgmod  16459  bitsval  16477  bitsp1e  16485  bitsp1o  16486  sadfval  16505  sadcp1  16508  sadval  16509  sadcadd  16511  sadadd2  16513  saddisjlem  16517  sadadd  16520  sadass  16524  smufval  16530  smuval  16534  smuval2  16535  smupvallem  16536  smu01lem  16538  smueqlem  16543  smumul  16546  bezoutlem2  16593  bezoutlem4  16595  algfx  16633  eucalgcvga  16639  reumodprminv  16859  nnnn0modprm0  16861  unbenlem  16963  prmreclem5  16975  vdwapval  17028  vdwapun  17029  vdwnnlem1  17050  vdwnn  17053  ramval  17063  0ram  17075  ramub1lem2  17082  prmgaplem7  17112  prmlem0  17160  elrest  17475  prdsbasmpt  17518  prdsleval  17525  prdsbasmpt2  17530  pwselbasb  17536  imasaddfnlem  17577  imasvscafn  17586  divsfval  17596  ismre  17637  mreunirn  17648  mrisval  17681  ismri  17682  isacs  17702  catidd  17731  iscatd2  17732  ismon  17785  isepi  17792  sectffval  17802  sectfval  17803  dfiso2  17824  cicsym  17856  issubc  17887  catsubcat  17891  isfunc  17916  funcres  17948  funcpropd  17954  ffthiso  17983  isnat  18002  isnat2  18003  fuciso  18030  initoval  18045  termoval  18046  isinito  18048  istermo  18049  iszeroo  18050  isinitoi  18051  istermoi  18052  initoid  18053  termoid  18054  iszeroi  18061  2initoinv  18062  initoeu1  18063  initoeu2  18068  2termoinv  18069  termoeu1  18070  arwhoma  18097  elsetchom  18133  setcmon  18139  setcepi  18140  setciso  18143  catciso  18163  elestrchom  18179  estrcbasbas  18182  funcestrcsetclem7  18197  funcestrcsetclem8  18198  funcestrcsetclem9  18199  fthestrcsetc  18201  fullestrcsetc  18202  equivestrcsetc  18203  setc1strwun  18204  funcsetcestrclem7  18212  funcsetcestrclem8  18213  funcsetcestrclem9  18214  fthsetcestrc  18216  fullsetcestrc  18217  hofcl  18310  hofpropd  18318  yonedalem4c  18328  yonedainv  18332  yonffthlem  18333  lubeldm  18402  glbeldm  18415  joindef  18425  meetdef  18439  poslubdg  18463  acsficl2d  18603  acsmapd  18605  psref  18625  psss  18631  dirge  18654  chnccats1  18676  chnccat  18677  chnrev  18678  mgmpropd  18704  issstrmgm  18706  grpidval  18714  grpidpropd  18715  grpidd  18724  ismgmhm  18749  issubmgm  18755  issgrpd  18783  sgrppropd  18784  ismndd  18809  mndpropd  18812  imasmnd2  18827  imasmnd  18828  xpsmnd0  18831  ismhm  18838  issubm  18856  gsumsgrpccat  18894  elefmndbas2  18928  smndex1mndlem  18966  imasgrp2  19116  imasgrp  19117  issubg  19187  subginv  19194  isnsg  19216  eqg0el  19249  quselbas  19250  isghm  19281  resghm2b  19299  conjnmzb  19318  conjnsg  19319  ghmpropd  19321  isga  19356  elcntz  19387  elcntzsn  19390  cntzrcl  19392  resscntz  19398  symgextf1  19486  gsmsymgreqlem2  19496  f1otrspeq  19512  pmtrfrn  19523  pmtrdifellem3  19543  pmtrdifellem4  19544  psgnunilem1  19558  psgnunilem5  19559  psgnunilem2  19560  psgnunilem3  19561  psgneldm2  19569  psgnfitr  19582  psgnsn  19585  gexdvds  19649  gex1  19656  isslw  19673  sylow3lem2  19693  lsmelvalx  19705  pj1ghm  19768  efgtlen  19791  efgsfo  19804  efgredlemc  19810  frgp0  19825  frgpmhm  19830  qusabl  19930  frgpnabllem1  19938  imasabl  19941  cycsubmcmn  19954  0cyg  19958  cycsubgcyg  19966  gsumval3  19972  gsumcllem  19973  gsumzaddlem  19986  gsumzsplit  19992  gsummptfzcl  20034  eldprd  20071  dprdcntz2  20105  dprd2d2  20111  dmdprdsplit2lem  20112  dmdprdsplit2  20113  dprdsplit  20115  ablfac2  20156  isrngd  20246  rngpropd  20247  imasrng  20250  qusrng  20253  ringurd  20262  isringd  20370  imasring  20408  xpsring1d  20411  dvdsrval  20439  isunit  20451  dvdsrpropd  20494  isirred  20497  isrnghm  20519  isrngim  20523  c0ghm  20539  c0snghm  20542  isrhm0  20554  isrhm  20557  isrim0  20561  crngrhmfo  20574  islring  20639  issubrng  20646  opprsubrng  20658  issubrg  20670  opprsubrg  20692  resrhm2b  20701  rhmpropd  20708  rnghmresel  20719  elrngchom  20723  rnghmsubcsetclem1  20730  rnghmsubcsetclem2  20731  rngcid  20734  rngcsect  20735  rngciso  20737  funcrngcsetcALT  20740  zrinitorngc  20741  zrtermorngc  20742  rhmresel  20748  elringchom  20752  rhmsubcsetclem1  20759  rhmsubcsetclem2  20760  ringcid  20763  rhmsscrnghm  20764  rhmsubcrngclem1  20765  rhmsubcrngclem2  20766  ringcsect  20769  ringciso  20771  ringcbasbas  20772  zrtermoringc  20774  srhmsubc  20779  rhmsubclem3  20786  rhmsubclem4  20787  drngunit  20832  isdrng4  20839  isdrngd  20868  isdrngdOLD  20870  issdrg  20891  sdrgunit  20899  isabv  20914  issrngd  20958  islmod  20985  lmodprop2d  21045  islss  21055  islssd  21056  lssats2  21121  ellspsn  21124  islmhm  21148  lmhmf1o  21167  lmhmima  21168  lmhmpreima  21169  reslmhm  21173  pwssplit3  21182  lmhmpropd  21194  islbs  21197  lspprel  21215  lspfixed  21252  lbsacsbs  21280  lbsextlem1  21282  lbsextlem2  21283  lbsextlem3  21284  lbsextlem4  21285  ixpsnbasval  21329  isridlrng  21344  rnglidlmmgm  21379  isridl  21391  quscrng  21423  rngqiprngimfolem  21430  rngqiprngimf1lem  21434  rngqiprngimfo  21441  isprmidl  21463  qsidomlem1  21480  qsidomlem2  21481  islpidl  21493  lidldvgen  21502  irinitoringc  21629  pzriprnglem13  21643  pzriprnglem14  21644  zrhrhmb  21660  znf1o  21701  frgpcyg  21723  psgnevpmb  21737  isphld  21804  phlssphl  21809  elocv  21818  iscss  21833  isobs  21870  obs2ss  21879  dsmmfi  21888  dsmmelbas  21889  dsmmlss  21894  frlmelbas  21906  frlmlbs  21947  frlmup1  21948  ellspd  21952  islinds  21959  islindf2  21964  f1lindf  21972  islindf4  21988  assamulgscmlem2  22050  psrgrp  22106  mplsubglem  22148  mpllsslem  22149  mplmonmul  22187  subrgascl  22217  subrgasclcl  22218  mpfind  22266  ismhp  22303  gsumply1subr  22393  lply1binomsc  22471  matbas2d  22580  matecl  22582  matvscl  22588  mat1  22604  mat0dim0  22624  mat0dimid  22625  mat0dimscm  22626  mat1dimelbas  22628  dmatel  22650  scmatel  22662  scmateALT  22669  scmataddcl  22673  scmatsubcl  22674  smatvscl  22681  scmatghm  22690  mat1scmat  22696  mdetunilem7  22775  mdetunilem9  22777  smadiadetr  22832  cramerimplem2  22841  cramer0  22847  pmatcoe1fsupp  22858  cpmatpmat  22867  cpmatel  22868  cpmatacl  22873  cpmatinvcl  22874  mat2pmatghm  22887  mat2pmatmul  22888  decpmatmullem  22928  pmatcollpwlem  22937  pmatcollpw3fi1lem1  22943  pmatcollpwscmatlem1  22946  monmat2matmon  22981  chfacfscmul0  23015  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  cayhamlem1  23023  cpmadugsumlemB  23031  cpmadugsumlemC  23032  cpmadugsumlemF  23033  cayhamlem2  23041  istopon  23069  eltg  23114  eltg2  23115  eltop  23131  eltop2  23132  eltop3  23133  pptbas  23165  iscld  23184  neiss2  23258  isnei  23260  neiptopnei  23289  neiptopreu  23290  lpfval  23295  lpval  23296  islp  23297  maxlp  23304  islpi  23306  neitr  23337  restlp  23340  ordtbas2  23348  ordtrest2  23361  lmfval  23389  cnfval  23390  iscn  23392  iscnp  23394  tgcn  23409  tgcnp  23410  lmbrf  23417  cnpresti  23445  ist1  23478  ist1-2  23504  cnt1  23507  haust1  23509  cmpfi  23565  cmpfii  23566  1stcfb  23602  2ndc1stc  23608  1stcrest  23610  2ndcdisj  23613  1stcelcls  23618  nllyi  23632  subislly  23638  islocfin  23674  lfinpfin  23681  locfindis  23687  locfincf  23688  comppfsc  23689  kgenval  23692  elkgen  23693  kgencn2  23714  txbas  23724  eltx  23725  ptval  23727  ptpjpre1  23728  ptopn2  23741  ptpjopn  23769  ptclsg  23772  xkoccn  23776  txdis  23789  txdis1cn  23792  ptrescn  23796  hausdiag  23802  hauseqlcld  23803  txhaus  23804  xkohaus  23810  elqtop  23854  qtopeu  23873  kqcldsat  23890  hmeofval  23915  ptuncnv  23964  ptunhmeo  23965  elmptrab  23984  fbdmn0  23991  elfg  24028  elfilss  24033  filunirn  24039  fixufil  24079  elfm  24104  rnelfmlem  24109  rnelfm  24110  fmfnfmlem4  24114  elflim2  24121  flimtopon  24127  elflim  24128  hausflim  24138  flimcls  24142  flfnei  24148  isflf  24150  hausflf  24154  cnpflf  24158  cnflf  24159  txflf  24163  isfcls  24166  fclstopon  24169  isfcls2  24170  fclssscls  24175  fclsnei  24176  fclsfnflim  24184  flimfnfcls  24185  isfcf  24191  fcfelbas  24193  cnpfcf  24198  cnfcf  24199  flfcntr  24200  alexsublem  24201  alexsubALTlem3  24206  cnextfun  24221  cnextfvval  24222  cnextf  24223  cnextcn  24224  tmdgsum2  24253  tgpconncomp  24270  ghmcnp  24272  qustgplem  24278  eltsms  24290  haustsms  24293  tsmsgsum  24296  tsmssubm  24300  tsmssplit  24309  isust  24361  ustbas  24384  elutop  24390  ustuqtoplem  24396  ustuqtop4  24401  ustuqtop  24403  utopsnneiplem  24404  utopsnneip  24405  utopsnnei  24406  isusp  24418  isucn  24434  ucncn  24441  iscfilu  24444  neipcfilu  24452  iscusp  24455  cnextucn  24459  ispsmet  24461  ismet  24480  isxmet  24481  elblps  24544  elbl  24545  elmopn  24599  prdsbl  24648  neibl  24658  met1stc  24678  metrest  24681  prdsxmslem2  24686  txmetcnp  24704  txmetcn  24705  metustsym  24712  cfilucfil2  24718  elbl4  24720  metuel  24721  psmetutop  24724  restmetu  24727  metucn  24728  tngngp  24811  isnmhm  24903  zcld  24971  metnrmlem1a  25016  elcncf  25048  cncfcnvcn  25084  cnheibor  25114  lebnumlem1  25120  ishtpy  25131  isphtpy  25140  om1elbas  25191  elpi1  25204  pi1xfr  25214  pi1coghm  25220  tcphcph  25396  lmmbrf  25421  iscfil  25424  iscau  25435  iscauf  25439  caucfil  25442  iscmet  25443  cmetcaulem  25447  iscmet3lem1  25450  iscmet3lem2  25451  iscmet3  25452  bcthlem1  25483  cmsss  25510  cmetcusp1  25512  cmetcusp  25513  cmscsscms  25532  rrxcph  25551  minveclem3b  25587  ovolfioo  25626  ovolficc  25627  ovolctb  25649  ovoliunnul  25666  ovolshftlem1  25668  sca2rab  25671  ovolscalem1  25672  ovolicc2lem1  25676  ovolicc2lem2  25677  ovolicc2lem4  25679  ovolicc2lem5  25680  iundisj  25707  iunmbl2  25716  uniioombllem3  25744  vitalilem2  25768  vitalilem3  25769  mbfss  25805  i1faddlem  25852  i1fmullem  25853  mbfi1fseqlem2  25875  mbfi1fseqlem4  25877  mbfi1fseq  25880  itg2splitlem  25907  itg2split  25908  itg2monolem1  25909  itg2gt0  25919  isibl  25924  iblss2  25965  itgss3  25974  itgsplit  25995  ellimc  26032  limcmo  26041  cnlimc  26047  limciun  26053  limcun  26054  eldv  26057  dvbsss  26061  dvreslem  26068  elcpn  26093  dvaddf  26101  dvmulf  26102  dvcof  26107  rolle  26149  dvlip2  26154  dvivthlem1  26167  lhop1  26173  lhop2  26174  ftc1cn  26202  fta1glem2  26326  plyco0  26349  elply  26352  ply1termlem  26360  eltayl  26523  tayl0  26525  taylplem1  26526  taylplem2  26527  dvtaylp  26533  taylthlem1  26536  taylthlem2  26537  abelth  26604  cxpcn3  26913  rlimcnp  27130  fsumharmonic  27176  dchrelbas  27400  pntrsumbnd2  27731  ostth2lem2  27798  nolesgn2ores  27836  nogesgn1ores  27838  nosupprefixmo  27864  noinfprefixmo  27865  nosupcbv  27866  nosupdm  27868  nosupfv  27870  nosupres  27871  nosupbnd1lem1  27872  nosupbnd1lem3  27874  nosupbnd1lem5  27876  nosupbnd2lem1  27879  noinfcbv  27881  noinfdm  27883  noinffv  27885  noinfres  27886  noinfbnd1lem1  27887  noinfbnd1lem3  27889  noinfbnd1lem5  27891  noinfbnd2lem1  27894  elmade  28050  elold  28052  sltsleft  28053  sltsright  28054  oldlim  28080  madebday  28093  newbday  28095  ltslpss  28101  bdayiun  28108  cofcutr  28117  cofcutrtime  28120  lrrecval  28132  lrrecval2  28133  addsval  28155  precsexlem9  28408  precsexlem11  28410  ltonold  28454  onnolt  28459  onlts  28460  noseqrdgfn  28499  istrkgb  28724  istrkgcb  28725  istrkge  28726  istrkgl  28727  istrkgld  28728  axtgsegcon  28733  axtg5seg  28734  axtgbtwnid  28735  axtgpasch  28736  axtgupdim2  28740  axtgeucl  28741  tgdim01  28776  iscgrg  28781  isismt  28803  tglnunirn  28817  tglngval  28820  tgellng  28822  legval  28853  legov  28854  legov2  28855  ishlg2  28871  ishlg  28874  mirreu3  28931  mirval  28932  mirfv  28933  mircgr  28934  mirbtwn  28935  ismir  28936  mireq  28942  symquadlem  28966  israg  28977  perpln1  28990  perpln2  28991  isperp  28992  islnopp  29020  outpasch  29037  ishpg  29041  tgplnfn  29057  plngval  29059  isplng  29060  elplng  29062  elplngid  29064  lnincplng  29066  plngcplem  29067  plngcp  29068  plngrot  29072  nhpmirhp  29080  lnperpexs  29114  iscgra  29120  dfcgra2  29141  ragraghl  29149  isinag  29155  isleag  29164  iseqlg  29184  brprlng  29188  prlnghpg  29196  prlngmo  29204  f1otrgitv  29219  f1otrg  29220  f1otrge  29221  ttgval  29224  ttgelitv  29232  elee  29243  brbtwn  29249  brcgr  29250  axlowdimlem16  29307  ebtwntg  29332  elntg2  29335  upgrex  29442  edgupgr  29484  upgredg  29487  edglnl  29493  numedglnl  29494  uhgr2edg  29558  umgr2edg1  29561  usgredg2vlem1  29575  usgredg2vlem2  29576  ushgredgedg  29579  ushgredgedgloop  29581  uhgrspansubgrlem  29640  fusgrfisstep  29679  nbgrval  29686  nbgrel  29690  nbupgrel  29695  nbgr2vtx1edg  29700  nbuhgr2vtx1edgblem  29701  nbuhgr2vtx1edgb  29702  nbusgreledg  29703  usgrnbcnvfv  29715  uvtxval  29737  uvtxel  29738  uvtx01vtx  29747  uvtxusgrel  29753  nbcplgr  29784  cplgr3v  29785  cusgrexi  29793  structtocusgr  29796  vtxdgfval  29817  vtxdg0v  29823  vtxdeqd  29827  vtxdun  29831  1loopgrnb0  29852  1loopgrvd0  29854  1hevtxdg0  29855  1hevtxdg1  29856  1egrvtxdg1  29859  umgr2v2evtxel  29872  umgr2v2enb1  29876  umgr2v2evd2  29877  vtxdginducedm1lem4  29892  vtxdginducedm1  29893  finsumvtxdg2sstep  29899  ewlksfval  29951  isewlk  29952  wksfval  29959  iswlk  29960  uspgr2wlkeq  29995  wlkres  30018  dfpth2  30078  usgr2pthlem  30112  clwlkcompim  30129  uspgrn2crct  30157  wwlks  30184  iswwlksn  30187  wwlknvtx  30194  wlkiswwlks2  30224  wwlksm1edg  30230  wwlksnred  30241  wwlksnext  30242  wwlksnredwwlkn  30244  wwlksnredwwlkn0  30245  wwlksnwwlksnon  30264  wspn0  30273  usgr2wspthons3  30316  rusgrnumwwlkb0  30323  clwwlk  30334  clwwlkccatlem  30340  clwlkclwwlklem2a4  30348  clwlkclwwlk  30353  clwwisshclwwslem  30365  clwwlkinwwlk  30391  clwwlkel  30397  clwwlkf  30398  clwwlkext2edg  30407  wwlksext2clwwlk  30408  wwlksubclwwlk  30409  clwwnisshclwwsn  30410  eleclclwwlknlem2  30412  erclwwlknsym  30421  erclwwlkntr  30422  umgrhashecclwwlk  30429  clwwlkvbij  30464  eupth2lem3lem3  30581  eupth2lem3lem4  30582  eupth2lem3lem6  30584  eupth2lemb  30588  eucrct2eupth  30596  fusgreg2wsplem  30684  2clwwlklem  30694  2clwwlk2clwwlklem  30697  2clwwlkel  30700  2clwwlk2clwwlk  30701  extwwlkfabel  30704  clwwlknonclwlknonf1o  30713  dlwwlknondlwlknonf1olem1  30715  numclwwlk2lem1  30727  numclwlk2lem2f  30728  numclwlk2lem2f1o  30730  ex-res  30792  isssp  31076  sspn  31088  islno  31105  isblo  31134  nmlno0  31147  ishmo  31163  dipdir  31194  dipass  31197  ubthlem1  31222  ubthlem2  31223  htthlem  31269  htth  31270  ocel  31633  ocnel  31650  shsel  31666  shsel2  31674  shmodsi  31741  pjhtheu  31746  pjeq  31751  axpjpj  31772  pjoc2  31791  elspani  31895  h1de2ctlem  31907  elspansn  31918  elspansn2  31919  elnlfn  32280  eleigvec  32309  riesz3i  32414  cbviunf  32900  iuneq12daf  32901  iunrdx  32908  iunrnmptss  32910  cbvdisjf  32916  disjorf  32924  disjabrex  32927  disjabrexf  32928  iundisjf  32934  disjrdx  32936  fresunsn  32970  2ndresdju  32994  abfmpunirn  32997  abfmpeld  32999  abfmpel  33000  fmptcof2  33002  acunirnmpt2  33005  acunirnmpt2f  33006  aciunf1lem  33007  suppss3  33068  fpwrelmap  33078  xrofsup  33112  iundisjfi  33141  eliccioo  33250  s3f1  33267  ccatf1  33269  ccatws1f1o  33271  swrdrn3  33275  ismnt  33303  mgcoval  33306  gsummpt2co  33368  gsumpart  33383  gsumhashmul  33387  gsummulsubdishift1  33388  xrge0tsmsbi  33394  gsumwrd2dccatlem  33397  gsumwrd2dccat  33398  cycpmco2  33453  cyc3co2  33460  isfxp  33488  cntrval2  33491  inftmrel  33500  isinftm  33501  isslmd  33522  urpropd  33550  elrgspn  33566  erlval  33578  rlocval  33579  rloccring  33591  rloc1r  33593  rlocisunit  33596  domnprodeq0  33599  domnpropd  33600  fracfld  33629  resv1r  33659  ellspds  33683  ellpi  33687  lbslsp  33690  rhmimaidl  33740  ismxidl  33745  crngmxidl  33752  drng0mxidl  33758  opprqus0g  33772  qsfld  33780  isrprm  33807  rsprprmprmidlb  33813  ressply1evls1  33855  ply1mulrtss  33872  ply1coedeg  33879  psrmonmul  33940  dimpropd  33999  lbslsat  34006  extdg1id  34056  fldextrspunlsplem  34063  fldextrspunlsp  34064  elirng  34076  ply1annidllem  34091  constrsuc  34128  constrconj  34135  constrllcllem  34142  constrlccllem  34143  constrcccllem  34144  nn0constr  34151  smatrcl  34186  smatcl  34192  ist0cld  34223  txomap  34224  locfinreflem  34230  zarclsiin  34261  zart0  34269  rhmpreimacnlem  34274  metidval  34280  cnre2csqima  34301  ordtrest2NEW  34313  fmcncfil  34321  fsumcvg4  34340  ofcfval  34488  measvuni  34604  meascnbl  34609  faeval  34636  ismbfm  34641  elunirnmbfm  34642  imambfm  34652  elcarsg  34695  itgeq12dv  34716  issibf  34723  eulerpartlems  34750  eulerpartlemgc  34752  eulerpartlemgvv  34766  eulerpartlemgu  34767  eulerpart  34772  rrvmbfm  34832  elorvc  34850  elorrvc  34854  dstfrvunirn  34865  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemsima  34906  ballotlemrv  34910  fzssfzo  34929  signstfvn  34956  signstfvneq0  34959  signstres  34962  repr0  34998  reprinrn  35005  reprdifc  35014  hgt750lemg  35041  hgt750lemb  35043  istrkg2d  35053  axtgupdim2ALTV  35055  afsval  35061  brafs  35062  bnj945  35162  bnj1400  35223  bnj18eq1  35315  bnj916  35321  bnj1014  35349  bnj1015  35350  bnj1110  35370  bnj1417  35429  rankval2b  35492  r1filimi  35497  r1ssel  35501  acnum  35525  onvf1odlem3  35589  vonf1wev  35592  vonf1owevOLD  35594  vonf1osev  35596  revpfxsfxrev  35607  cplgredgex  35613  pfxwlk  35616  revwlk  35617  subfacp1lem2b  35673  subfacp1lem4  35675  subfacp1lem5  35676  subfacp1lem6  35677  ptpconn  35725  cvmscbv  35750  iscvm  35751  cvmsi  35757  cvmsval  35758  cvmliftmolem1  35773  cvmlift2lem12  35806  cvmlift2lem13  35807  cvmlift3lem7  35817  snmlval  35823  satfv1  35855  satfvsucsuc  35857  satfrnmapom  35862  satf0op  35869  satf0n0  35870  sat1el2xp  35871  fmlafvel  35877  isfmlasuc  35880  fmlaomn0  35882  gonan0  35884  goaln0  35885  gonar  35887  goalr  35889  satffunlem1lem2  35895  satffunlem2lem2  35898  satfv0fvfmla0  35905  satef  35908  satefvfmla0  35910  sategoelfvb  35911  satfv1fvfmla1  35915  mrsubfval  36000  mrsubvrs  36014  mclsrcl  36053  mclsval  36055  mppsval  36064  mclsppslem  36075  opelco3  36267  wsuclem  36315  funtransport  36523  fvtransport  36524  brcolinear  36551  colineardim1  36553  funray  36632  fvray  36633  funline  36634  fvline  36636  lineelsb2  36640  fwddifval  36654  fwddifnval  36655  rankelg  36660  rankeq1o  36663  elhf2  36667  0hf  36669  nmulprop  36682  nmulr0  36687  nmuladdel  36704  ltnmul  36708  ltnadd  36710  rmoeqbidv  36745  disjeq12dv  36747  ixpeq12dv  36748  prodeq12sdv  36750  itgeq12sdv  36751  cbvralvw2  36758  cbvrexvw2  36759  cbvrmovw2  36760  cbvreuvw2  36761  cbvcsbvw2  36763  cbviunvw2  36764  cbviinvw2  36765  cbvmptvw2  36766  cbvdisjvw2  36767  cbvmpo1vw2  36775  cbvmpo2vw2  36776  cbvsbcdavw  36789  cbvcsbdavw  36791  cbvcsbdavw2  36792  cbviundavw  36794  cbviindavw  36795  cbvdisjdavw  36800  cbvrabdavw2  36817  cbviundavw2  36818  cbviindavw2  36819  cbvmptdavw2  36820  cbvdisjdavw2  36821  cbvriotadavw2  36822  cbvmpo1davw2  36824  cbvmpo2davw2  36825  cbvsumdavw2  36827  neibastop2lem  36891  neibastop3  36893  eltail  36905  ttctr  37024  dfttc2g  37037  mh-infprim2bi  37078  bj-projeq  37648  bj-projval  37652  bj-restsn  37744  opelopabbv  37807  brabd0  37811  bj-eldiag  37840  bj-eldiag2  37841  mptsnunlem  38004  dissneqlem  38006  iooelexlt  38028  relowlssretop  38029  rdgellim  38042  exrecfnlem  38045  finxpeq1  38052  finxpreclem6  38062  pibp21  38081  curf  38269  uncf  38270  curunc  38273  unccur  38274  fin2so  38278  lindsadd  38284  lindsdom  38285  lindsenlbs  38286  matunitlindflem1  38287  matunitlindflem2  38288  matunitlindf  38289  ptrest  38290  ptrecube  38291  poimirlem2  38293  poimirlem8  38299  poimirlem17  38308  poimirlem18  38309  poimirlem20  38311  poimirlem21  38312  poimirlem22  38313  poimirlem24  38315  poimirlem26  38317  poimirlem29  38320  heicant  38326  mblfinlem1  38328  mblfinlem2  38329  volsupnfl  38336  itg2addnclem  38342  itg2gt0cn  38346  indexdom  38405  incsequz  38419  istotbnd  38440  istotbnd3  38442  0totbnd  38444  sstotbnd  38446  sstotbnd3  38447  isbnd  38451  prdstotbnd  38465  cntotbnd  38467  isismty  38472  heibor1lem  38480  heiborlem2  38483  heiborlem3  38484  heibor  38492  isass  38517  exidcl  38547  exidreslem  38548  elghomlem2OLD  38557  rngoidmlem  38607  rngo1cl  38610  divrngcl  38628  isdrngo2  38629  isrngohom  38636  isrngoiso  38649  isriscg  38655  iscom2  38666  iscringd  38669  isidl  38685  ispridl  38705  ismaxidl  38711  ac6s6  38841  dmecd  38979  dfpre4  39149  releldmqs  39412  releldmqscoss  39414  erimeq2  39432  qmapeldisjsim  39529  eldisjlem19  39582  membpartlem19  39583  prter3  39676  islshp  39773  islsat  39785  lcvfbr  39814  islfl  39854  ellkr  39883  islshpkrN  39914  ldual1dim  39960  isopos  39974  cmtfvalN  40004  cvrfval  40062  isat  40080  islln  40300  islpln  40324  islvol  40367  isline  40533  ispointN  40536  ispsubsp  40539  elpmap  40552  elpmapat  40558  elpadd  40593  paddclN  40636  elpclN  40686  elpcliN  40687  pclfinN  40694  pclcmpatN  40695  ispsubclN  40731  iswatN  40788  islhp  40790  islaut  40877  ispautN  40893  isldil  40904  isltrn  40913  isdilN  40948  istrnN  40951  istendo  41554  dvhb1dimN  41780  erng1lem  41781  erngdvlem4-rN  41793  diaelval  41827  diaeldm  41830  dia1dimid  41857  cdlemm10N  41912  dibopelvalN  41937  dibopelval2  41939  dibelval3  41941  dibelval1st  41943  dibelval2nd  41946  dibeldmN  41952  dibvalrel  41957  dibglbN  41960  dicffval  41968  dicfval  41969  dicopelval  41971  dicelvalN  41972  dicelval3  41974  dicvalrelN  41979  dicelval1sta  41981  diclspsn  41988  dihopelvalbN  42032  dihopelvalcqat  42040  dihopelvalcpre  42042  dihvalrel  42073  dih1  42080  dihmeetlem4preN  42100  dihmeetlem13N  42113  dih1dimatlem  42123  dochnel2  42186  dihjatcclem4  42215  dvh2dim  42239  dvh3dim  42240  dvh4dimN  42241  dochfln0  42271  lpolsetN  42276  islpolN  42277  lcfrvalsnN  42335  lcfrlem21  42357  lcfrlem27  42363  lcfrlem37  42373  lcfr  42379  lcdlss  42413  mapdcv  42454  hdmap1fval  42590  hdmapffval  42620  hdmapfval  42621  hdmapval  42622  hgmapffval  42679  hgmapfval  42680  hdmapellkr  42708  hlhilhillem  42754  fzsplitnd  42769  isprimroot  42880  primrootsunit1  42884  primrootscoprmpow  42886  primrootscoprbij  42889  aks6d1c1p2  42896  aks6d1c1p3  42897  aks6d1c1p4  42898  aks6d1c1p5  42899  aks6d1c1p6  42901  aks6d1c1  42903  evl1gprodd  42904  sticksstones11  42943  sticksstones12a  42944  rhmqusspan  42972  grpods  42981  fzosumm1  43038  frlmfielbas  43294  frlmsnic  43328  psrmnd  43331  isnacs  43455  mrefg2  43458  elmzpcl  43477  mzpcompact2  43503  eldiophb  43508  elpell1qr  43594  elpell14qr  43596  elpell1234qr  43598  pw2f1ocnv  43784  pw2f1o2val2  43787  aomclem4  43804  aomclem6  43806  islssfg2  43818  imasgim  43847  lnr2i  43863  elmnc  43883  rngunsnply  43916  onexomgt  43988  onexlimgt  43990  onexoegt  43991  oaordnr  44043  omnord1  44052  oenord1  44063  cantnfresb  44071  tfsconcatun  44084  tfsconcat0i  44092  ofoaf  44102  naddcnff  44109  naddcnffo  44111  naddcnfcom  44113  naddcnfid1  44114  naddcnfid2  44115  naddcnfass  44116  naddwordnexlem4  44148  fiinfi  44319  sqrtcvallem1  44377  elintima  44399  eliunov2  44425  ov2ssiunov2  44446  brtrclfv2  44473  rfovcnvf1od  44750  rfovcnvfvd  44753  fsovrfovd  44755  fsovfvd  44756  fsovcnvlem  44759  ntrclsfv1  44801  ntrclselnel1  44803  ntrclsneine0lem  44810  ntrneifv1  44825  ntrneifv2  44826  ntrneiel  44827  gneispace2  44878  gneispacess2  44892  extoimad  44910  mnringelbased  44961  dvconstbi  45064  bccbc  45075  wfac8prim  45731  permaxrep  45735  permac8prim  45743  eliin2f  45842  iineq12dv  45844  rabbida2  45870  disjinfi  45930  unirnmap  45944  elmptima  45993  iuneqfzuzlem  46070  iooiinioc  46292  fsumiunss  46311  fsumsupp0  46314  lptre2pt  46374  icccncfext  46621  cncfiooicclem1  46627  dvnprodlem2  46681  stoweidlem27  46761  stoweidlem29  46763  stoweidlem31  46765  stoweidlem34  46768  stoweidlem48  46782  stoweidlem59  46793  dirkercncflem2  46838  dirkercncflem4  46840  fourierdlem2  46843  fourierdlem3  46844  fourierdlem25  46866  fourierdlem32  46873  fourierdlem33  46874  fourierdlem41  46882  fourierdlem48  46888  fourierdlem49  46889  fourierdlem62  46902  fourierdlem70  46910  fourierdlem80  46920  fourierdlem92  46932  fourierdlem93  46933  fourierdlem101  46941  etransclem37  47005  sge0val  47100  sge0f1o  47116  sge0iunmptlemre  47149  sge0iunmpt  47152  iundjiun  47194  caragenel  47229  ovncvrrp  47298  ovnsubaddlem1  47304  ovnsubadd  47306  hoidmvlelem2  47330  hoidmvlelem3  47331  hoidmvlelem4  47332  hoidmvle  47334  ovncvr2  47345  hspdifhsp  47350  hoiqssbl  47359  hspmbllem2  47361  hspmbl  47363  opnvonmbllem1  47366  isvonmbl  47372  ovnovollem1  47390  issmflem  47461  smflimlem3  47507  smflimlem4  47508  smflim  47511  smfmullem2  47526  smflimmpt  47544  smfsuplem1  47545  smflimsuplem1  47554  smflimsuplem3  47556  smflimsuplem4  47557  smflimsuplem7  47560  smflimsup  47562  chnsubseq  47616  fcores  47824  fcoresf1  47826  afvelrnb  47920  afvelrnb0  47921  afv2co2  48014  el1fzopredsuc  48083  muldvdsfacm1  48144  iccpart  48185  iccpartgtprec  48189  iccpartiltu  48191  iccpartigtl  48192  iccpartltu  48194  iccpartgtl  48195  iccpartgt  48196  iccpartleu  48197  iccpartgel  48198  iccelpart  48202  iccpartiun  48203  icceuelpart  48205  fargshiftfv  48208  fargshiftfo  48211  sprel  48253  prprelb  48285  prprelprb  48286  nprmdvdsfacm1lem4  48395  fpprel  48513  sbgoldbo  48572  wtgoldbnnsum4prm  48587  bgoldbnnsum3prm  48589  bgoldbtbndlem3  48592  bgoldbtbnd  48594  clnbgrval  48607  elclnbgrelnbgr  48610  clnbgrel  48613  clnbupgrel  48619  vopnbgrel  48639  isubgredg  48651  upgrimwlklem3  48684  upgrimwlklem5  48686  upgrimpths  48694  grtriprop  48726  isgrtri  48728  grtriclwlk3  48730  stgredgel  48742  gpgvtxel  48832  gpgiedgdmel  48834  gpgedgel  48835  opgpgvtx  48840  gpg5nbgrvtx13starlem1  48856  gpg5nbgrvtx13starlem2  48857  gpg5nbgrvtx13starlem3  48858  gpg3kgrtriex  48874  grlimedgnedg  48916  upwlksfval  48920  isupwlk  48921  intop  48988  isclintop  48992  assintop  48994  isassintop  48995  assintopcllaw  48997  uzlidlring  49020  elrngchomALTV  49054  rngccatidALTV  49057  rngcsectALTV  49060  rngcisoALTV  49062  rhmsubcALTVlem3  49068  rhmsubcALTVlem4  49069  funcringcsetcALTV2lem7  49081  funcringcsetcALTV2lem9  49083  elringchomALTV  49088  ringccatidALTV  49091  ringcsectALTV  49094  ringcisoALTV  49096  ringcbasbasALTV  49097  funcringcsetclem7ALTV  49104  funcringcsetclem9ALTV  49106  srhmsubcALTV  49110  smprngprmrng  49124  cbvmpox2  49136  ply1sclrmsm  49184  dmatALTbasel  49202  lcoval  49212  lindslinindsimp1  49257  lindslinindsimp2  49263  lmod1  49292  elbigo  49351  elbigo2  49352  elbigolo1  49357  dig2nn0ld  49404  naryfvalel  49430  rrxlines  49533  rrxlinesc  49535  rrxlinec  49536  eenglngeehlnm  49539  elrrx2linest2  49545  rrxsphere  49548  itsclc0  49571  itsclc0b  49572  itsclinecirc0  49573  itsclinecirc0b  49574  itscnhlinecirc02p  49585  brab2dd  49626  f1omo  49691  f1omoOLD  49692  lubeldm2d  49756  glbeldm2d  49757  catprs  49809  sectpropdlem  49834  nelsubc3lem  49868  initc  49889  imaid  49952  upfval  49974  upfval2  49975  upfval3  49976  uppropd  49979  oppcinito  50033  oppctermo  50034  oppczeroo  50035  initopropd  50041  termopropd  50042  isthinc  50217  isthincd2lem1  50223  thincmoALT  50227  thincmod  50228  isthincd  50234  thincpropd  50240  indcthing  50258  discthing  50259  prsthinc  50262  termcterm  50311  termc2  50316  isinito4  50345  2arwcatlem1  50393  setc1onsubc  50400  cnelsubclem  50401  ranval3  50429  lmdfval2  50453  cmdfval2  50454  termolmd  50468  elsetrecslem  50497