Theorem eleq2d 2845

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 2771	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	sylib 210	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		anbi2 626	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1876	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 17	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		df-clel 2774	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		df-clel 2774	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4g 306	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386  ∀wal 1599   = wceq 1601  ∃wex 1823   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-clel 2774

This theorem is referenced by:  eleq2  2848  eleq12d  2853  eleqtrd  2861  neleqtrd  2880  abeq2d  2894  nfceqdf  2930  drnfc1  2951  drnfc1OLD  2952  drnfc2  2953  raleqbidv  3326  rexeqbidv  3327  sbcbid  3701  cbvcsb  3756  csbie2g  3782  cbvralcsf  3783  cbvreucsf  3785  cbvrabcsf  3786  sbcel12  4208  sbcel1g  4212  sbcel2  4214  csbeq2d  4216  prel12gOLD  4615  prel12g  4627  eliuni  4759  iuneq12df  4777  cbviun  4790  cbviin  4791  iinxsng  4833  iinxprg  4834  iunxsng  4835  iunxsngf  4837  cbvdisj  4864  disjor  4868  disjiund  4877  mpteq12f  4967  mpteq12df  4970  axpweq  5076  rabxfrd  5129  rbropapd  5252  opeliunxp  5416  opeliunxp2  5506  iunxpf  5516  elrelimasn  5743  elimasng  5745  elimasni  5746  xpdifid  5816  ressn  5925  predbrg  5953  funfni  6237  fnbr  6239  dffv3  6442  elfv2ex  6488  fvelrnb  6503  foelrni  6504  fvun1  6529  fvco2  6533  elfvmptrab1  6567  elfvmptrab  6568  elpreima  6600  dff3  6636  fmptco  6661  fnelfp  6708  fnelnfp  6710  tpres  6738  fnprb  6744  fntpb  6745  funfvima3  6768  eluniima  6780  dff13  6784  f1eqcocnv  6828  isoini  6860  riotaeqdv  6884  mpt2eq123dva  6993  cbvmpt2x  7010  ovelrn  7087  elovmpt2  7156  elovmpt2rab  7157  elovmpt2rab1  7158  elovmpt3rab1  7170  fun11iun  7405  zfrep6  7413  fmpt2x  7516  el2mpt2csbcl  7530  el2mpt2cl  7531  bropopvvv  7536  bropfvvvv  7538  elsuppfn  7584  suppfnss  7601  suppfnssOLD  7602  opeliunxp2f  7618  mpt2xopn0yelv  7621  mpt2xopovel  7628  rntpos  7647  mpt2curryd  7677  wfrdmcl  7706  wfrlem12  7709  onoviun  7723  smoel  7740  smoiso  7742  smoel2  7743  smo11  7744  tfrlem9  7764  oalimcl  7924  oaass  7925  omordi  7930  omordlim  7941  omlimcl  7942  odi  7943  omeulem1  7946  omeulem2  7947  oen0  7950  oeordi  7951  oeordsuc  7958  oelimcl  7964  oeeulem  7965  oeeui  7966  nnmordi  7995  oaabs2  8009  omabs  8011  omsmolem  8017  ereldm  8072  iiner  8102  elmapg  8153  elpmg  8156  elixpsn  8233  ixpsnf1o  8234  boxriin  8236  omxpenlem  8349  pw2f1olem  8352  phplem4  8430  php3  8434  elfi  8607  dffi3  8625  marypha2lem2  8630  ordiso2  8709  wemapsolem  8744  elharval  8757  inf3lemd  8821  inf3lem1  8822  inf3lem2  8823  inf3lem3  8824  cantnfs  8860  cantnfp1lem3  8874  cantnflem1b  8880  cantnflem1  8883  trcl  8901  r1sdom  8934  r1ordg  8938  r1pwss  8944  tz9.12lem3  8949  tz9.12  8950  r1elwf  8956  rankr1ai  8958  rankidb  8960  rankr1bg  8963  rankval2  8978  rankunb  9010  tcrank  9044  acni  9201  acni2  9202  acndom  9207  infpwfien  9218  alephnbtwn  9227  cardaleph  9245  cardinfima  9253  iunfictbso  9270  dfac3  9277  dfac5lem5  9283  dfac5  9284  dfac9  9293  dfac12r  9303  kmlem2  9308  kmlem12  9318  kmlem13  9319  kmlem14  9320  ackbij2lem3  9398  ackbij2  9400  cofsmo  9426  alephsing  9433  fin23lem30  9499  isf32lem9  9518  itunisuc  9576  axcc2lem  9593  axcc3  9595  domtriomlem  9599  axdc2lem  9605  axdc2  9606  axdc3lem2  9608  axdc3lem4  9610  axdc4lem  9612  ac6c4  9638  zorn2lem1  9653  ttukeylem6  9671  pwcfsdom  9740  axregndlem2  9760  axinfndlem1  9762  axacndlem4  9767  axacnd  9769  pwfseqlem1  9815  inar1  9932  inatsk  9935  gruurn  9955  grur1  9977  eltskm  10000  genpelv  10157  eluz1  11996  eluzadd  12021  eluzsub  12022  elixx1  12496  elixx3g  12500  elioo2  12528  elfz1  12648  elfz2  12650  elfzp1  12708  fzpr  12713  fzsuc2  12716  fzrev3  12724  elfzp12  12737  fzm1  12738  elfzo  12791  fz0add1fz1  12857  elfzo0l  12877  elfzom1b  12886  fzosplitsni  12898  elfzr  12900  elfzlmr  12901  zmodidfzo  13018  seqp1  13134  seqf1o  13160  bcval  13409  bcpasc  13426  hashf1lem1  13553  fundmge2nop0  13588  wrdmap  13635  elovmpt2wrd  13648  ccatfval  13663  elfzelfzccat  13670  ccatlid  13676  ccatass  13678  ccatrn  13679  ccatalpha  13683  swrdidOLD  13745  swrd0len0OLD  13755  swrd0fvOLD  13758  swrdeqOLD  13763  swrdfv2  13765  ccatswrd  13776  swrdccat2  13778  pfxfv  13791  pfxeq  13805  ccatpfx  13810  swrdswrd  13814  swrdswrd0OLD  13817  swrdpfx  13818  pfxpfx  13820  cats1un  13841  swrdccatfn  13850  swrdccatin1  13851  swrdccatin12lem1  13852  pfxccatin12lem1  13854  swrdccatin12lem2bOLD  13855  swrdccatin2  13856  swrdccatin12lem2c  13857  pfxccatin12lem2  13858  swrdccatin12lem2OLD  13859  swrdccat3blem  13871  swrdccatin1d  13878  swrdccatin2d  13879  pfxccatin12d  13880  swrdccatin12dOLD  13881  revccat  13912  revrev  13913  repswpfx  13931  repswccat  13932  cshwidxmod  13954  2cshw  13964  cshwcshid  13978  cshwcsh2id  13979  cshimadifsn  13980  cshimadifsn0  13981  revco  13985  ccatco  13986  cshco  13987  swrdco  13988  ofccat  14117  shftfn  14220  shftval  14221  limsupgle  14616  ello12  14655  elo12  14666  isercolllem3  14805  sumeq1  14827  fsumsplit  14878  sumsplit  14904  fsum2dlem  14906  fsumcom2  14910  fsumparts  14942  explecnv  15001  fprodser  15082  fprodsplit  15099  fprod2dlem  15113  fprodcom2  15117  eftlub  15241  divalgmod  15536  bitsval  15552  bitsp1e  15560  bitsp1o  15561  sadfval  15580  sadcp1  15583  sadval  15584  sadcadd  15586  sadadd2  15588  saddisjlem  15592  sadadd  15595  sadass  15599  smufval  15605  smuval  15609  smuval2  15610  smupvallem  15611  smu01lem  15613  smueqlem  15618  smumul  15621  bezoutlem2  15663  bezoutlem4  15665  algfx  15699  eucalgcvga  15705  reumodprminv  15913  nnnn0modprm0  15915  unbenlem  16016  prmreclem5  16028  vdwapval  16081  vdwapun  16082  vdwnnlem1  16103  vdwnn  16106  ramval  16116  0ram  16128  ramub1lem2  16135  prmgaplem7  16165  prmlem0  16211  elrest  16474  prdsbasmpt  16516  prdsleval  16523  prdsbasmpt2  16528  pwselbasb  16534  imasaddfnlem  16574  imasvscafn  16583  divsfval  16593  ismre  16636  mreunirn  16647  mrisval  16676  ismri  16677  isacs  16697  catidd  16726  iscatd2  16727  ismon  16778  isepi  16785  sectffval  16795  sectfval  16796  dfiso2  16817  cicsym  16849  issubc  16880  catsubcat  16884  isfunc  16909  funcres  16941  funcpropd  16945  ffthiso  16974  isnat  16992  isnat2  16993  fuciso  17020  initoval  17032  termoval  17033  isinito  17035  istermo  17036  iszeroo  17037  isinitoi  17038  istermoi  17039  initoid  17040  termoid  17041  iszeroi  17044  2initoinv  17045  initoeu1  17046  initoeu2  17051  2termoinv  17052  termoeu1  17053  arwhoma  17080  elsetchom  17116  setcmon  17122  setcepi  17123  setciso  17126  catciso  17142  elestrchom  17153  estrcbasbas  17156  funcestrcsetclem7  17172  funcestrcsetclem8  17173  funcestrcsetclem9  17174  fthestrcsetc  17176  fullestrcsetc  17177  equivestrcsetc  17178  setc1strwun  17179  funcsetcestrclem7  17187  funcsetcestrclem8  17188  funcsetcestrclem9  17189  fthsetcestrc  17191  fullsetcestrc  17192  hofcl  17285  hofpropd  17293  yonedalem4c  17303  yonedainv  17307  yonffthlem  17308  lubeldm  17367  glbeldm  17380  joindef  17390  meetdef  17404  poslubdg  17535  acsficl2d  17562  acsmapd  17564  psref  17594  psss  17600  dirge  17623  issstrmgm  17638  grpidval  17646  grpidpropd  17647  grpidd  17654  ismndd  17699  mndpropd  17702  imasmnd2  17713  imasmnd  17714  ismhm  17723  issubm  17733  gsumccat  17764  imasgrp2  17917  imasgrp  17918  issubg  17978  subginv  17985  isnsg  18007  isghm  18044  resghm2b  18062  conjnmzb  18079  conjnsg  18080  ghmpropd  18082  isga  18107  elcntz  18138  elcntzsn  18141  cntzrcl  18143  resscntz  18147  symgextf1  18224  gsmsymgreqlem2  18234  f1otrspeq  18250  pmtrfrn  18261  pmtrdifellem3  18281  pmtrdifellem4  18282  psgnunilem1  18296  psgnunilem5  18297  psgnunilem5OLD  18298  psgnunilem2  18299  psgnunilem3  18300  psgneldm2  18308  psgnfitr  18321  psgnsn  18324  gexdvds  18383  gex1  18390  isslw  18407  sylow3lem2  18427  lsmelvalx  18439  pj1ghm  18500  efgtlen  18523  efgsfo  18537  efgredlemc  18543  frgp0  18559  frgpmhm  18564  qusabl  18654  frgpnabllem1  18662  0cyg  18680  cycsubgcyg  18688  gsumval3  18694  gsumcllem  18695  gsumzaddlem  18707  gsumzsplit  18713  gsummptfzcl  18754  eldprd  18790  dprdcntz2  18824  dprd2d2  18830  dmdprdsplit2lem  18831  dmdprdsplit2  18832  dprdsplit  18834  ablfac2  18875  isringd  18972  imasring  19006  dvdsrval  19032  isunit  19044  dvdsrpropd  19083  isirred  19086  isrhm  19110  isrim0  19112  drngunit  19144  isdrngd  19164  issubrg  19172  opprsubrg  19193  rhmpropd  19207  isabv  19211  issrngd  19253  islmod  19259  lmodprop2d  19317  islss  19327  islssd  19328  lssats2  19395  lspsnel  19398  islmhm  19422  lmhmf1o  19441  lmhmima  19442  lmhmpreima  19443  reslmhm  19447  pwssplit3  19456  lmhmpropd  19468  islbs  19471  lspprel  19489  lspfixed  19523  lspfixedOLD  19524  lbsacsbs  19553  lbsextlem1  19555  lbsextlem2  19556  lbsextlem3  19557  lbsextlem4  19558  ixpsnbasval  19606  lidlmcl  19614  quscrng  19637  islpidl  19643  lidldvgen  19652  assamulgscmlem2  19746  mplsubglem  19831  mpllsslem  19832  mplmonmul  19861  subrgascl  19894  subrgasclcl  19895  mpfind  19932  gsumply1subr  20000  lply1binomsc  20073  zrhrhmb  20255  znf1o  20295  frgpcyg  20317  psgnevpmb  20328  isphld  20397  phlssphl  20402  elocv  20411  iscss  20426  isobs  20463  obs2ss  20472  dsmmbas2  20480  dsmmfi  20481  dsmmelbas  20482  dsmmlss  20487  frlmelbas  20499  frlmlbs  20540  frlmup1  20541  ellspd  20545  islinds  20552  islindf2  20557  f1lindf  20565  islindf4  20581  matbas2d  20633  matecl  20635  matvscl  20641  mat1  20658  mat0dim0  20678  mat0dimid  20679  mat0dimscm  20680  mat1dimelbas  20682  dmatel  20704  scmatel  20716  scmateALT  20723  scmataddcl  20727  scmatsubcl  20728  smatvscl  20735  scmatghm  20744  mat1scmat  20750  mdetunilem7  20829  mdetunilem9  20831  smadiadetr  20887  cramerimplem2  20897  cramer0  20903  pmatcoe1fsupp  20913  cpmatpmat  20922  cpmatel  20923  cpmatacl  20928  cpmatinvcl  20929  mat2pmatghm  20942  mat2pmatmul  20943  decpmatmullem  20983  pmatcollpwlem  20992  pmatcollpw3fi1lem1  20998  pmatcollpwscmatlem1  21001  monmat2matmon  21036  chfacfscmul0  21070  chfacfscmulgsum  21072  chfacfpmmulgsum  21076  cayhamlem1  21078  cpmadugsumlemB  21086  cpmadugsumlemC  21087  cpmadugsumlemF  21088  cayhamlem2  21096  istopon  21124  eltg  21169  eltg2  21170  eltop  21186  eltop2  21187  eltop3  21188  pptbas  21220  iscld  21239  neiss2  21313  isnei  21315  neiptopnei  21344  neiptopreu  21345  lpfval  21350  lpval  21351  islp  21352  maxlp  21359  islpi  21361  neitr  21392  restlp  21395  ordtbas2  21403  ordtrest2  21416  lmfval  21444  cnfval  21445  iscn  21447  iscnp  21449  tgcn  21464  tgcnp  21465  lmbrf  21472  cnpresti  21500  ist1  21533  ist1-2  21559  cnt1  21562  haust1  21564  cmpfi  21620  cmpfii  21621  1stcfb  21657  2ndc1stc  21663  1stcrest  21665  2ndcdisj  21668  1stcelcls  21673  nllyi  21687  subislly  21693  islocfin  21729  lfinpfin  21736  locfindis  21742  locfincf  21743  comppfsc  21744  kgenval  21747  elkgen  21748  kgencn2  21769  txbas  21779  eltx  21780  ptval  21782  ptpjpre1  21783  ptopn2  21796  ptpjopn  21824  ptclsg  21827  xkoccn  21831  txdis  21844  txdis1cn  21847  ptrescn  21851  hausdiag  21857  hauseqlcld  21858  txhaus  21859  xkohaus  21865  elqtop  21909  qtopeu  21928  kqcldsat  21945  hmeofval  21970  ptuncnv  22019  ptunhmeo  22020  elmptrab  22039  fbdmn0  22046  elfg  22083  elfilss  22088  filunirn  22094  fixufil  22134  elfm  22159  rnelfmlem  22164  rnelfm  22165  fmfnfmlem4  22169  elflim2  22176  flimtopon  22182  elflim  22183  hausflim  22193  flimcls  22197  flfnei  22203  isflf  22205  hausflf  22209  cnpflf  22213  cnflf  22214  txflf  22218  isfcls  22221  fclstopon  22224  isfcls2  22225  fclssscls  22230  fclsnei  22231  fclsfnflim  22239  flimfnfcls  22240  isfcf  22246  fcfelbas  22248  cnpfcf  22253  cnfcf  22254  flfcntr  22255  alexsublem  22256  alexsubALTlem3  22261  cnextfun  22276  cnextfvval  22277  cnextf  22278  cnextcn  22279  cnextfres  22281  tmdgsum2  22308  tgpconncomp  22324  ghmcnp  22326  qustgplem  22332  eltsms  22344  haustsms  22347  tsmsgsum  22350  tsmssubm  22354  tsmssplit  22363  isust  22415  elrnust  22436  ustbas  22439  elutop  22445  ustuqtoplem  22451  ustuqtop4  22456  ustuqtop  22458  utopsnneiplem  22459  utopsnneip  22460  utopsnnei  22461  isusp  22473  isucn  22490  ucncn  22497  iscfilu  22500  neipcfilu  22508  iscusp  22511  cnextucn  22515  ispsmet  22517  ismet  22536  isxmet  22537  elblps  22600  elbl  22601  elmopn  22655  prdsbl  22704  neibl  22714  met1stc  22734  metrest  22737  prdsxmslem2  22742  txmetcnp  22760  txmetcn  22761  metuval  22762  metustsym  22768  cfilucfil2  22774  elbl4  22776  metuel  22777  psmetutop  22780  restmetu  22783  metucn  22784  tngngp  22866  isnmhm  22958  zcld  23024  metnrmlem1a  23069  elcncf  23100  cncfcnvcn  23132  cnheibor  23162  lebnumlem1  23168  ishtpy  23179  isphtpy  23188  om1elbas  23239  elpi1  23252  pi1xfr  23262  pi1coghm  23268  tcphcph  23443  lmmbrf  23468  iscfil  23471  iscau  23482  iscauf  23486  caucfil  23489  iscmet  23490  cmetcaulem  23494  iscmet3lem1  23497  iscmet3lem2  23498  iscmet3  23499  bcthlem1  23530  cmsss  23557  cmetcusp1  23559  cmetcusp  23560  cmscsscms  23579  rrxcph  23598  minveclem3b  23634  ovolfioo  23671  ovolficc  23672  ovolctb  23694  ovoliunnul  23711  ovolshftlem1  23713  sca2rab  23716  ovolscalem1  23717  ovolicc2lem1  23721  ovolicc2lem2  23722  ovolicc2lem4  23724  ovolicc2lem5  23725  iundisj  23752  iunmbl2  23761  uniioombllem3  23789  vitalilem2  23813  vitalilem3  23814  mbfss  23850  i1faddlem  23897  i1fmullem  23898  mbfi1fseqlem2  23920  mbfi1fseqlem4  23922  mbfi1fseq  23925  itg2splitlem  23952  itg2split  23953  itg2monolem1  23954  itg2gt0  23964  isibl  23969  iblss2  24009  itgss3  24018  itgsplit  24039  ellimc  24074  limcmo  24083  cnlimc  24089  limciun  24095  limcun  24096  eldv  24099  dvbsss  24103  dvreslem  24110  elcpn  24134  dvaddf  24142  dvmulf  24143  dvcof  24148  rolle  24190  dvlip2  24195  dvivthlem1  24208  lhop1  24214  lhop2  24215  ftc1cn  24243  fta1glem2  24363  plyco0  24385  elply  24388  ply1termlem  24396  eltayl  24551  tayl0  24553  taylplem1  24554  taylplem2  24555  dvtaylp  24561  taylthlem1  24564  taylthlem2  24565  abelth  24632  cxpcn3  24929  rlimcnp  25144  fsumharmonic  25190  dchrelbas  25413  pntrsumbnd2  25708  ostth2lem2  25775  istrkgb  25806  istrkgcb  25807  istrkge  25808  istrkgl  25809  istrkgld  25810  axtgsegcon  25815  axtg5seg  25816  axtgbtwnid  25817  axtgpasch  25818  axtgupdim2  25822  axtgeucl  25823  tgdim01  25858  iscgrg  25863  isismt  25885  tglnunirn  25899  tglngval  25902  tgellng  25904  legval  25935  legov  25936  legov2  25937  ishlg  25953  mirreu3  26005  mirval  26006  mirfv  26007  mircgr  26008  mirbtwn  26009  ismir  26010  mireq  26016  symquadlem  26040  israg  26048  perpln1  26061  perpln2  26062  isperp  26063  islnopp  26087  outpasch  26103  ishpg  26107  iscgra  26157  acopyeu  26183  isinag  26187  isleag  26196  iseqlg  26216  f1otrgitv  26219  f1otrg  26220  f1otrge  26221  ttgval  26224  ttgelitv  26232  elee  26243  brbtwn  26248  brcgr  26249  axlowdimlem16  26306  ebtwntg  26331  elntg2  26334  upgrex  26440  edgupgr  26482  upgredg  26486  edglnl  26492  numedglnl  26493  uhgr2edg  26554  umgr2edg1  26557  usgredg2vlem1  26571  usgredg2vlem2  26572  ushgredgedg  26575  ushgredgedgloop  26577  ushgredgedgloopOLD  26578  uhgrspansubgrlem  26637  fusgrfisstep  26676  nbgrval  26683  nbgrel  26687  nbupgrel  26692  nbgr2vtx1edg  26697  nbuhgr2vtx1edgblem  26698  nbuhgr2vtx1edgb  26699  nbusgreledg  26700  usgrnbcnvfv  26712  uvtxval  26735  uvtxel  26736  uvtx01vtx  26745  uvtxusgrel  26751  nbcplgr  26782  cplgr3v  26783  cusgrexi  26791  structtocusgr  26794  vtxdgfval  26815  vtxdg0v  26821  vtxdeqd  26825  vtxdun  26829  1loopgrnb0  26850  1loopgrvd0  26852  1hevtxdg0  26853  1hevtxdg1  26854  1egrvtxdg1  26857  umgr2v2evtxel  26870  umgr2v2enb1  26874  umgr2v2evd2  26875  vtxdginducedm1lem4  26890  vtxdginducedm1  26891  finsumvtxdg2sstep  26897  ewlksfval  26949  isewlk  26950  wksfval  26957  iswlk  26958  uspgr2wlkeq  26993  wlkres  27019  wlkresOLD  27021  usgr2pthlem  27115  clwlkcompim  27132  uspgrn2crct  27157  wwlks  27184  iswwlksn  27187  wwlknvtx  27194  wlkiswwlks2  27224  wwlksm1edg  27230  wwlksm1edgOLD  27231  wwlksnred  27252  wwlksnredOLD  27253  wwlksnext  27254  wwlksnredwwlkn  27257  wwlksnredwwlknOLD  27258  wwlksnredwwlkn0  27259  wwlksnredwwlkn0OLD  27260  wwlksnwwlksnon  27295  wspn0  27304  usgr2wspthons3  27344  rusgrnumwwlkb0  27351  clwwlk  27363  clwwlkccatlem  27369  clwlkclwwlklem2a4  27377  clwlkclwwlk  27382  clwlkclwwlkOLD  27383  clwwisshclwwslem  27403  clwwlkinwwlk  27429  clwwlkinwwlkOLD  27430  clwwlkel  27437  clwwlkfOLD  27438  clwwlkf  27443  clwwlkext2edg  27453  wwlksext2clwwlk  27454  wwlksubclwwlk  27455  wwlksubclwwlkOLD  27456  clwwnisshclwwsn  27457  eleclclwwlknlem2  27459  erclwwlknsym  27468  erclwwlkntr  27469  umgrhashecclwwlk  27476  clwwlkvbij  27515  clwwlkvbijOLD  27516  eupth2lem3lem3  27634  eupth2lem3lem4  27635  eupth2lem3lem6  27637  eupth2lemb  27641  eucrct2eupthOLD  27650  eucrct2eupth  27651  fusgreg2wsplem  27741  2clwwlklem  27751  2clwwlklemOLD  27752  2clwwlk2clwwlklem  27757  2clwwlkel  27760  2clwwlk2clwwlk  27761  2clwwlk2clwwlkOLD  27762  extwwlkfabel  27767  extwwlkfabelOLD  27768  clwwlknonclwlknonf1o  27785  clwwlknonclwlknonf1oOLD  27786  dlwwlknondlwlknonf1olem1  27789  dlwwlknonclwlknonf1olem1OLD  27790  numclwwlk2lem1  27804  numclwlk2lem2f  27805  numclwlk2lem2f1o  27807  numclwlk2lem2fOLD  27808  numclwlk2lem2f1oOLD  27810  ex-res  27873  isssp  28151  sspn  28163  islno  28180  isblo  28209  nmlno0  28222  ishmo  28238  dipdir  28269  dipass  28272  ubthlem1  28298  ubthlem2  28299  htthlem  28346  htth  28347  ocel  28712  ocnel  28729  shsel  28745  shsel2  28753  shmodsi  28820  pjhtheu  28825  pjeq  28830  axpjpj  28851  pjoc2  28870  elspani  28974  h1de2ctlem  28986  elspansn  28997  elspansn2  28998  elnlfn  29359  eleigvec  29388  riesz3i  29493  cbviunf  29935  iuneq12daf  29936  iunrdx  29944  iunrnmptss  29946  cbvdisjf  29948  disjorf  29955  disjabrex  29958  disjabrexf  29959  iundisjf  29965  disjrdx  29967  elimampt  30003  elunirn2  30016  abfmpunirn  30017  abfmpeld  30019  abfmpel  30020  fmptcof2  30022  acunirnmpt2  30025  acunirnmpt2f  30026  aciunf1lem  30027  funcnvmpt  30032  suppss3  30068  fpwrelmap  30074  xrofsup  30098  iundisjfi  30119  eliccioo  30201  inftmrel  30296  isinftm  30297  isslmd  30317  gsummpt2co  30342  xrge0tsmsbi  30348  rngurd  30350  resv1r  30399  ellspds  30415  dimpropd  30425  lbslsat  30432  smatrcl  30460  smatcl  30466  txomap  30499  locfinreflem  30505  metidval  30531  pstmval  30536  cnre2csqima  30555  ordtrest2NEW  30567  fmcncfil  30575  fsumcvg4  30594  ofcfval  30758  measvuni  30875  meascnbl  30880  faeval  30907  ismbfm  30912  elunirnmbfm  30913  isanmbfm  30916  imambfm  30922  elcarsg  30965  itgeq12dv  30986  issibf  30993  eulerpartlems  31020  eulerpartlemgc  31022  eulerpartlemgvv  31036  eulerpartlemgu  31037  eulerpart  31042  rrvmbfm  31103  elorvc  31120  elorrvc  31124  dstfrvunirn  31135  ballotlemfc0  31153  ballotlemfcc  31154  ballotlemsima  31176  ballotlemrv  31180  fzssfzo  31212  signstfvn  31246  signstfvneq0  31250  signstres  31253  repr0  31291  reprinrn  31298  reprdifc  31307  hgt750lemg  31334  hgt750lemb  31336  istrkg2d  31346  axtgupdim2OLD  31348  afsval  31351  brafs  31352  bnj945  31443  bnj1400  31505  bnj18eq1  31596  bnj916  31602  bnj1014  31629  bnj1015  31630  bnj1110  31649  bnj1417  31708  subfacp1lem2b  31762  subfacp1lem4  31764  subfacp1lem5  31765  subfacp1lem6  31766  ptpconn  31814  cvmscbv  31839  iscvm  31840  cvmsi  31846  cvmsval  31847  cvmliftmolem1  31862  cvmlift2lem12  31895  cvmlift2lem13  31896  cvmlift3lem7  31906  snmlval  31912  mrsubfval  32004  mrsubvrs  32018  mclsrcl  32057  mclsval  32059  mppsval  32068  mclsppslem  32079  opelco3  32266  trpredrec  32326  wsuclem  32359  frrlem5e  32377  nolesgn2ores  32414  noprefixmo  32437  nosupdm  32439  nosupfv  32441  nosupres  32442  nosupbnd1lem1  32443  nosupbnd1lem3  32445  nosupbnd1lem5  32447  nosupbnd2lem1  32450  funtransport  32727  fvtransport  32728  brcolinear  32755  colineardim1  32757  funray  32836  fvray  32837  funline  32838  fvline  32840  lineelsb2  32844  fwddifval  32858  fwddifnval  32859  rankelg  32864  rankeq1o  32867  elhf2  32871  0hf  32873  neibastop2lem  32943  neibastop3  32945  eltail  32957  bj-projeq  33552  bj-projval  33556  bj-restsn  33608  bj-eldiag  33670  bj-eldiag2  33671  mptsnunlem  33781  dissneqlem  33783  iooelexlt  33805  relowlssretop  33806  finxpeq1  33818  finxpreclem6  33828  curf  34014  uncf  34015  curunc  34018  unccur  34019  fin2so  34023  lindsadd  34030  lindsdom  34031  lindsenlbs  34032  matunitlindflem1  34033  matunitlindflem2  34034  matunitlindf  34035  ptrest  34036  ptrecube  34037  poimirlem2  34039  poimirlem8  34045  poimirlem17  34054  poimirlem18  34055  poimirlem20  34057  poimirlem21  34058  poimirlem22  34059  poimirlem24  34061  poimirlem26  34063  poimirlem29  34066  heicant  34072  mblfinlem1  34074  mblfinlem2  34075  volsupnfl  34082  itg2addnclem  34088  itg2gt0cn  34092  indexdom  34156  incsequz  34170  istotbnd  34194  istotbnd3  34196  0totbnd  34198  sstotbnd  34200  sstotbnd3  34201  isbnd  34205  prdstotbnd  34219  cntotbnd  34221  isismty  34226  heibor1lem  34234  heiborlem2  34237  heiborlem3  34238  heibor  34246  isass  34271  exidcl  34301  exidreslem  34302  elghomlem2OLD  34311  rngoidmlem  34361  rngo1cl  34364  divrngcl  34382  isdrngo2  34383  isrngohom  34390  isrngoiso  34403  isriscg  34409  iscom2  34420  iscringd  34423  isidl  34439  ispridl  34459  ismaxidl  34465  ac6s6  34605  dmecd  34706  prter3  35038  islshp  35135  islsat  35147  lcvfbr  35176  islfl  35216  ellkr  35245  islshpkrN  35276  ldual1dim  35322  isopos  35336  cmtfvalN  35366  cvrfval  35424  isat  35442  islln  35662  islpln  35686  islvol  35729  isline  35895  ispointN  35898  ispsubsp  35901  elpmap  35914  elpmapat  35920  elpadd  35955  paddclN  35998  elpclN  36048  elpcliN  36049  pclfinN  36056  pclcmpatN  36057  ispsubclN  36093  iswatN  36150  islhp  36152  islaut  36239  ispautN  36255  isldil  36266  isltrn  36275  isdilN  36310  istrnN  36313  istendo  36916  dvhb1dimN  37142  erng1lem  37143  erngdvlem4-rN  37155  diaelval  37189  diaeldm  37192  dia1dimid  37219  cdlemm10N  37274  dibopelvalN  37299  dibopelval2  37301  dibelval3  37303  dibelval1st  37305  dibelval2nd  37308  dibeldmN  37314  dibvalrel  37319  dibglbN  37322  dicffval  37330  dicfval  37331  dicopelval  37333  dicelvalN  37334  dicelval3  37336  dicvalrelN  37341  dicelval1sta  37343  diclspsn  37350  dihopelvalbN  37394  dihopelvalcqat  37402  dihopelvalcpre  37404  dihvalrel  37435  dih1  37442  dihmeetlem4preN  37462  dihmeetlem13N  37475  dih1dimatlem  37485  dochnel2  37548  dihjatcclem4  37577  dvh2dim  37601  dvh3dim  37602  dvh4dimN  37603  dochfln0  37633  lpolsetN  37638  islpolN  37639  lcfrvalsnN  37697  lcfrlem21  37719  lcfrlem27  37725  lcfrlem37  37735  lcfr  37741  lcdlss  37775  mapdcv  37816  hdmap1fval  37952  hdmapffval  37982  hdmapfval  37983  hdmapval  37984  hgmapffval  38041  hgmapfval  38042  hdmapellkr  38070  hlhilhillem  38116  isnacs  38231  mrefg2  38234  elmzpcl  38253  mzpcompact2  38279  eldiophb  38284  elpell1qr  38375  elpell14qr  38377  elpell1234qr  38379  pw2f1ocnv  38567  pw2f1o2val2  38570  aomclem4  38590  aomclem6  38592  islssfg2  38604  imasgim  38633  lnr2i  38649  elmnc  38669  rngunsnply  38706  issdrg  38730  fiinfi  38839  elintima  38906  eliunov2  38932  ov2ssiunov2  38953  brtrclfv2  38980  rfovcnvf1od  39258  rfovcnvfvd  39261  fsovrfovd  39263  fsovfvd  39264  fsovcnvlem  39267  ntrclsfv1  39313  ntrclselnel1  39315  ntrclsneine0lem  39322  ntrneifv1  39337  ntrneifv2  39338  ntrneiel  39339  gneispace2  39390  gneispacess2  39404  extoimad  39424  dvconstbi  39493  bccbc  39504  iunxsngf2  40165  eliin2f  40220  rabbida2  40248  disjinfi  40307  unirnmap  40325  elmptima  40388  iuneqfzuzlem  40462  iooiinioc  40695  fsumiunss  40719  fsumsupp0  40722  lptre2pt  40784  icccncfext  41032  cncfiooicclem1  41038  dvnprodlem2  41094  stoweidlem27  41175  stoweidlem29  41177  stoweidlem31  41179  stoweidlem34  41182  stoweidlem48  41196  stoweidlem59  41207  dirkercncflem2  41252  dirkercncflem4  41254  fourierdlem2  41257  fourierdlem3  41258  fourierdlem25  41280  fourierdlem32  41287  fourierdlem33  41288  fourierdlem41  41296  fourierdlem48  41302  fourierdlem49  41303  fourierdlem62  41316  fourierdlem70  41324  fourierdlem80  41334  fourierdlem92  41346  fourierdlem93  41347  fourierdlem101  41355  etransclem37  41419  sge0val  41511  sge0f1o  41527  sge0iunmptlemre  41560  sge0iunmpt  41563  iundjiun  41605  caragenel  41640  ovncvrrp  41709  ovnsubaddlem1  41715  ovnsubadd  41717  hoidmvlelem2  41741  hoidmvlelem3  41742  hoidmvlelem4  41743  hoidmvle  41745  ovncvr2  41756  hspdifhsp  41761  hoiqssbl  41770  hspmbllem2  41772  hspmbl  41774  opnvonmbllem1  41777  isvonmbl  41783  ovnovollem1  41801  issmflem  41867  smflimlem3  41912  smflimlem4  41913  smflim  41916  smfmullem2  41930  smflimmpt  41947  smfsuplem1  41948  smflimsuplem1  41957  smflimsuplem3  41959  smflimsuplem4  41960  smflimsuplem7  41963  smflimsup  41965  afvelrnb  42208  afvelrnb0  42209  afv2co2  42302  el1fzopredsuc  42371  iccpart  42388  iccpartgtprec  42392  iccpartiltu  42394  iccpartigtl  42395  iccpartltu  42397  iccpartgtl  42398  iccpartgt  42399  iccpartleu  42400  iccpartgel  42401  iccelpart  42405  iccpartiun  42406  icceuelpart  42408  fargshiftfv  42411  fargshiftfo  42414  sprel  42427  prprelb  42459  prprelprb  42460  pwdif  42526  sbgoldbo  42704  wtgoldbnnsum4prm  42719  bgoldbnnsum3prm  42721  bgoldbtbndlem3  42724  bgoldbtbnd  42726  upwlksfval  42762  isupwlk  42763  mgmpropd  42794  ismgmhm  42802  issubmgm  42808  intop  42858  isclintop  42862  assintop  42864  isassintop  42865  assintopcllaw  42867  isrnghm  42911  isrngisom  42915  c0ghm  42930  c0snghm  42935  uzlidlring  42948  rnghmresel  42983  elrngchom  42987  rnghmsubcsetclem1  42994  rnghmsubcsetclem2  42995  rngcid  42998  rngcsect  42999  rngciso  43001  elrngchomALTV  43005  rngccatidALTV  43008  rngcsectALTV  43011  rngcisoALTV  43013  funcrngcsetcALT  43018  zrinitorngc  43019  zrtermorngc  43020  rhmresel  43029  elringchom  43033  rhmsubcsetclem1  43040  rhmsubcsetclem2  43041  ringcid  43044  rhmsscrnghm  43045  rhmsubcrngclem1  43046  rhmsubcrngclem2  43047  ringcsect  43050  ringciso  43052  ringcbasbas  43053  funcringcsetcALTV2lem7  43061  funcringcsetcALTV2lem9  43063  elringchomALTV  43068  ringccatidALTV  43071  ringcsectALTV  43074  ringcisoALTV  43076  ringcbasbasALTV  43077  funcringcsetclem7ALTV  43084  funcringcsetclem9ALTV  43086  irinitoringc  43088  zrtermoringc  43089  srhmsubc  43095  rhmsubclem3  43107  rhmsubclem4  43108  srhmsubcALTV  43113  rhmsubcALTVlem3  43125  rhmsubcALTVlem4  43126  opeliun2xp  43130  cbvmpt2x2  43133  ply1sclrmsm  43190  dmatALTbasel  43210  lcoval  43220  lindslinindsimp1  43265  lindslinindsimp2  43271  lmod1  43300  elbigo  43364  elbigo2  43365  elbigolo1  43370  dig2nn0ld  43417  rrxlines  43473  rrxlinesc  43475  rrxlinec  43476  eenglngeehlnm  43479  elrrx2linest2  43485  rrxsphere  43488  itsclc0  43511  itsclc0b  43512  itsclinecirc0  43513  itsclinecirc0b  43514  itscnhlinecirc02p  43525  elsetrecslem  43554