Theorem eleq2d 2875

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  eleq2  2878  eleq12d  2884  eleqtrd  2892  neleqtrd  2911  abeq2d  2924  nfceqdf  2951  drnfc1  2974  drnfc2  2975  raleqbidv  3354  rexeqbidv  3355  sbcbid  3773  csbeq2d  3834  cbvcsbw  3838  cbvcsb  3839  csbie2g  3868  cbvralcsf  3870  cbvreucsf  3872  cbvrabcsf  3873  sbcel12  4316  sbcel1g  4321  sbcel2  4323  prel12g  4754  opeq1  4763  opeq2  4765  eliuni  4887  iuneqconst  4892  iuneq12df  4907  cbviun  4923  cbviin  4924  cbviung  4925  cbviing  4926  iinxsng  4973  iinxprg  4974  iunxsng  4975  iunxsngf  4977  cbvdisj  5005  disjor  5010  disjiund  5020  mpteq12df  5112  mpteq12f  5113  axpweq  5230  rabxfrd  5283  rbropapd  5414  opeliunxp  5583  opeliunxp2  5673  iunxpf  5683  elrelimasn  5920  elimasng  5922  elimasni  5923  xpdifid  5992  ressn  6104  predbrg  6136  funfni  6428  fnbr  6430  dffv3  6641  elfv2ex  6686  fvelrnb  6701  foelrni  6702  fvun1  6729  fvco2  6735  elfvmptrab1w  6771  elfvmptrab1  6772  elfvmptrab  6773  elpreima  6805  dff3  6843  fmptco  6868  fnelfp  6914  fnelnfp  6916  tpres  6940  fnprb  6948  fntpb  6949  funfvima3  6976  eluniima  6987  dff13  6991  f1eqcocnv  7035  f1eqcocnvOLD  7036  isoini  7070  riotaeqdv  7094  mpoeq123dva  7207  cbvmpox  7226  ovelrn  7304  elovmpo  7370  elovmporab  7371  elovmporab1w  7372  elovmporab1  7373  elovmpt3rab1  7385  fiun  7626  f1iun  7627  zfrep6  7638  fmpox  7747  el2mpocsbcl  7763  el2mpocl  7764  bropopvvv  7768  bropfvvvv  7770  elsuppfn  7821  suppfnss  7838  opeliunxp2f  7859  mpoxopn0yelv  7862  mpoxopovel  7869  rntpos  7888  mpocurryd  7918  wfrdmcl  7946  wfrlem12  7949  onoviun  7963  smoel  7980  smoiso  7982  smoel2  7983  smo11  7984  tfrlem9  8004  oalimcl  8169  oaass  8170  omordi  8175  omordlim  8186  omlimcl  8187  odi  8188  omeulem1  8191  omeulem2  8192  oen0  8195  oeordi  8196  oeordsuc  8203  oelimcl  8209  oeeulem  8210  oeeui  8211  nnmordi  8240  oaabs2  8255  omabs  8257  omsmolem  8263  ereldm  8320  iiner  8352  elmapg  8402  elpmg  8405  elixpsn  8484  ixpsnf1o  8485  boxriin  8487  omxpenlem  8601  pw2f1olem  8604  phplem4  8683  php3  8687  elfi  8861  dffi3  8879  marypha2lem2  8884  ordiso2  8963  wemapsolem  8998  elharval  9009  inf3lemd  9074  inf3lem1  9075  inf3lem2  9076  inf3lem3  9077  cantnfs  9113  cantnfp1lem3  9127  cantnflem1b  9133  cantnflem1  9136  trcl  9154  r1sdom  9187  r1ordg  9191  r1pwss  9197  tz9.12lem3  9202  tz9.12  9203  r1elwf  9209  rankr1ai  9211  rankidb  9213  rankr1bg  9216  rankval2  9231  rankunb  9263  tcrank  9297  acni  9456  acni2  9457  acndom  9462  infpwfien  9473  alephnbtwn  9482  cardaleph  9500  cardinfima  9508  iunfictbso  9525  dfac3  9532  dfac5lem5  9538  dfac5  9539  dfac9  9547  dfac12r  9557  kmlem2  9562  kmlem12  9572  kmlem13  9573  kmlem14  9574  ackbij2lem3  9652  ackbij2  9654  cofsmo  9680  alephsing  9687  fin23lem30  9753  isf32lem9  9772  itunisuc  9830  axcc2lem  9847  axcc3  9849  domtriomlem  9853  axdc2lem  9859  axdc2  9860  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  ac6c4  9892  zorn2lem1  9907  ttukeylem6  9925  pwcfsdom  9994  axregndlem2  10014  axinfndlem1  10016  axacndlem4  10021  axacnd  10023  pwfseqlem1  10069  inar1  10186  inatsk  10189  gruurn  10209  grur1  10231  eltskm  10254  genpelv  10411  eluz1  12235  eluzadd  12261  eluzsub  12262  elixx1  12735  elixx3g  12739  elioo2  12767  elfz1  12890  elfz2  12892  elfzp1  12952  fzpr  12957  fzsuc2  12960  fzrev3  12968  elfzp12  12981  fzm1  12982  elfzo  13035  fz0add1fz1  13102  elfzo0l  13122  elfzom1b  13131  fzosplitsni  13143  elfzr  13145  elfzlmr  13146  zmodidfzo  13263  seqp1  13379  seqf1o  13407  bcval  13660  bcpasc  13677  hashf1lem1  13809  fundmge2nop0  13846  wrdmap  13889  elovmpowrd  13901  ccatfval  13916  elfzelfzccat  13925  ccatlid  13931  ccatass  13933  ccatrn  13934  ccatalpha  13938  swrdfv2  14014  ccatswrd  14021  swrdccat2  14022  pfxfv  14035  pfxeq  14049  ccatpfx  14054  swrdswrd  14058  swrdpfx  14060  pfxpfx  14061  cats1un  14074  swrdccatfn  14077  swrdccatin1  14078  pfxccatin12lem4  14079  pfxccatin12lem1  14081  swrdccatin2  14082  pfxccatin12lem2c  14083  pfxccatin12lem2  14084  swrdccat3blem  14092  swrdccatin1d  14096  swrdccatin2d  14097  pfxccatin12d  14098  revccat  14119  revrev  14120  repswpfx  14138  repswccat  14139  cshwidxmod  14156  2cshw  14166  cshwcshid  14180  cshwcsh2id  14181  cshimadifsn  14182  cshimadifsn0  14183  revco  14187  ccatco  14188  cshco  14189  swrdco  14190  ofccat  14320  shftfn  14424  shftval  14425  limsupgle  14826  ello12  14865  elo12  14876  isercolllem3  15015  sumeq1  15037  fsumsplit  15089  sumsplit  15115  fsum2dlem  15117  fsumcom2  15121  fsumparts  15153  explecnv  15212  pwdif  15215  fprodser  15295  fprodsplit  15312  fprod2dlem  15326  fprodcom2  15330  eftlub  15454  divalgmod  15747  bitsval  15763  bitsp1e  15771  bitsp1o  15772  sadfval  15791  sadcp1  15794  sadval  15795  sadcadd  15797  sadadd2  15799  saddisjlem  15803  sadadd  15806  sadass  15810  smufval  15816  smuval  15820  smuval2  15821  smupvallem  15822  smu01lem  15824  smueqlem  15829  smumul  15832  bezoutlem2  15878  bezoutlem4  15880  algfx  15914  eucalgcvga  15920  reumodprminv  16131  nnnn0modprm0  16133  unbenlem  16234  prmreclem5  16246  vdwapval  16299  vdwapun  16300  vdwnnlem1  16321  vdwnn  16324  ramval  16334  0ram  16346  ramub1lem2  16353  prmgaplem7  16383  prmlem0  16431  elrest  16693  prdsbasmpt  16735  prdsleval  16742  prdsbasmpt2  16747  pwselbasb  16753  imasaddfnlem  16793  imasvscafn  16802  divsfval  16812  ismre  16853  mreunirn  16864  mrisval  16893  ismri  16894  isacs  16914  catidd  16943  iscatd2  16944  ismon  16995  isepi  17002  sectffval  17012  sectfval  17013  dfiso2  17034  cicsym  17066  issubc  17097  catsubcat  17101  isfunc  17126  funcres  17158  funcpropd  17162  ffthiso  17191  isnat  17209  isnat2  17210  fuciso  17237  initoval  17249  termoval  17250  isinito  17252  istermo  17253  iszeroo  17254  isinitoi  17255  istermoi  17256  initoid  17257  termoid  17258  iszeroi  17261  2initoinv  17262  initoeu1  17263  initoeu2  17268  2termoinv  17269  termoeu1  17270  arwhoma  17297  elsetchom  17333  setcmon  17339  setcepi  17340  setciso  17343  catciso  17359  elestrchom  17370  estrcbasbas  17373  funcestrcsetclem7  17388  funcestrcsetclem8  17389  funcestrcsetclem9  17390  fthestrcsetc  17392  fullestrcsetc  17393  equivestrcsetc  17394  setc1strwun  17395  funcsetcestrclem7  17403  funcsetcestrclem8  17404  funcsetcestrclem9  17405  fthsetcestrc  17407  fullsetcestrc  17408  hofcl  17501  hofpropd  17509  yonedalem4c  17519  yonedainv  17523  yonffthlem  17524  lubeldm  17583  glbeldm  17596  joindef  17606  meetdef  17620  poslubdg  17751  acsficl2d  17778  acsmapd  17780  psref  17810  psss  17816  dirge  17839  issstrmgm  17855  grpidval  17863  grpidpropd  17864  grpidd  17873  ismndd  17925  mndpropd  17928  imasmnd2  17940  imasmnd  17941  ismhm  17950  issubm  17960  gsumsgrpccat  17996  gsumccatOLD  17997  elefmndbas2  18031  smndex1mndlem  18066  imasgrp2  18206  imasgrp  18207  issubg  18271  subginv  18278  isnsg  18299  isghm  18350  resghm2b  18368  conjnmzb  18385  conjnsg  18386  ghmpropd  18388  isga  18413  elcntz  18444  elcntzsn  18447  cntzrcl  18449  resscntz  18454  symgextf1  18541  gsmsymgreqlem2  18551  f1otrspeq  18567  pmtrfrn  18578  pmtrdifellem3  18598  pmtrdifellem4  18599  psgnunilem1  18613  psgnunilem5  18614  psgnunilem2  18615  psgnunilem3  18616  psgneldm2  18624  psgnfitr  18637  psgnsn  18640  gexdvds  18701  gex1  18708  isslw  18725  sylow3lem2  18745  lsmelvalx  18757  pj1ghm  18821  efgtlen  18844  efgsfo  18857  efgredlemc  18863  frgp0  18878  frgpmhm  18883  qusabl  18978  frgpnabllem1  18986  cycsubmcmn  19001  0cyg  19006  cycsubgcyg  19014  gsumval3  19020  gsumcllem  19021  gsumzaddlem  19034  gsumzsplit  19040  gsummptfzcl  19082  eldprd  19119  dprdcntz2  19153  dprd2d2  19159  dmdprdsplit2lem  19160  dmdprdsplit2  19161  dprdsplit  19163  ablfac2  19204  isringd  19331  imasring  19365  dvdsrval  19391  isunit  19403  dvdsrpropd  19442  isirred  19445  isrhm  19469  isrim0  19471  drngunit  19500  isdrngd  19520  issubrg  19528  opprsubrg  19549  rhmpropd  19564  issdrg  19567  isabv  19583  issrngd  19625  islmod  19631  lmodprop2d  19689  islss  19699  islssd  19700  lssats2  19765  lspsnel  19768  islmhm  19792  lmhmf1o  19811  lmhmima  19812  lmhmpreima  19813  reslmhm  19817  pwssplit3  19826  lmhmpropd  19838  islbs  19841  lspprel  19859  lspfixed  19893  lbsacsbs  19921  lbsextlem1  19923  lbsextlem2  19924  lbsextlem3  19925  lbsextlem4  19926  ixpsnbasval  19975  lidlmcl  19983  quscrng  20006  islpidl  20012  lidldvgen  20021  zrhrhmb  20204  znf1o  20243  frgpcyg  20265  psgnevpmb  20276  isphld  20343  phlssphl  20348  elocv  20357  iscss  20372  isobs  20409  obs2ss  20418  dsmmfi  20427  dsmmelbas  20428  dsmmlss  20433  frlmelbas  20445  frlmlbs  20486  frlmup1  20487  ellspd  20491  islinds  20498  islindf2  20503  f1lindf  20511  islindf4  20527  assamulgscmlem2  20586  mplsubglem  20672  mpllsslem  20673  mplmonmul  20704  subrgascl  20737  subrgasclcl  20738  mpfind  20779  ismhp  20793  mhplss  20803  gsumply1subr  20863  lply1binomsc  20936  matbas2d  21028  matecl  21030  matvscl  21036  mat1  21052  mat0dim0  21072  mat0dimid  21073  mat0dimscm  21074  mat1dimelbas  21076  dmatel  21098  scmatel  21110  scmateALT  21117  scmataddcl  21121  scmatsubcl  21122  smatvscl  21129  scmatghm  21138  mat1scmat  21144  mdetunilem7  21223  mdetunilem9  21225  smadiadetr  21280  cramerimplem2  21289  cramer0  21295  pmatcoe1fsupp  21306  cpmatpmat  21315  cpmatel  21316  cpmatacl  21321  cpmatinvcl  21322  mat2pmatghm  21335  mat2pmatmul  21336  decpmatmullem  21376  pmatcollpwlem  21385  pmatcollpw3fi1lem1  21391  pmatcollpwscmatlem1  21394  monmat2matmon  21429  chfacfscmul0  21463  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  cayhamlem1  21471  cpmadugsumlemB  21479  cpmadugsumlemC  21480  cpmadugsumlemF  21481  cayhamlem2  21489  istopon  21517  eltg  21562  eltg2  21563  eltop  21579  eltop2  21580  eltop3  21581  pptbas  21613  iscld  21632  neiss2  21706  isnei  21708  neiptopnei  21737  neiptopreu  21738  lpfval  21743  lpval  21744  islp  21745  maxlp  21752  islpi  21754  neitr  21785  restlp  21788  ordtbas2  21796  ordtrest2  21809  lmfval  21837  cnfval  21838  iscn  21840  iscnp  21842  tgcn  21857  tgcnp  21858  lmbrf  21865  cnpresti  21893  ist1  21926  ist1-2  21952  cnt1  21955  haust1  21957  cmpfi  22013  cmpfii  22014  1stcfb  22050  2ndc1stc  22056  1stcrest  22058  2ndcdisj  22061  1stcelcls  22066  nllyi  22080  subislly  22086  islocfin  22122  lfinpfin  22129  locfindis  22135  locfincf  22136  comppfsc  22137  kgenval  22140  elkgen  22141  kgencn2  22162  txbas  22172  eltx  22173  ptval  22175  ptpjpre1  22176  ptopn2  22189  ptpjopn  22217  ptclsg  22220  xkoccn  22224  txdis  22237  txdis1cn  22240  ptrescn  22244  hausdiag  22250  hauseqlcld  22251  txhaus  22252  xkohaus  22258  elqtop  22302  qtopeu  22321  kqcldsat  22338  hmeofval  22363  ptuncnv  22412  ptunhmeo  22413  elmptrab  22432  fbdmn0  22439  elfg  22476  elfilss  22481  filunirn  22487  fixufil  22527  elfm  22552  rnelfmlem  22557  rnelfm  22558  fmfnfmlem4  22562  elflim2  22569  flimtopon  22575  elflim  22576  hausflim  22586  flimcls  22590  flfnei  22596  isflf  22598  hausflf  22602  cnpflf  22606  cnflf  22607  txflf  22611  isfcls  22614  fclstopon  22617  isfcls2  22618  fclssscls  22623  fclsnei  22624  fclsfnflim  22632  flimfnfcls  22633  isfcf  22639  fcfelbas  22641  cnpfcf  22646  cnfcf  22647  flfcntr  22648  alexsublem  22649  alexsubALTlem3  22654  cnextfun  22669  cnextfvval  22670  cnextf  22671  cnextcn  22672  tmdgsum2  22701  tgpconncomp  22718  ghmcnp  22720  qustgplem  22726  eltsms  22738  haustsms  22741  tsmsgsum  22744  tsmssubm  22748  tsmssplit  22757  isust  22809  elrnust  22830  ustbas  22833  elutop  22839  ustuqtoplem  22845  ustuqtop4  22850  ustuqtop  22852  utopsnneiplem  22853  utopsnneip  22854  utopsnnei  22855  isusp  22867  isucn  22884  ucncn  22891  iscfilu  22894  neipcfilu  22902  iscusp  22905  cnextucn  22909  ispsmet  22911  ismet  22930  isxmet  22931  elblps  22994  elbl  22995  elmopn  23049  prdsbl  23098  neibl  23108  met1stc  23128  metrest  23131  prdsxmslem2  23136  txmetcnp  23154  txmetcn  23155  metuval  23156  metustsym  23162  cfilucfil2  23168  elbl4  23170  metuel  23171  psmetutop  23174  restmetu  23177  metucn  23178  tngngp  23260  isnmhm  23352  zcld  23418  metnrmlem1a  23463  elcncf  23494  cncfcnvcn  23530  cnheibor  23560  lebnumlem1  23566  ishtpy  23577  isphtpy  23586  om1elbas  23637  elpi1  23650  pi1xfr  23660  pi1coghm  23666  tcphcph  23841  lmmbrf  23866  iscfil  23869  iscau  23880  iscauf  23884  caucfil  23887  iscmet  23888  cmetcaulem  23892  iscmet3lem1  23895  iscmet3lem2  23896  iscmet3  23897  bcthlem1  23928  cmsss  23955  cmetcusp1  23957  cmetcusp  23958  cmscsscms  23977  rrxcph  23996  minveclem3b  24032  ovolfioo  24071  ovolficc  24072  ovolctb  24094  ovoliunnul  24111  ovolshftlem1  24113  sca2rab  24116  ovolscalem1  24117  ovolicc2lem1  24121  ovolicc2lem2  24122  ovolicc2lem4  24124  ovolicc2lem5  24125  iundisj  24152  iunmbl2  24161  uniioombllem3  24189  vitalilem2  24213  vitalilem3  24214  mbfss  24250  i1faddlem  24297  i1fmullem  24298  mbfi1fseqlem2  24320  mbfi1fseqlem4  24322  mbfi1fseq  24325  itg2splitlem  24352  itg2split  24353  itg2monolem1  24354  itg2gt0  24364  isibl  24369  iblss2  24409  itgss3  24418  itgsplit  24439  ellimc  24476  limcmo  24485  cnlimc  24491  limciun  24497  limcun  24498  eldv  24501  dvbsss  24505  dvreslem  24512  elcpn  24537  dvaddf  24545  dvmulf  24546  dvcof  24551  rolle  24593  dvlip2  24598  dvivthlem1  24611  lhop1  24617  lhop2  24618  ftc1cn  24646  fta1glem2  24767  plyco0  24789  elply  24792  ply1termlem  24800  eltayl  24955  tayl0  24957  taylplem1  24958  taylplem2  24959  dvtaylp  24965  taylthlem1  24968  taylthlem2  24969  abelth  25036  cxpcn3  25337  rlimcnp  25551  fsumharmonic  25597  dchrelbas  25820  pntrsumbnd2  26151  ostth2lem2  26218  istrkgb  26249  istrkgcb  26250  istrkge  26251  istrkgl  26252  istrkgld  26253  axtgsegcon  26258  axtg5seg  26259  axtgbtwnid  26260  axtgpasch  26261  axtgupdim2  26265  axtgeucl  26266  tgdim01  26301  iscgrg  26306  isismt  26328  tglnunirn  26342  tglngval  26345  tgellng  26347  legval  26378  legov  26379  legov2  26380  ishlg  26396  mirreu3  26448  mirval  26449  mirfv  26450  mircgr  26451  mirbtwn  26452  ismir  26453  mireq  26459  symquadlem  26483  israg  26491  perpln1  26504  perpln2  26505  isperp  26506  islnopp  26533  outpasch  26549  ishpg  26553  iscgra  26603  dfcgra2  26624  isinag  26632  isleag  26641  iseqlg  26661  f1otrgitv  26664  f1otrg  26665  f1otrge  26666  ttgval  26669  ttgelitv  26677  elee  26688  brbtwn  26693  brcgr  26694  axlowdimlem16  26751  ebtwntg  26776  elntg2  26779  upgrex  26885  edgupgr  26927  upgredg  26930  edglnl  26936  numedglnl  26937  uhgr2edg  26998  umgr2edg1  27001  usgredg2vlem1  27015  usgredg2vlem2  27016  ushgredgedg  27019  ushgredgedgloop  27021  uhgrspansubgrlem  27080  fusgrfisstep  27119  nbgrval  27126  nbgrel  27130  nbupgrel  27135  nbgr2vtx1edg  27140  nbuhgr2vtx1edgblem  27141  nbuhgr2vtx1edgb  27142  nbusgreledg  27143  usgrnbcnvfv  27155  uvtxval  27177  uvtxel  27178  uvtx01vtx  27187  uvtxusgrel  27193  nbcplgr  27224  cplgr3v  27225  cusgrexi  27233  structtocusgr  27236  vtxdgfval  27257  vtxdg0v  27263  vtxdeqd  27267  vtxdun  27271  1loopgrnb0  27292  1loopgrvd0  27294  1hevtxdg0  27295  1hevtxdg1  27296  1egrvtxdg1  27299  umgr2v2evtxel  27312  umgr2v2enb1  27316  umgr2v2evd2  27317  vtxdginducedm1lem4  27332  vtxdginducedm1  27333  finsumvtxdg2sstep  27339  ewlksfval  27391  isewlk  27392  wksfval  27399  iswlk  27400  uspgr2wlkeq  27435  wlkres  27460  usgr2pthlem  27552  clwlkcompim  27569  uspgrn2crct  27594  wwlks  27621  iswwlksn  27624  wwlknvtx  27631  wlkiswwlks2  27661  wwlksm1edg  27667  wwlksnred  27678  wwlksnext  27679  wwlksnredwwlkn  27681  wwlksnredwwlkn0  27682  wwlksnwwlksnon  27701  wspn0  27710  usgr2wspthons3  27750  rusgrnumwwlkb0  27757  clwwlk  27768  clwwlkccatlem  27774  clwlkclwwlklem2a4  27782  clwlkclwwlk  27787  clwwisshclwwslem  27799  clwwlkinwwlk  27825  clwwlkel  27831  clwwlkf  27832  clwwlkext2edg  27841  wwlksext2clwwlk  27842  wwlksubclwwlk  27843  clwwnisshclwwsn  27844  eleclclwwlknlem2  27846  erclwwlknsym  27855  erclwwlkntr  27856  umgrhashecclwwlk  27863  clwwlkvbij  27898  eupth2lem3lem3  28015  eupth2lem3lem4  28016  eupth2lem3lem6  28018  eupth2lemb  28022  eucrct2eupth  28030  fusgreg2wsplem  28118  2clwwlklem  28128  2clwwlk2clwwlklem  28131  2clwwlkel  28134  2clwwlk2clwwlk  28135  extwwlkfabel  28138  clwwlknonclwlknonf1o  28147  dlwwlknondlwlknonf1olem1  28149  numclwwlk2lem1  28161  numclwlk2lem2f  28162  numclwlk2lem2f1o  28164  ex-res  28226  isssp  28507  sspn  28519  islno  28536  isblo  28565  nmlno0  28578  ishmo  28594  dipdir  28625  dipass  28628  ubthlem1  28653  ubthlem2  28654  htthlem  28700  htth  28701  ocel  29064  ocnel  29081  shsel  29097  shsel2  29105  shmodsi  29172  pjhtheu  29177  pjeq  29182  axpjpj  29203  pjoc2  29222  elspani  29326  h1de2ctlem  29338  elspansn  29349  elspansn2  29350  elnlfn  29711  eleigvec  29740  riesz3i  29845  cbviunf  30319  iuneq12daf  30320  iunrdx  30327  iunrnmptss  30329  cbvdisjf  30334  disjorf  30342  disjabrex  30345  disjabrexf  30346  iundisjf  30352  disjrdx  30354  elimampt  30397  2ndresdju  30411  elunirn2  30414  abfmpunirn  30415  abfmpeld  30417  abfmpel  30418  fmptcof2  30420  acunirnmpt2  30423  acunirnmpt2f  30424  aciunf1lem  30425  funcnvmpt  30430  suppss3  30486  fpwrelmap  30495  xrofsup  30518  iundisjfi  30545  eliccioo  30633  s3f1  30649  ccatf1  30651  swrdrn3  30655  ismnt  30691  mgcoval  30694  gsummpt2co  30733  gsumpart  30740  gsumhashmul  30741  xrge0tsmsbi  30743  cycpmco2  30825  cyc3co2  30832  inftmrel  30859  isinftm  30860  isslmd  30880  rngurd  30907  resv1r  30961  eqg0el  30977  ellspds  30984  lbslsp  30992  rhmimaidl  31017  isprmidl  31021  qsidomlem1  31036  qsidomlem2  31037  ismxidl  31042  isrprm  31073  dimpropd  31095  lbslsat  31102  extdg1id  31141  smatrcl  31149  smatcl  31155  ist0cld  31186  txomap  31187  locfinreflem  31193  zarclsiin  31224  zart0  31232  rhmpreimacnlem  31237  metidval  31243  pstmval  31248  cnre2csqima  31264  ordtrest2NEW  31276  fmcncfil  31284  fsumcvg4  31303  ofcfval  31467  measvuni  31583  meascnbl  31588  faeval  31615  ismbfm  31620  elunirnmbfm  31621  isanmbfm  31624  imambfm  31630  elcarsg  31673  itgeq12dv  31694  issibf  31701  eulerpartlems  31728  eulerpartlemgc  31730  eulerpartlemgvv  31744  eulerpartlemgu  31745  eulerpart  31750  rrvmbfm  31810  elorvc  31827  elorrvc  31831  dstfrvunirn  31842  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemsima  31883  ballotlemrv  31887  fzssfzo  31919  signstfvn  31949  signstfvneq0  31952  signstres  31955  repr0  31992  reprinrn  31999  reprdifc  32008  hgt750lemg  32035  hgt750lemb  32037  istrkg2d  32047  axtgupdim2ALTV  32049  afsval  32052  brafs  32053  bnj945  32155  bnj1400  32217  bnj18eq1  32309  bnj916  32315  bnj1014  32343  bnj1015  32344  bnj1110  32364  bnj1417  32423  revpfxsfxrev  32475  cplgredgex  32480  pfxwlk  32483  revwlk  32484  subfacp1lem2b  32541  subfacp1lem4  32543  subfacp1lem5  32544  subfacp1lem6  32545  ptpconn  32593  cvmscbv  32618  iscvm  32619  cvmsi  32625  cvmsval  32626  cvmliftmolem1  32641  cvmlift2lem12  32674  cvmlift2lem13  32675  cvmlift3lem7  32685  snmlval  32691  satfv1  32723  satfvsucsuc  32725  satfrnmapom  32730  satf0op  32737  satf0n0  32738  sat1el2xp  32739  fmlafvel  32745  isfmlasuc  32748  fmlaomn0  32750  gonan0  32752  goaln0  32753  gonar  32755  goalr  32757  satffunlem1lem2  32763  satffunlem2lem2  32766  satfv0fvfmla0  32773  satef  32776  satefvfmla0  32778  sategoelfvb  32779  satfv1fvfmla1  32783  mrsubfval  32868  mrsubvrs  32882  mclsrcl  32921  mclsval  32923  mppsval  32932  mclsppslem  32943  opelco3  33131  trpredrec  33190  wsuclem  33225  fpr2  33253  frr2  33258  nolesgn2ores  33292  noprefixmo  33315  nosupdm  33317  nosupfv  33319  nosupres  33320  nosupbnd1lem1  33321  nosupbnd1lem3  33323  nosupbnd1lem5  33325  nosupbnd2lem1  33328  funtransport  33605  fvtransport  33606  brcolinear  33633  colineardim1  33635  funray  33714  fvray  33715  funline  33716  fvline  33718  lineelsb2  33722  fwddifval  33736  fwddifnval  33737  rankelg  33742  rankeq1o  33745  elhf2  33749  0hf  33751  neibastop2lem  33821  neibastop3  33823  eltail  33835  bj-projeq  34428  bj-projval  34432  bj-restsn  34497  opelopabbv  34558  brabd0  34562  bj-eldiag  34591  bj-eldiag2  34592  mptsnunlem  34755  dissneqlem  34757  iooelexlt  34779  relowlssretop  34780  rdgellim  34793  exrecfnlem  34796  finxpeq1  34803  finxpreclem6  34813  pibp21  34832  curf  35035  uncf  35036  curunc  35039  unccur  35040  fin2so  35044  lindsadd  35050  lindsdom  35051  lindsenlbs  35052  matunitlindflem1  35053  matunitlindflem2  35054  matunitlindf  35055  ptrest  35056  ptrecube  35057  poimirlem2  35059  poimirlem8  35065  poimirlem17  35074  poimirlem18  35075  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem24  35081  poimirlem26  35083  poimirlem29  35086  heicant  35092  mblfinlem1  35094  mblfinlem2  35095  volsupnfl  35102  itg2addnclem  35108  itg2gt0cn  35112  indexdom  35172  incsequz  35186  istotbnd  35207  istotbnd3  35209  0totbnd  35211  sstotbnd  35213  sstotbnd3  35214  isbnd  35218  prdstotbnd  35232  cntotbnd  35234  isismty  35239  heibor1lem  35247  heiborlem2  35250  heiborlem3  35251  heibor  35259  isass  35284  exidcl  35314  exidreslem  35315  elghomlem2OLD  35324  rngoidmlem  35374  rngo1cl  35377  divrngcl  35395  isdrngo2  35396  isrngohom  35403  isrngoiso  35416  isriscg  35422  iscom2  35433  iscringd  35436  isidl  35452  ispridl  35472  ismaxidl  35478  ac6s6  35610  dmecd  35722  releldmqs  36052  releldmqscoss  36054  erim2  36071  prter3  36178  islshp  36275  islsat  36287  lcvfbr  36316  islfl  36356  ellkr  36385  islshpkrN  36416  ldual1dim  36462  isopos  36476  cmtfvalN  36506  cvrfval  36564  isat  36582  islln  36802  islpln  36826  islvol  36869  isline  37035  ispointN  37038  ispsubsp  37041  elpmap  37054  elpmapat  37060  elpadd  37095  paddclN  37138  elpclN  37188  elpcliN  37189  pclfinN  37196  pclcmpatN  37197  ispsubclN  37233  iswatN  37290  islhp  37292  islaut  37379  ispautN  37395  isldil  37406  isltrn  37415  isdilN  37450  istrnN  37453  istendo  38056  dvhb1dimN  38282  erng1lem  38283  erngdvlem4-rN  38295  diaelval  38329  diaeldm  38332  dia1dimid  38359  cdlemm10N  38414  dibopelvalN  38439  dibopelval2  38441  dibelval3  38443  dibelval1st  38445  dibelval2nd  38448  dibeldmN  38454  dibvalrel  38459  dibglbN  38462  dicffval  38470  dicfval  38471  dicopelval  38473  dicelvalN  38474  dicelval3  38476  dicvalrelN  38481  dicelval1sta  38483  diclspsn  38490  dihopelvalbN  38534  dihopelvalcqat  38542  dihopelvalcpre  38544  dihvalrel  38575  dih1  38582  dihmeetlem4preN  38602  dihmeetlem13N  38615  dih1dimatlem  38625  dochnel2  38688  dihjatcclem4  38717  dvh2dim  38741  dvh3dim  38742  dvh4dimN  38743  dochfln0  38773  lpolsetN  38778  islpolN  38779  lcfrvalsnN  38837  lcfrlem21  38859  lcfrlem27  38865  lcfrlem37  38875  lcfr  38881  lcdlss  38915  mapdcv  38956  hdmap1fval  39092  hdmapffval  39122  hdmapfval  39123  hdmapval  39124  hgmapffval  39181  hgmapfval  39182  hdmapellkr  39210  hlhilhillem  39256  fzsplitnd  39270  fzosumm1  39421  frlmfielbas  39434  frlmsnic  39453  isnacs  39645  mrefg2  39648  elmzpcl  39667  mzpcompact2  39693  eldiophb  39698  elpell1qr  39788  elpell14qr  39790  elpell1234qr  39792  pw2f1ocnv  39978  pw2f1o2val2  39981  aomclem4  40001  aomclem6  40003  islssfg2  40015  imasgim  40044  lnr2i  40060  elmnc  40080  rngunsnply  40117  fiinfi  40272  sqrtcvallem1  40331  elintima  40354  eliunov2  40380  ov2ssiunov2  40401  brtrclfv2  40428  rfovcnvf1od  40705  rfovcnvfvd  40708  fsovrfovd  40710  fsovfvd  40711  fsovcnvlem  40714  ntrclsfv1  40758  ntrclselnel1  40760  ntrclsneine0lem  40767  ntrneifv1  40782  ntrneifv2  40783  ntrneiel  40784  gneispace2  40835  gneispacess2  40849  extoimad  40868  mnringelbased  40925  dvconstbi  41038  bccbc  41049  eliin2f  41740  rabbida2  41768  disjinfi  41820  unirnmap  41837  elmptima  41896  iuneqfzuzlem  41966  iooiinioc  42193  fsumiunss  42217  fsumsupp0  42220  lptre2pt  42282  icccncfext  42529  cncfiooicclem1  42535  dvnprodlem2  42589  stoweidlem27  42669  stoweidlem29  42671  stoweidlem31  42673  stoweidlem34  42676  stoweidlem48  42690  stoweidlem59  42701  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem2  42751  fourierdlem3  42752  fourierdlem25  42774  fourierdlem32  42781  fourierdlem33  42782  fourierdlem41  42790  fourierdlem48  42796  fourierdlem49  42797  fourierdlem62  42810  fourierdlem70  42818  fourierdlem80  42828  fourierdlem92  42840  fourierdlem93  42841  fourierdlem101  42849  etransclem37  42913  sge0val  43005  sge0f1o  43021  sge0iunmptlemre  43054  sge0iunmpt  43057  iundjiun  43099  caragenel  43134  ovncvrrp  43203  ovnsubaddlem1  43209  ovnsubadd  43211  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  hoidmvle  43239  ovncvr2  43250  hspdifhsp  43255  hoiqssbl  43264  hspmbllem2  43266  hspmbl  43268  opnvonmbllem1  43271  isvonmbl  43277  ovnovollem1  43295  issmflem  43361  smflimlem3  43406  smflimlem4  43407  smflim  43410  smfmullem2  43424  smflimmpt  43441  smfsuplem1  43442  smflimsuplem1  43451  smflimsuplem3  43453  smflimsuplem4  43454  smflimsuplem7  43457  smflimsup  43459  afvelrnb  43719  afvelrnb0  43720  afv2co2  43813  el1fzopredsuc  43882  iccpart  43933  iccpartgtprec  43937  iccpartiltu  43939  iccpartigtl  43940  iccpartltu  43942  iccpartgtl  43943  iccpartgt  43944  iccpartleu  43945  iccpartgel  43946  iccelpart  43950  iccpartiun  43951  icceuelpart  43953  fargshiftfv  43956  fargshiftfo  43959  sprel  44001  prprelb  44033  prprelprb  44034  fpprel  44246  sbgoldbo  44305  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  bgoldbtbndlem3  44325  bgoldbtbnd  44327  upwlksfval  44363  isupwlk  44364  mgmpropd  44395  ismgmhm  44403  issubmgm  44409  intop  44463  isclintop  44467  assintop  44469  isassintop  44470  assintopcllaw  44472  isrnghm  44516  isrngisom  44520  c0ghm  44535  c0snghm  44540  uzlidlring  44553  rnghmresel  44588  elrngchom  44592  rnghmsubcsetclem1  44599  rnghmsubcsetclem2  44600  rngcid  44603  rngcsect  44604  rngciso  44606  elrngchomALTV  44610  rngccatidALTV  44613  rngcsectALTV  44616  rngcisoALTV  44618  funcrngcsetcALT  44623  zrinitorngc  44624  zrtermorngc  44625  rhmresel  44634  elringchom  44638  rhmsubcsetclem1  44645  rhmsubcsetclem2  44646  ringcid  44649  rhmsscrnghm  44650  rhmsubcrngclem1  44651  rhmsubcrngclem2  44652  ringcsect  44655  ringciso  44657  ringcbasbas  44658  funcringcsetcALTV2lem7  44666  funcringcsetcALTV2lem9  44668  elringchomALTV  44673  ringccatidALTV  44676  ringcsectALTV  44679  ringcisoALTV  44681  ringcbasbasALTV  44682  funcringcsetclem7ALTV  44689  funcringcsetclem9ALTV  44691  irinitoringc  44693  zrtermoringc  44694  srhmsubc  44700  rhmsubclem3  44712  rhmsubclem4  44713  srhmsubcALTV  44718  rhmsubcALTVlem3  44730  rhmsubcALTVlem4  44731  opeliun2xp  44734  cbvmpox2  44737  ply1sclrmsm  44791  dmatALTbasel  44811  lcoval  44821  lindslinindsimp1  44866  lindslinindsimp2  44872  lmod1  44901  elbigo  44965  elbigo2  44966  elbigolo1  44971  dig2nn0ld  45018  naryfvalel  45044  rrxlines  45147  rrxlinesc  45149  rrxlinec  45150  eenglngeehlnm  45153  elrrx2linest2  45159  rrxsphere  45162  itsclc0  45185  itsclc0b  45186  itsclinecirc0  45187  itsclinecirc0b  45188  itscnhlinecirc02p  45199  elsetrecslem  45228