Theorem eleq2d 2825

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 2732	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	sylib 217	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		anbi2 633	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1836	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 17	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		dfclel 2818	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		dfclel 2818	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  eleq2  2828  eleq12d  2834  eleqtrd  2842  neleqtrd  2861  abeq2d  2875  nfceqdfOLD  2904  drnfc1OLD  2928  drnfc2OLD  2930  raleqbidv  3337  rexeqbidv  3338  elabd2  3602  sbcbid  3775  csbeq2d  3839  cbvcsbw  3843  cbvcsb  3844  csbie  3869  csbied  3871  csbie2g  3876  cbvralcsf  3878  cbvreucsf  3880  cbvrabcsf  3881  sbcel12  4343  sbcel1g  4348  sbcel2  4350  prel12g  4795  eliuni  4931  iuneqconst  4936  iuneq12df  4951  cbviun  4967  cbviin  4968  cbviung  4969  cbviing  4970  iinxsng  5018  iinxprg  5019  iunxsng  5020  iunxsngf  5022  cbvdisj  5050  disjor  5055  disjiund  5065  mpteq12da  5160  mpteq12dfOLD  5162  mpteq12f  5163  mpteq12dva  5164  axpweq  5288  rabxfrd  5341  rbropapd  5478  opeliunxp  5655  opeliunxp2  5750  iunxpf  5760  elrelimasn  5996  elimasngOLD  6001  elimasni  6002  xpdifid  6076  ressn  6192  predbrg  6228  funfni  6548  fnbr  6550  dffv3  6779  elfv2ex  6824  fvelrnb  6839  foelrni  6840  fvun1  6868  fvco2  6874  elfvmptrab1w  6910  elfvmptrab1  6911  elfvmptrab  6912  elpreima  6944  dff3  6985  fmptco  7010  fnelfp  7056  fnelnfp  7058  tpres  7085  fnprb  7093  fntpb  7094  funfvima3  7121  eluniima  7132  elunirn2  7135  dff13  7137  f1eqcocnv  7182  f1eqcocnvOLD  7183  isoini  7218  riotaeqdv  7242  mpoeq123dva  7358  cbvmpox  7377  ovelrn  7457  elovmpo  7523  elovmporab  7524  elovmporab1w  7525  elovmporab1  7526  elovmpt3rab1  7538  fiun  7794  f1iun  7795  zfrep6  7806  fmpox  7916  el2mpocsbcl  7934  el2mpocl  7935  bropopvvv  7939  bropfvvvv  7941  elsuppfng  7995  elsuppfn  7996  suppfnss  8014  opeliunxp2f  8035  mpoxopn0yelv  8038  mpoxopovel  8045  rntpos  8064  mpocurryd  8094  fpr2  8129  wfrdmclOLD  8157  wfrlem12OLD  8160  wfr2  8176  onoviun  8183  smoel  8200  smoiso  8202  smoel2  8203  smo11  8204  tfrlem9  8225  oalimcl  8400  oaass  8401  omordi  8406  omordlim  8417  omlimcl  8418  odi  8419  omeulem1  8422  omeulem2  8423  oen0  8426  oeordi  8427  oeordsuc  8434  oelimcl  8440  oeeulem  8441  oeeui  8442  nnmordi  8471  oaabs2  8488  omabs  8490  omsmolem  8496  ereldm  8555  iiner  8587  elmapg  8637  elpmg  8640  elixpsn  8734  ixpsnf1o  8735  boxriin  8737  omxpenlem  8869  pw2f1olem  8872  phplem2  9000  php3  9004  phplem4OLD  9012  php3OLD  9016  elfi  9181  dffi3  9199  marypha2lem2  9204  ordiso2  9283  wemapsolem  9318  elharval  9329  inf3lemd  9394  inf3lem1  9395  inf3lem2  9396  inf3lem3  9397  cantnfs  9433  cantnfp1lem3  9447  cantnflem1b  9453  cantnflem1  9456  ttrclselem2  9493  trcl  9495  frr2  9527  r1sdom  9541  r1ordg  9545  r1pwss  9551  tz9.12lem3  9556  tz9.12  9557  r1elwf  9563  rankr1ai  9565  rankidb  9567  rankr1bg  9570  rankval2  9585  rankunb  9617  tcrank  9651  acni  9810  acni2  9811  acndom  9816  infpwfien  9827  alephnbtwn  9836  cardaleph  9854  cardinfima  9862  iunfictbso  9879  dfac3  9886  dfac5lem5  9892  dfac5  9893  dfac9  9901  dfac12r  9911  kmlem2  9916  kmlem12  9926  kmlem13  9927  kmlem14  9928  ackbij2lem3  10006  ackbij2  10008  cofsmo  10034  alephsing  10041  fin23lem30  10107  isf32lem9  10126  itunisuc  10184  axcc2lem  10201  axcc3  10203  domtriomlem  10207  axdc2lem  10213  axdc2  10214  axdc3lem2  10216  axdc3lem4  10218  axdc4lem  10220  ac6c4  10246  zorn2lem1  10261  ttukeylem6  10279  pwcfsdom  10348  axregndlem2  10368  axinfndlem1  10370  axacndlem4  10375  axacnd  10377  pwfseqlem1  10423  inar1  10540  inatsk  10543  gruurn  10563  grur1  10585  eltskm  10608  genpelv  10765  eluz1  12595  eluzadd  12622  eluzsub  12623  elixx1  13097  elixx3g  13101  elioo2  13129  elfz1  13253  elfz2  13255  elfzp1  13315  fzpr  13320  fzsuc2  13323  fzrev3  13331  elfzp12  13344  fzm1  13345  elfzo  13398  fz0add1fz1  13466  elfzo0l  13486  elfzom1b  13495  fzosplitsni  13507  elfzr  13509  elfzlmr  13510  zmodidfzo  13629  seqp1  13745  seqf1o  13773  bcval  14027  bcpasc  14044  hashf1lem1  14177  hashf1lem1OLD  14178  fundmge2nop0  14215  wrdmap  14258  elovmpowrd  14270  ccatfval  14285  elfzelfzccat  14294  ccatlid  14300  ccatass  14302  ccatrn  14303  ccatalpha  14307  swrdfv2  14383  ccatswrd  14390  swrdccat2  14391  pfxfv  14404  pfxeq  14418  ccatpfx  14423  swrdswrd  14427  swrdpfx  14429  pfxpfx  14430  cats1un  14443  swrdccatfn  14446  swrdccatin1  14447  pfxccatin12lem4  14448  pfxccatin12lem1  14450  swrdccatin2  14451  pfxccatin12lem2c  14452  pfxccatin12lem2  14453  swrdccat3blem  14461  swrdccatin1d  14465  swrdccatin2d  14466  pfxccatin12d  14467  revccat  14488  revrev  14489  repswpfx  14507  repswccat  14508  cshwidxmod  14525  2cshw  14535  cshwcshid  14549  cshwcsh2id  14550  cshimadifsn  14551  cshimadifsn0  14552  revco  14556  ccatco  14557  cshco  14558  swrdco  14559  ofccat  14689  shftfn  14793  shftval  14794  limsupgle  15195  ello12  15234  elo12  15245  isercolllem3  15387  sumeq1  15409  fsumsplit  15462  sumsplit  15489  fsum2dlem  15491  fsumcom2  15495  fsumparts  15527  explecnv  15586  pwdif  15589  fprodser  15668  fprodsplit  15685  fprod2dlem  15699  fprodcom2  15703  eftlub  15827  divalgmod  16124  bitsval  16140  bitsp1e  16148  bitsp1o  16149  sadfval  16168  sadcp1  16171  sadval  16172  sadcadd  16174  sadadd2  16176  saddisjlem  16180  sadadd  16183  sadass  16187  smufval  16193  smuval  16197  smuval2  16198  smupvallem  16199  smu01lem  16201  smueqlem  16206  smumul  16209  bezoutlem2  16257  bezoutlem4  16259  algfx  16294  eucalgcvga  16300  reumodprminv  16514  nnnn0modprm0  16516  unbenlem  16618  prmreclem5  16630  vdwapval  16683  vdwapun  16684  vdwnnlem1  16705  vdwnn  16708  ramval  16718  0ram  16730  ramub1lem2  16737  prmgaplem7  16767  prmlem0  16816  elrest  17147  prdsbasmpt  17190  prdsleval  17197  prdsbasmpt2  17202  pwselbasb  17208  imasaddfnlem  17248  imasvscafn  17257  divsfval  17267  ismre  17308  mreunirn  17319  mrisval  17348  ismri  17349  isacs  17369  catidd  17398  iscatd2  17399  ismon  17454  isepi  17461  sectffval  17471  sectfval  17472  dfiso2  17493  cicsym  17525  issubc  17559  catsubcat  17563  isfunc  17588  funcres  17620  funcpropd  17625  ffthiso  17654  isnat  17672  isnat2  17673  fuciso  17702  initoval  17717  termoval  17718  isinito  17720  istermo  17721  iszeroo  17722  isinitoi  17723  istermoi  17724  initoid  17725  termoid  17726  iszeroi  17733  2initoinv  17734  initoeu1  17735  initoeu2  17740  2termoinv  17741  termoeu1  17742  arwhoma  17769  elsetchom  17805  setcmon  17811  setcepi  17812  setciso  17815  catciso  17835  elestrchom  17853  estrcbasbas  17856  funcestrcsetclem7  17872  funcestrcsetclem8  17873  funcestrcsetclem9  17874  fthestrcsetc  17876  fullestrcsetc  17877  equivestrcsetc  17878  setc1strwun  17879  funcsetcestrclem7  17887  funcsetcestrclem8  17888  funcsetcestrclem9  17889  fthsetcestrc  17891  fullsetcestrc  17892  hofcl  17986  hofpropd  17994  yonedalem4c  18004  yonedainv  18008  yonffthlem  18009  lubeldm  18080  glbeldm  18093  joindef  18103  meetdef  18117  poslubdg  18141  acsficl2d  18279  acsmapd  18281  psref  18301  psss  18307  dirge  18330  issstrmgm  18346  grpidval  18354  grpidpropd  18355  grpidd  18364  ismndd  18416  mndpropd  18419  imasmnd2  18431  imasmnd  18432  ismhm  18441  issubm  18451  gsumsgrpccat  18487  gsumccatOLD  18488  elefmndbas2  18522  smndex1mndlem  18557  imasgrp2  18699  imasgrp  18700  issubg  18764  subginv  18771  isnsg  18792  isghm  18843  resghm2b  18861  conjnmzb  18878  conjnsg  18879  ghmpropd  18881  isga  18906  elcntz  18937  elcntzsn  18940  cntzrcl  18942  resscntz  18947  symgextf1  19038  gsmsymgreqlem2  19048  f1otrspeq  19064  pmtrfrn  19075  pmtrdifellem3  19095  pmtrdifellem4  19096  psgnunilem1  19110  psgnunilem5  19111  psgnunilem2  19112  psgnunilem3  19113  psgneldm2  19121  psgnfitr  19134  psgnsn  19137  gexdvds  19198  gex1  19205  isslw  19222  sylow3lem2  19242  lsmelvalx  19254  pj1ghm  19318  efgtlen  19341  efgsfo  19354  efgredlemc  19360  frgp0  19375  frgpmhm  19380  qusabl  19475  frgpnabllem1  19483  cycsubmcmn  19498  0cyg  19503  cycsubgcyg  19511  gsumval3  19517  gsumcllem  19518  gsumzaddlem  19531  gsumzsplit  19537  gsummptfzcl  19579  eldprd  19616  dprdcntz2  19650  dprd2d2  19656  dmdprdsplit2lem  19657  dmdprdsplit2  19658  dprdsplit  19660  ablfac2  19701  isringd  19833  imasring  19867  dvdsrval  19896  isunit  19908  dvdsrpropd  19947  isirred  19950  isrhm  19974  isrim0  19976  drngunit  20005  isdrngd  20025  issubrg  20033  opprsubrg  20054  rhmpropd  20069  issdrg  20072  isabv  20088  issrngd  20130  islmod  20136  lmodprop2d  20194  islss  20205  islssd  20206  lssats2  20271  lspsnel  20274  islmhm  20298  lmhmf1o  20317  lmhmima  20318  lmhmpreima  20319  reslmhm  20323  pwssplit3  20332  lmhmpropd  20344  islbs  20347  lspprel  20365  lspfixed  20399  lbsacsbs  20427  lbsextlem1  20429  lbsextlem2  20430  lbsextlem3  20431  lbsextlem4  20432  ixpsnbasval  20489  lidlmcl  20497  quscrng  20520  islpidl  20526  lidldvgen  20535  zrhrhmb  20721  znf1o  20768  frgpcyg  20790  psgnevpmb  20801  isphld  20868  phlssphl  20873  elocv  20882  iscss  20897  isobs  20936  obs2ss  20945  dsmmfi  20954  dsmmelbas  20955  dsmmlss  20960  frlmelbas  20972  frlmlbs  21013  frlmup1  21014  ellspd  21018  islinds  21025  islindf2  21030  f1lindf  21038  islindf4  21054  assamulgscmlem2  21113  mplsubglem  21214  mpllsslem  21215  mplmonmul  21246  subrgascl  21283  subrgasclcl  21284  mpfind  21326  ismhp  21340  mhplss  21354  gsumply1subr  21414  lply1binomsc  21487  matbas2d  21581  matecl  21583  matvscl  21589  mat1  21605  mat0dim0  21625  mat0dimid  21626  mat0dimscm  21627  mat1dimelbas  21629  dmatel  21651  scmatel  21663  scmateALT  21670  scmataddcl  21674  scmatsubcl  21675  smatvscl  21682  scmatghm  21691  mat1scmat  21697  mdetunilem7  21776  mdetunilem9  21778  smadiadetr  21833  cramerimplem2  21842  cramer0  21848  pmatcoe1fsupp  21859  cpmatpmat  21868  cpmatel  21869  cpmatacl  21874  cpmatinvcl  21875  mat2pmatghm  21888  mat2pmatmul  21889  decpmatmullem  21929  pmatcollpwlem  21938  pmatcollpw3fi1lem1  21944  pmatcollpwscmatlem1  21947  monmat2matmon  21982  chfacfscmul0  22016  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  cayhamlem1  22024  cpmadugsumlemB  22032  cpmadugsumlemC  22033  cpmadugsumlemF  22034  cayhamlem2  22042  istopon  22070  eltg  22116  eltg2  22117  eltop  22133  eltop2  22134  eltop3  22135  pptbas  22167  iscld  22187  neiss2  22261  isnei  22263  neiptopnei  22292  neiptopreu  22293  lpfval  22298  lpval  22299  islp  22300  maxlp  22307  islpi  22309  neitr  22340  restlp  22343  ordtbas2  22351  ordtrest2  22364  lmfval  22392  cnfval  22393  iscn  22395  iscnp  22397  tgcn  22412  tgcnp  22413  lmbrf  22420  cnpresti  22448  ist1  22481  ist1-2  22507  cnt1  22510  haust1  22512  cmpfi  22568  cmpfii  22569  1stcfb  22605  2ndc1stc  22611  1stcrest  22613  2ndcdisj  22616  1stcelcls  22621  nllyi  22635  subislly  22641  islocfin  22677  lfinpfin  22684  locfindis  22690  locfincf  22691  comppfsc  22692  kgenval  22695  elkgen  22696  kgencn2  22717  txbas  22727  eltx  22728  ptval  22730  ptpjpre1  22731  ptopn2  22744  ptpjopn  22772  ptclsg  22775  xkoccn  22779  txdis  22792  txdis1cn  22795  ptrescn  22799  hausdiag  22805  hauseqlcld  22806  txhaus  22807  xkohaus  22813  elqtop  22857  qtopeu  22876  kqcldsat  22893  hmeofval  22918  ptuncnv  22967  ptunhmeo  22968  elmptrab  22987  fbdmn0  22994  elfg  23031  elfilss  23036  filunirn  23042  fixufil  23082  elfm  23107  rnelfmlem  23112  rnelfm  23113  fmfnfmlem4  23117  elflim2  23124  flimtopon  23130  elflim  23131  hausflim  23141  flimcls  23145  flfnei  23151  isflf  23153  hausflf  23157  cnpflf  23161  cnflf  23162  txflf  23166  isfcls  23169  fclstopon  23172  isfcls2  23173  fclssscls  23178  fclsnei  23179  fclsfnflim  23187  flimfnfcls  23188  isfcf  23194  fcfelbas  23196  cnpfcf  23201  cnfcf  23202  flfcntr  23203  alexsublem  23204  alexsubALTlem3  23209  cnextfun  23224  cnextfvval  23225  cnextf  23226  cnextcn  23227  tmdgsum2  23256  tgpconncomp  23273  ghmcnp  23275  qustgplem  23281  eltsms  23293  haustsms  23296  tsmsgsum  23299  tsmssubm  23303  tsmssplit  23312  isust  23364  elrnust  23385  ustbas  23388  elutop  23394  ustuqtoplem  23400  ustuqtop4  23405  ustuqtop  23407  utopsnneiplem  23408  utopsnneip  23409  utopsnnei  23410  isusp  23422  isucn  23439  ucncn  23446  iscfilu  23449  neipcfilu  23457  iscusp  23460  cnextucn  23464  ispsmet  23466  ismet  23485  isxmet  23486  elblps  23549  elbl  23550  elmopn  23604  prdsbl  23656  neibl  23666  met1stc  23686  metrest  23689  prdsxmslem2  23694  txmetcnp  23712  txmetcn  23713  metuval  23714  metustsym  23720  cfilucfil2  23726  elbl4  23728  metuel  23729  psmetutop  23732  restmetu  23735  metucn  23736  tngngp  23827  isnmhm  23919  zcld  23985  metnrmlem1a  24030  elcncf  24061  cncfcnvcn  24097  cnheibor  24127  lebnumlem1  24133  ishtpy  24144  isphtpy  24153  om1elbas  24204  elpi1  24217  pi1xfr  24227  pi1coghm  24233  tcphcph  24410  lmmbrf  24435  iscfil  24438  iscau  24449  iscauf  24453  caucfil  24456  iscmet  24457  cmetcaulem  24461  iscmet3lem1  24464  iscmet3lem2  24465  iscmet3  24466  bcthlem1  24497  cmsss  24524  cmetcusp1  24526  cmetcusp  24527  cmscsscms  24546  rrxcph  24565  minveclem3b  24601  ovolfioo  24640  ovolficc  24641  ovolctb  24663  ovoliunnul  24680  ovolshftlem1  24682  sca2rab  24685  ovolscalem1  24686  ovolicc2lem1  24690  ovolicc2lem2  24691  ovolicc2lem4  24693  ovolicc2lem5  24694  iundisj  24721  iunmbl2  24730  uniioombllem3  24758  vitalilem2  24782  vitalilem3  24783  mbfss  24819  i1faddlem  24866  i1fmullem  24867  mbfi1fseqlem2  24890  mbfi1fseqlem4  24892  mbfi1fseq  24895  itg2splitlem  24922  itg2split  24923  itg2monolem1  24924  itg2gt0  24934  isibl  24939  iblss2  24979  itgss3  24988  itgsplit  25009  ellimc  25046  limcmo  25055  cnlimc  25061  limciun  25067  limcun  25068  eldv  25071  dvbsss  25075  dvreslem  25082  elcpn  25107  dvaddf  25115  dvmulf  25116  dvcof  25121  rolle  25163  dvlip2  25168  dvivthlem1  25181  lhop1  25187  lhop2  25188  ftc1cn  25216  fta1glem2  25340  plyco0  25362  elply  25365  ply1termlem  25373  eltayl  25528  tayl0  25530  taylplem1  25531  taylplem2  25532  dvtaylp  25538  taylthlem1  25541  taylthlem2  25542  abelth  25609  cxpcn3  25910  rlimcnp  26124  fsumharmonic  26170  dchrelbas  26393  pntrsumbnd2  26724  ostth2lem2  26791  istrkgb  26825  istrkgcb  26826  istrkge  26827  istrkgl  26828  istrkgld  26829  axtgsegcon  26834  axtg5seg  26835  axtgbtwnid  26836  axtgpasch  26837  axtgupdim2  26841  axtgeucl  26842  tgdim01  26877  iscgrg  26882  isismt  26904  tglnunirn  26918  tglngval  26921  tgellng  26923  legval  26954  legov  26955  legov2  26956  ishlg  26972  mirreu3  27024  mirval  27025  mirfv  27026  mircgr  27027  mirbtwn  27028  ismir  27029  mireq  27035  symquadlem  27059  israg  27067  perpln1  27080  perpln2  27081  isperp  27082  islnopp  27109  outpasch  27125  ishpg  27129  iscgra  27179  dfcgra2  27200  isinag  27208  isleag  27217  iseqlg  27237  f1otrgitv  27240  f1otrg  27241  f1otrge  27242  ttgval  27245  ttgvalOLD  27246  ttgelitv  27259  elee  27271  brbtwn  27276  brcgr  27277  axlowdimlem16  27334  ebtwntg  27359  elntg2  27362  upgrex  27471  edgupgr  27513  upgredg  27516  edglnl  27522  numedglnl  27523  uhgr2edg  27584  umgr2edg1  27587  usgredg2vlem1  27601  usgredg2vlem2  27602  ushgredgedg  27605  ushgredgedgloop  27607  uhgrspansubgrlem  27666  fusgrfisstep  27705  nbgrval  27712  nbgrel  27716  nbupgrel  27721  nbgr2vtx1edg  27726  nbuhgr2vtx1edgblem  27727  nbuhgr2vtx1edgb  27728  nbusgreledg  27729  usgrnbcnvfv  27741  uvtxval  27763  uvtxel  27764  uvtx01vtx  27773  uvtxusgrel  27779  nbcplgr  27810  cplgr3v  27811  cusgrexi  27819  structtocusgr  27822  vtxdgfval  27843  vtxdg0v  27849  vtxdeqd  27853  vtxdun  27857  1loopgrnb0  27878  1loopgrvd0  27880  1hevtxdg0  27881  1hevtxdg1  27882  1egrvtxdg1  27885  umgr2v2evtxel  27898  umgr2v2enb1  27902  umgr2v2evd2  27903  vtxdginducedm1lem4  27918  vtxdginducedm1  27919  finsumvtxdg2sstep  27925  ewlksfval  27977  isewlk  27978  wksfval  27985  iswlk  27986  uspgr2wlkeq  28022  wlkres  28047  usgr2pthlem  28140  clwlkcompim  28157  uspgrn2crct  28182  wwlks  28209  iswwlksn  28212  wwlknvtx  28219  wlkiswwlks2  28249  wwlksm1edg  28255  wwlksnred  28266  wwlksnext  28267  wwlksnredwwlkn  28269  wwlksnredwwlkn0  28270  wwlksnwwlksnon  28289  wspn0  28298  usgr2wspthons3  28338  rusgrnumwwlkb0  28345  clwwlk  28356  clwwlkccatlem  28362  clwlkclwwlklem2a4  28370  clwlkclwwlk  28375  clwwisshclwwslem  28387  clwwlkinwwlk  28413  clwwlkel  28419  clwwlkf  28420  clwwlkext2edg  28429  wwlksext2clwwlk  28430  wwlksubclwwlk  28431  clwwnisshclwwsn  28432  eleclclwwlknlem2  28434  erclwwlknsym  28443  erclwwlkntr  28444  umgrhashecclwwlk  28451  clwwlkvbij  28486  eupth2lem3lem3  28603  eupth2lem3lem4  28604  eupth2lem3lem6  28606  eupth2lemb  28610  eucrct2eupth  28618  fusgreg2wsplem  28706  2clwwlklem  28716  2clwwlk2clwwlklem  28719  2clwwlkel  28722  2clwwlk2clwwlk  28723  extwwlkfabel  28726  clwwlknonclwlknonf1o  28735  dlwwlknondlwlknonf1olem1  28737  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  ex-res  28814  isssp  29095  sspn  29107  islno  29124  isblo  29153  nmlno0  29166  ishmo  29182  dipdir  29213  dipass  29216  ubthlem1  29241  ubthlem2  29242  htthlem  29288  htth  29289  ocel  29652  ocnel  29669  shsel  29685  shsel2  29693  shmodsi  29760  pjhtheu  29765  pjeq  29770  axpjpj  29791  pjoc2  29810  elspani  29914  h1de2ctlem  29926  elspansn  29937  elspansn2  29938  elnlfn  30299  eleigvec  30328  riesz3i  30433  cbviunf  30904  iuneq12daf  30905  iunrdx  30912  iunrnmptss  30914  cbvdisjf  30919  disjorf  30927  disjabrex  30930  disjabrexf  30931  iundisjf  30937  disjrdx  30939  elimampt  30982  2ndresdju  30995  abfmpunirn  30998  abfmpeld  31000  abfmpel  31001  fmptcof2  31003  acunirnmpt2  31006  acunirnmpt2f  31007  aciunf1lem  31008  funcnvmpt  31013  suppss3  31068  fpwrelmap  31077  xrofsup  31099  iundisjfi  31126  eliccioo  31214  s3f1  31230  ccatf1  31232  swrdrn3  31236  ismnt  31270  mgcoval  31273  gsummpt2co  31317  gsumpart  31324  gsumhashmul  31325  xrge0tsmsbi  31327  cycpmco2  31409  cyc3co2  31416  inftmrel  31443  isinftm  31444  isslmd  31464  rngurd  31491  resv1r  31550  eqg0el  31566  ellspds  31573  lbslsp  31581  rhmimaidl  31618  isprmidl  31622  qsidomlem1  31637  qsidomlem2  31638  ismxidl  31643  isrprm  31674  dimpropd  31701  lbslsat  31708  extdg1id  31747  smatrcl  31755  smatcl  31761  ist0cld  31792  txomap  31793  locfinreflem  31799  zarclsiin  31830  zart0  31838  rhmpreimacnlem  31843  metidval  31849  pstmval  31854  cnre2csqima  31870  ordtrest2NEW  31882  fmcncfil  31890  fsumcvg4  31909  ofcfval  32075  measvuni  32191  meascnbl  32196  faeval  32223  ismbfm  32228  elunirnmbfm  32229  isanmbfm  32232  imambfm  32238  elcarsg  32281  itgeq12dv  32302  issibf  32309  eulerpartlems  32336  eulerpartlemgc  32338  eulerpartlemgvv  32352  eulerpartlemgu  32353  eulerpart  32358  rrvmbfm  32418  elorvc  32435  elorrvc  32439  dstfrvunirn  32450  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemsima  32491  ballotlemrv  32495  fzssfzo  32527  signstfvn  32557  signstfvneq0  32560  signstres  32563  repr0  32600  reprinrn  32607  reprdifc  32616  hgt750lemg  32643  hgt750lemb  32645  istrkg2d  32655  axtgupdim2ALTV  32657  afsval  32660  brafs  32661  bnj945  32762  bnj1400  32824  bnj18eq1  32916  bnj916  32922  bnj1014  32950  bnj1015  32951  bnj1110  32971  bnj1417  33030  revpfxsfxrev  33086  cplgredgex  33091  pfxwlk  33094  revwlk  33095  subfacp1lem2b  33152  subfacp1lem4  33154  subfacp1lem5  33155  subfacp1lem6  33156  ptpconn  33204  cvmscbv  33229  iscvm  33230  cvmsi  33236  cvmsval  33237  cvmliftmolem1  33252  cvmlift2lem12  33285  cvmlift2lem13  33286  cvmlift3lem7  33296  snmlval  33302  satfv1  33334  satfvsucsuc  33336  satfrnmapom  33341  satf0op  33348  satf0n0  33349  sat1el2xp  33350  fmlafvel  33356  isfmlasuc  33359  fmlaomn0  33361  gonan0  33363  goaln0  33364  gonar  33366  goalr  33368  satffunlem1lem2  33374  satffunlem2lem2  33377  satfv0fvfmla0  33384  satef  33387  satefvfmla0  33389  sategoelfvb  33390  satfv1fvfmla1  33394  mrsubfval  33479  mrsubvrs  33493  mclsrcl  33532  mclsval  33534  mppsval  33543  mclsppslem  33554  opelco3  33758  xpord2ind  33803  xpord3ind  33809  wsuclem  33828  nolesgn2ores  33884  nogesgn1ores  33886  nosupprefixmo  33912  noinfprefixmo  33913  nosupcbv  33914  nosupdm  33916  nosupfv  33918  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1lem3  33922  nosupbnd1lem5  33924  nosupbnd2lem1  33927  noinfcbv  33929  noinfdm  33931  noinffv  33933  noinfres  33934  noinfbnd1lem1  33935  noinfbnd1lem3  33937  noinfbnd1lem5  33939  noinfbnd2lem1  33942  elmade  34060  elold  34062  ssltleft  34063  ssltright  34064  oldlim  34078  madebday  34089  newbday  34091  sltlpss  34096  cofcutr  34101  cofcutrtime  34102  lrrecval  34105  lrrecval2  34106  addsval  34135  funtransport  34342  fvtransport  34343  brcolinear  34370  colineardim1  34372  funray  34451  fvray  34452  funline  34453  fvline  34455  lineelsb2  34459  fwddifval  34473  fwddifnval  34474  rankelg  34479  rankeq1o  34482  elhf2  34486  0hf  34488  neibastop2lem  34558  neibastop3  34560  eltail  34572  bj-projeq  35191  bj-projval  35195  bj-restsn  35262  opelopabbv  35323  brabd0  35327  bj-eldiag  35356  bj-eldiag2  35357  mptsnunlem  35518  dissneqlem  35520  iooelexlt  35542  relowlssretop  35543  rdgellim  35556  exrecfnlem  35559  finxpeq1  35566  finxpreclem6  35576  pibp21  35595  curf  35764  uncf  35765  curunc  35768  unccur  35769  fin2so  35773  lindsadd  35779  lindsdom  35780  lindsenlbs  35781  matunitlindflem1  35782  matunitlindflem2  35783  matunitlindf  35784  ptrest  35785  ptrecube  35786  poimirlem2  35788  poimirlem8  35794  poimirlem17  35803  poimirlem18  35804  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem24  35810  poimirlem26  35812  poimirlem29  35815  heicant  35821  mblfinlem1  35823  mblfinlem2  35824  volsupnfl  35831  itg2addnclem  35837  itg2gt0cn  35841  indexdom  35901  incsequz  35915  istotbnd  35936  istotbnd3  35938  0totbnd  35940  sstotbnd  35942  sstotbnd3  35943  isbnd  35947  prdstotbnd  35961  cntotbnd  35963  isismty  35968  heibor1lem  35976  heiborlem2  35979  heiborlem3  35980  heibor  35988  isass  36013  exidcl  36043  exidreslem  36044  elghomlem2OLD  36053  rngoidmlem  36103  rngo1cl  36106  divrngcl  36124  isdrngo2  36125  isrngohom  36132  isrngoiso  36145  isriscg  36151  iscom2  36162  iscringd  36165  isidl  36181  ispridl  36201  ismaxidl  36207  ac6s6  36339  dmecd  36447  releldmqs  36777  releldmqscoss  36779  erim2  36796  prter3  36903  islshp  37000  islsat  37012  lcvfbr  37041  islfl  37081  ellkr  37110  islshpkrN  37141  ldual1dim  37187  isopos  37201  cmtfvalN  37231  cvrfval  37289  isat  37307  islln  37527  islpln  37551  islvol  37594  isline  37760  ispointN  37763  ispsubsp  37766  elpmap  37779  elpmapat  37785  elpadd  37820  paddclN  37863  elpclN  37913  elpcliN  37914  pclfinN  37921  pclcmpatN  37922  ispsubclN  37958  iswatN  38015  islhp  38017  islaut  38104  ispautN  38120  isldil  38131  isltrn  38140  isdilN  38175  istrnN  38178  istendo  38781  dvhb1dimN  39007  erng1lem  39008  erngdvlem4-rN  39020  diaelval  39054  diaeldm  39057  dia1dimid  39084  cdlemm10N  39139  dibopelvalN  39164  dibopelval2  39166  dibelval3  39168  dibelval1st  39170  dibelval2nd  39173  dibeldmN  39179  dibvalrel  39184  dibglbN  39187  dicffval  39195  dicfval  39196  dicopelval  39198  dicelvalN  39199  dicelval3  39201  dicvalrelN  39206  dicelval1sta  39208  diclspsn  39215  dihopelvalbN  39259  dihopelvalcqat  39267  dihopelvalcpre  39269  dihvalrel  39300  dih1  39307  dihmeetlem4preN  39327  dihmeetlem13N  39340  dih1dimatlem  39350  dochnel2  39413  dihjatcclem4  39442  dvh2dim  39466  dvh3dim  39467  dvh4dimN  39468  dochfln0  39498  lpolsetN  39503  islpolN  39504  lcfrvalsnN  39562  lcfrlem21  39584  lcfrlem27  39590  lcfrlem37  39600  lcfr  39606  lcdlss  39640  mapdcv  39681  hdmap1fval  39817  hdmapffval  39847  hdmapfval  39848  hdmapval  39849  hgmapffval  39906  hgmapfval  39907  hdmapellkr  39935  hlhilhillem  39985  fzsplitnd  39998  sticksstones11  40119  sticksstones12a  40120  fzosumm1  40225  frlmfielbas  40238  frlmsnic  40270  mhphf  40292  isnacs  40533  mrefg2  40536  elmzpcl  40555  mzpcompact2  40581  eldiophb  40586  elpell1qr  40676  elpell14qr  40678  elpell1234qr  40680  pw2f1ocnv  40866  pw2f1o2val2  40869  aomclem4  40889  aomclem6  40891  islssfg2  40903  imasgim  40932  lnr2i  40948  elmnc  40968  rngunsnply  41005  fiinfi  41187  sqrtcvallem1  41246  elintima  41268  eliunov2  41294  ov2ssiunov2  41315  brtrclfv2  41342  rfovcnvf1od  41619  rfovcnvfvd  41622  fsovrfovd  41624  fsovfvd  41625  fsovcnvlem  41628  ntrclsfv1  41672  ntrclselnel1  41674  ntrclsneine0lem  41681  ntrneifv1  41696  ntrneifv2  41697  ntrneiel  41698  gneispace2  41749  gneispacess2  41763  extoimad  41782  mnringelbased  41839  dvconstbi  41959  bccbc  41970  eliin2f  42661  rabbida2  42688  disjinfi  42738  unirnmap  42755  elmptima  42811  iuneqfzuzlem  42880  iooiinioc  43101  fsumiunss  43123  fsumsupp0  43126  lptre2pt  43188  icccncfext  43435  cncfiooicclem1  43441  dvnprodlem2  43495  stoweidlem27  43575  stoweidlem29  43577  stoweidlem31  43579  stoweidlem34  43582  stoweidlem48  43596  stoweidlem59  43607  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem2  43657  fourierdlem3  43658  fourierdlem25  43680  fourierdlem32  43687  fourierdlem33  43688  fourierdlem41  43696  fourierdlem48  43702  fourierdlem49  43703  fourierdlem62  43716  fourierdlem70  43724  fourierdlem80  43734  fourierdlem92  43746  fourierdlem93  43747  fourierdlem101  43755  etransclem37  43819  sge0val  43911  sge0f1o  43927  sge0iunmptlemre  43960  sge0iunmpt  43963  iundjiun  44005  caragenel  44040  ovncvrrp  44109  ovnsubaddlem1  44115  ovnsubadd  44117  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  hoidmvle  44145  ovncvr2  44156  hspdifhsp  44161  hoiqssbl  44170  hspmbllem2  44172  hspmbl  44174  opnvonmbllem1  44177  isvonmbl  44183  ovnovollem1  44201  issmflem  44272  smflimlem3  44318  smflimlem4  44319  smflim  44322  smfmullem2  44337  smflimmpt  44354  smfsuplem1  44355  smflimsuplem1  44364  smflimsuplem3  44366  smflimsuplem4  44367  smflimsuplem7  44370  smflimsup  44372  fcores  44572  fcoresf1  44574  afvelrnb  44666  afvelrnb0  44667  afv2co2  44760  el1fzopredsuc  44828  iccpart  44879  iccpartgtprec  44883  iccpartiltu  44885  iccpartigtl  44886  iccpartltu  44888  iccpartgtl  44889  iccpartgt  44890  iccpartleu  44891  iccpartgel  44892  iccelpart  44896  iccpartiun  44897  icceuelpart  44899  fargshiftfv  44902  fargshiftfo  44905  sprel  44947  prprelb  44979  prprelprb  44980  fpprel  45191  sbgoldbo  45250  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  bgoldbtbndlem3  45270  bgoldbtbnd  45272  upwlksfval  45308  isupwlk  45309  mgmpropd  45340  ismgmhm  45348  issubmgm  45354  intop  45408  isclintop  45412  assintop  45414  isassintop  45415  assintopcllaw  45417  isrnghm  45461  isrngisom  45465  c0ghm  45480  c0snghm  45485  uzlidlring  45498  rnghmresel  45533  elrngchom  45537  rnghmsubcsetclem1  45544  rnghmsubcsetclem2  45545  rngcid  45548  rngcsect  45549  rngciso  45551  elrngchomALTV  45555  rngccatidALTV  45558  rngcsectALTV  45561  rngcisoALTV  45563  funcrngcsetcALT  45568  zrinitorngc  45569  zrtermorngc  45570  rhmresel  45579  elringchom  45583  rhmsubcsetclem1  45590  rhmsubcsetclem2  45591  ringcid  45594  rhmsscrnghm  45595  rhmsubcrngclem1  45596  rhmsubcrngclem2  45597  ringcsect  45600  ringciso  45602  ringcbasbas  45603  funcringcsetcALTV2lem7  45611  funcringcsetcALTV2lem9  45613  elringchomALTV  45618  ringccatidALTV  45621  ringcsectALTV  45624  ringcisoALTV  45626  ringcbasbasALTV  45627  funcringcsetclem7ALTV  45634  funcringcsetclem9ALTV  45636  irinitoringc  45638  zrtermoringc  45639  srhmsubc  45645  rhmsubclem3  45657  rhmsubclem4  45658  srhmsubcALTV  45663  rhmsubcALTVlem3  45675  rhmsubcALTVlem4  45676  opeliun2xp  45679  cbvmpox2  45682  ply1sclrmsm  45735  dmatALTbasel  45754  lcoval  45764  lindslinindsimp1  45809  lindslinindsimp2  45815  lmod1  45844  elbigo  45908  elbigo2  45909  elbigolo1  45914  dig2nn0ld  45961  naryfvalel  45987  rrxlines  46090  rrxlinesc  46092  rrxlinec  46093  eenglngeehlnm  46096  elrrx2linest2  46102  rrxsphere  46105  itsclc0  46128  itsclc0b  46129  itsclinecirc0  46130  itsclinecirc0b  46131  itscnhlinecirc02p  46142  f1omo  46199  lubeldm2d  46263  glbeldm2d  46264  catprs  46303  isthinc  46313  isthincd2lem1  46319  thincmoALT  46322  thincmod  46323  isthincd  46329  prsthinc  46346  elsetrecslem  46415  tworepnotupword  46532