Theorem eleq2d 2811

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1531   = wceq 1533  ∃wex 1773   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-clel 2802

This theorem is referenced by:  eleq2  2814  eleq12d  2819  eleqtrd  2827  neleqtrd  2847  eqabrd  2868  nfceqdfOLD  2891  drnfc1OLD  2915  drnfc2OLD  2917  raleqbidv  3334  rexeqbidv  3335  elabd2  3652  sbcbid  3827  csbeq2d  3891  cbvcsbw  3895  cbvcsb  3896  csbie  3921  csbied  3923  csbie2g  3928  cbvralcsf  3930  cbvreucsf  3932  cbvrabcsf  3933  sbcel12  4400  sbcel1g  4405  sbcel2  4407  prel12g  4856  eliuni  4993  iuneqconst  4998  iuneq12df  5013  cbviun  5029  cbviin  5030  cbviung  5031  cbviing  5032  iinxsng  5081  iinxprg  5082  iunxsng  5083  iunxsngf  5085  cbvdisj  5113  disjor  5118  disjiund  5128  mpteq12da  5223  mpteq12dfOLD  5225  mpteq12f  5226  mpteq12dva  5227  axpweq  5338  rabxfrd  5405  rbropapd  5554  opeliunxp  5733  opeliunxp2  5828  iunxpf  5838  elrelimasn  6074  elimasngOLD  6079  elimasni  6080  xpdifid  6157  ressn  6274  predbrg  6312  funfni  6645  fnbr  6647  dffv3  6877  elfv2ex  6927  fvelrnb  6942  foelcdmi  6943  fvun1  6972  fvco2  6978  elfvmptrab1w  7014  elfvmptrab1  7015  elfvmptrab  7016  elpreima  7049  dff3  7091  fmptco  7119  fnelfp  7165  fnelnfp  7167  tpres  7194  fnprb  7201  fntpb  7202  funfvima3  7229  eluniima  7241  elunirn2OLD  7244  dff13  7246  f1eqcocnv  7291  f1eqcocnvOLD  7292  isoini  7327  riotaeqdv  7358  mpoeq123dva  7475  cbvmpox  7494  ovelrn  7576  elovmpo  7644  elovmporab  7645  elovmporab1w  7646  elovmporab1  7647  elovmpt3rab1  7659  fiun  7922  f1iun  7923  zfrep6  7934  fmpox  8046  el2mpocsbcl  8065  el2mpocl  8066  bropopvvv  8070  bropfvvvv  8072  xpord2indlem  8127  xpord3inddlem  8134  elsuppfng  8149  elsuppfn  8150  suppfnss  8168  opeliunxp2f  8190  mpoxopn0yelv  8193  mpoxopovel  8200  rntpos  8219  mpocurryd  8249  fpr2  8284  wfrdmclOLD  8312  wfrlem12OLD  8315  wfr2  8331  onoviun  8338  smoel  8355  smoiso  8357  smoel2  8358  smo11  8359  tfrlem9  8380  oalimcl  8555  oaass  8556  omordi  8561  omordlim  8572  omlimcl  8573  odi  8574  omeulem1  8577  omeulem2  8578  oen0  8581  oeordi  8582  oeordsuc  8589  oelimcl  8595  oeeulem  8596  oeeui  8597  nnmordi  8626  oaabs2  8643  omabs  8645  omsmolem  8651  ereldm  8746  iiner  8778  elmapg  8828  elpmg  8832  elixpsn  8926  ixpsnf1o  8927  boxriin  8929  omxpenlem  9068  pw2f1olem  9071  phplem2  9203  php3  9207  phplem4OLD  9215  php3OLD  9219  infn0  9302  elfi  9403  dffi3  9421  marypha2lem2  9426  ordiso2  9505  wemapsolem  9540  elharval  9551  inf3lemd  9617  inf3lem1  9618  inf3lem2  9619  inf3lem3  9620  cantnfs  9656  cantnfp1lem3  9670  cantnflem1b  9676  cantnflem1  9679  ttrclselem2  9716  trcl  9718  frr2  9750  r1sdom  9764  r1ordg  9768  r1pwss  9774  tz9.12lem3  9779  tz9.12  9780  r1elwf  9786  rankr1ai  9788  rankidb  9790  rankr1bg  9793  rankval2  9808  rankunb  9840  tcrank  9874  acni  10035  acni2  10036  acndom  10041  infpwfien  10052  alephnbtwn  10061  cardaleph  10079  cardinfima  10087  iunfictbso  10104  dfac3  10111  dfac5lem5  10117  dfac5  10118  dfac9  10126  dfac12r  10136  kmlem2  10141  kmlem12  10151  kmlem13  10152  kmlem14  10153  ackbij2lem3  10231  ackbij2  10233  cofsmo  10259  alephsing  10266  fin23lem30  10332  isf32lem9  10351  itunisuc  10409  axcc2lem  10426  axcc3  10428  domtriomlem  10432  axdc2lem  10438  axdc2  10439  axdc3lem2  10441  axdc3lem4  10443  axdc4lem  10445  ac6c4  10471  zorn2lem1  10486  ttukeylem6  10504  pwcfsdom  10573  axregndlem2  10593  axinfndlem1  10595  axacndlem4  10600  axacnd  10602  pwfseqlem1  10648  inar1  10765  inatsk  10768  gruurn  10788  grur1  10810  eltskm  10833  genpelv  10990  eluz1  12822  eluzaddOLD  12853  eluzsubOLD  12854  elixx1  13329  elixx3g  13333  elioo2  13361  elfz1  13485  elfz2  13487  elfzp1  13547  fzpr  13552  fzsuc2  13555  fzrev3  13563  elfzp12  13576  fzm1  13577  elfzo  13630  fz0add1fz1  13698  elfzo0l  13718  elfzom1b  13727  fzosplitsni  13739  elfzr  13741  elfzlmr  13742  zmodidfzo  13861  seqp1  13977  seqf1o  14005  bcval  14260  bcpasc  14277  hashf1lem1  14411  hashf1lem1OLD  14412  fundmge2nop0  14449  wrdmap  14492  elovmpowrd  14504  ccatfval  14519  elfzelfzccat  14526  ccatlid  14532  ccatass  14534  ccatrn  14535  ccatalpha  14539  swrdfv2  14607  ccatswrd  14614  swrdccat2  14615  pfxfv  14628  pfxeq  14642  ccatpfx  14647  swrdswrd  14651  swrdpfx  14653  pfxpfx  14654  cats1un  14667  swrdccatfn  14670  swrdccatin1  14671  pfxccatin12lem4  14672  pfxccatin12lem1  14674  swrdccatin2  14675  pfxccatin12lem2c  14676  pfxccatin12lem2  14677  swrdccat3blem  14685  swrdccatin1d  14689  swrdccatin2d  14690  pfxccatin12d  14691  revccat  14712  revrev  14713  repswpfx  14731  repswccat  14732  cshwidxmod  14749  2cshw  14759  cshwcshid  14774  cshwcsh2id  14775  cshimadifsn  14776  cshimadifsn0  14777  revco  14781  ccatco  14782  cshco  14783  swrdco  14784  ofccat  14912  shftfn  15016  shftval  15017  limsupgle  15417  ello12  15456  elo12  15467  isercolllem3  15609  sumeq1  15631  fsumsplit  15683  sumsplit  15710  fsum2dlem  15712  fsumcom2  15716  fsumparts  15748  explecnv  15807  pwdif  15810  fprodser  15889  fprodsplit  15906  fprod2dlem  15920  fprodcom2  15924  eftlub  16048  divalgmod  16345  bitsval  16361  bitsp1e  16369  bitsp1o  16370  sadfval  16389  sadcp1  16392  sadval  16393  sadcadd  16395  sadadd2  16397  saddisjlem  16401  sadadd  16404  sadass  16408  smufval  16414  smuval  16418  smuval2  16419  smupvallem  16420  smu01lem  16422  smueqlem  16427  smumul  16430  bezoutlem2  16478  bezoutlem4  16480  algfx  16513  eucalgcvga  16519  reumodprminv  16733  nnnn0modprm0  16735  unbenlem  16837  prmreclem5  16849  vdwapval  16902  vdwapun  16903  vdwnnlem1  16924  vdwnn  16927  ramval  16937  0ram  16949  ramub1lem2  16956  prmgaplem7  16986  prmlem0  17035  elrest  17369  prdsbasmpt  17412  prdsleval  17419  prdsbasmpt2  17424  pwselbasb  17430  imasaddfnlem  17470  imasvscafn  17479  divsfval  17489  ismre  17530  mreunirn  17541  mrisval  17570  ismri  17571  isacs  17591  catidd  17620  iscatd2  17621  ismon  17676  isepi  17683  sectffval  17693  sectfval  17694  dfiso2  17715  cicsym  17747  issubc  17781  catsubcat  17785  isfunc  17810  funcres  17842  funcpropd  17849  ffthiso  17878  isnat  17897  isnat2  17898  fuciso  17927  initoval  17942  termoval  17943  isinito  17945  istermo  17946  iszeroo  17947  isinitoi  17948  istermoi  17949  initoid  17950  termoid  17951  iszeroi  17958  2initoinv  17959  initoeu1  17960  initoeu2  17965  2termoinv  17966  termoeu1  17967  arwhoma  17994  elsetchom  18030  setcmon  18036  setcepi  18037  setciso  18040  catciso  18060  elestrchom  18078  estrcbasbas  18081  funcestrcsetclem7  18097  funcestrcsetclem8  18098  funcestrcsetclem9  18099  fthestrcsetc  18101  fullestrcsetc  18102  equivestrcsetc  18103  setc1strwun  18104  funcsetcestrclem7  18112  funcsetcestrclem8  18113  funcsetcestrclem9  18114  fthsetcestrc  18116  fullsetcestrc  18117  hofcl  18211  hofpropd  18219  yonedalem4c  18229  yonedainv  18233  yonffthlem  18234  lubeldm  18305  glbeldm  18318  joindef  18328  meetdef  18342  poslubdg  18366  acsficl2d  18504  acsmapd  18506  psref  18526  psss  18532  dirge  18555  mgmpropd  18571  issstrmgm  18573  grpidval  18581  grpidpropd  18582  grpidd  18591  ismgmhm  18616  issubmgm  18622  issgrpd  18650  sgrppropd  18651  ismndd  18676  mndpropd  18679  imasmnd2  18691  imasmnd  18692  xpsmnd0  18695  ismhm  18702  issubm  18715  gsumsgrpccat  18752  elefmndbas2  18786  smndex1mndlem  18821  imasgrp2  18970  imasgrp  18971  issubg  19038  subginv  19045  isnsg  19067  quselbas  19095  isghm  19126  resghm2b  19144  conjnmzb  19163  conjnsg  19164  ghmpropd  19166  isga  19192  elcntz  19223  elcntzsn  19226  cntzrcl  19228  resscntz  19234  symgextf1  19326  gsmsymgreqlem2  19336  f1otrspeq  19352  pmtrfrn  19363  pmtrdifellem3  19383  pmtrdifellem4  19384  psgnunilem1  19398  psgnunilem5  19399  psgnunilem2  19400  psgnunilem3  19401  psgneldm2  19409  psgnfitr  19422  psgnsn  19425  gexdvds  19489  gex1  19496  isslw  19513  sylow3lem2  19533  lsmelvalx  19545  pj1ghm  19608  efgtlen  19631  efgsfo  19644  efgredlemc  19650  frgp0  19665  frgpmhm  19670  qusabl  19770  frgpnabllem1  19778  imasabl  19781  cycsubmcmn  19794  0cyg  19798  cycsubgcyg  19806  gsumval3  19812  gsumcllem  19813  gsumzaddlem  19826  gsumzsplit  19832  gsummptfzcl  19874  eldprd  19911  dprdcntz2  19945  dprd2d2  19951  dmdprdsplit2lem  19952  dmdprdsplit2  19953  dprdsplit  19955  ablfac2  19996  isrngd  20063  rngpropd  20064  imasrng  20067  qusrng  20070  ringurd  20075  isringd  20175  imasring  20214  xpsring1d  20217  dvdsrval  20248  isunit  20260  dvdsrpropd  20303  isirred  20306  isrnghm  20328  isrngim  20332  c0ghm  20348  c0snghm  20351  isrhm  20365  isrim0OLD  20368  isrim0  20370  islring  20425  issubrng  20432  opprsubrng  20444  issubrg  20458  opprsubrg  20480  resrhm2b  20489  rhmpropd  20496  rnghmresel  20501  elrngchom  20505  rnghmsubcsetclem1  20512  rnghmsubcsetclem2  20513  rngcid  20516  rngcsect  20517  rngciso  20519  funcrngcsetcALT  20522  zrinitorngc  20523  zrtermorngc  20524  rhmresel  20530  elringchom  20534  rhmsubcsetclem1  20541  rhmsubcsetclem2  20542  ringcid  20545  rhmsscrnghm  20546  rhmsubcrngclem1  20547  rhmsubcrngclem2  20548  ringcsect  20551  ringciso  20553  ringcbasbas  20554  zrtermoringc  20556  srhmsubc  20561  rhmsubclem3  20568  rhmsubclem4  20569  drngunit  20577  isdrngd  20605  isdrngdOLD  20607  issdrg  20624  sdrgunit  20632  isabv  20647  issrngd  20689  islmod  20695  lmodprop2d  20755  islss  20766  islssd  20767  lssats2  20832  lspsnel  20835  islmhm  20860  lmhmf1o  20879  lmhmima  20880  lmhmpreima  20881  reslmhm  20885  pwssplit3  20894  lmhmpropd  20906  islbs  20909  lspprel  20927  lspfixed  20964  lbsacsbs  20992  lbsextlem1  20994  lbsextlem2  20995  lbsextlem3  20996  lbsextlem4  20997  ixpsnbasval  21049  isridlrng  21063  rnglidlmmgm  21088  isridl  21094  quscrng  21123  rngqiprngimfolem  21128  rngqiprngimf1lem  21132  rngqiprngimfo  21139  islpidl  21163  lidldvgen  21172  irinitoringc  21329  pzriprnglem13  21343  pzriprnglem14  21344  zrhrhmb  21360  znf1o  21407  frgpcyg  21429  psgnevpmb  21440  isphld  21507  phlssphl  21512  elocv  21521  iscss  21536  isobs  21575  obs2ss  21584  dsmmfi  21593  dsmmelbas  21594  dsmmlss  21599  frlmelbas  21611  frlmlbs  21652  frlmup1  21653  ellspd  21657  islinds  21664  islindf2  21669  f1lindf  21677  islindf4  21693  assamulgscmlem2  21754  psrgrp  21818  mplsubglem  21859  mpllsslem  21860  mplmonmul  21892  subrgascl  21928  subrgasclcl  21929  mpfind  21971  ismhp  21983  mhplss  21997  gsumply1subr  22066  lply1binomsc  22141  matbas2d  22235  matecl  22237  matvscl  22243  mat1  22259  mat0dim0  22279  mat0dimid  22280  mat0dimscm  22281  mat1dimelbas  22283  dmatel  22305  scmatel  22317  scmateALT  22324  scmataddcl  22328  scmatsubcl  22329  smatvscl  22336  scmatghm  22345  mat1scmat  22351  mdetunilem7  22430  mdetunilem9  22432  smadiadetr  22487  cramerimplem2  22496  cramer0  22502  pmatcoe1fsupp  22513  cpmatpmat  22522  cpmatel  22523  cpmatacl  22528  cpmatinvcl  22529  mat2pmatghm  22542  mat2pmatmul  22543  decpmatmullem  22583  pmatcollpwlem  22592  pmatcollpw3fi1lem1  22598  pmatcollpwscmatlem1  22601  monmat2matmon  22636  chfacfscmul0  22670  chfacfscmulgsum  22672  chfacfpmmulgsum  22676  cayhamlem1  22678  cpmadugsumlemB  22686  cpmadugsumlemC  22687  cpmadugsumlemF  22688  cayhamlem2  22696  istopon  22724  eltg  22770  eltg2  22771  eltop  22787  eltop2  22788  eltop3  22789  pptbas  22821  iscld  22841  neiss2  22915  isnei  22917  neiptopnei  22946  neiptopreu  22947  lpfval  22952  lpval  22953  islp  22954  maxlp  22961  islpi  22963  neitr  22994  restlp  22997  ordtbas2  23005  ordtrest2  23018  lmfval  23046  cnfval  23047  iscn  23049  iscnp  23051  tgcn  23066  tgcnp  23067  lmbrf  23074  cnpresti  23102  ist1  23135  ist1-2  23161  cnt1  23164  haust1  23166  cmpfi  23222  cmpfii  23223  1stcfb  23259  2ndc1stc  23265  1stcrest  23267  2ndcdisj  23270  1stcelcls  23275  nllyi  23289  subislly  23295  islocfin  23331  lfinpfin  23338  locfindis  23344  locfincf  23345  comppfsc  23346  kgenval  23349  elkgen  23350  kgencn2  23371  txbas  23381  eltx  23382  ptval  23384  ptpjpre1  23385  ptopn2  23398  ptpjopn  23426  ptclsg  23429  xkoccn  23433  txdis  23446  txdis1cn  23449  ptrescn  23453  hausdiag  23459  hauseqlcld  23460  txhaus  23461  xkohaus  23467  elqtop  23511  qtopeu  23530  kqcldsat  23547  hmeofval  23572  ptuncnv  23621  ptunhmeo  23622  elmptrab  23641  fbdmn0  23648  elfg  23685  elfilss  23690  filunirn  23696  fixufil  23736  elfm  23761  rnelfmlem  23766  rnelfm  23767  fmfnfmlem4  23771  elflim2  23778  flimtopon  23784  elflim  23785  hausflim  23795  flimcls  23799  flfnei  23805  isflf  23807  hausflf  23811  cnpflf  23815  cnflf  23816  txflf  23820  isfcls  23823  fclstopon  23826  isfcls2  23827  fclssscls  23832  fclsnei  23833  fclsfnflim  23841  flimfnfcls  23842  isfcf  23848  fcfelbas  23850  cnpfcf  23855  cnfcf  23856  flfcntr  23857  alexsublem  23858  alexsubALTlem3  23863  cnextfun  23878  cnextfvval  23879  cnextf  23880  cnextcn  23881  tmdgsum2  23910  tgpconncomp  23927  ghmcnp  23929  qustgplem  23935  eltsms  23947  haustsms  23950  tsmsgsum  23953  tsmssubm  23957  tsmssplit  23966  isust  24018  ustbas  24042  elutop  24048  ustuqtoplem  24054  ustuqtop4  24059  ustuqtop  24061  utopsnneiplem  24062  utopsnneip  24063  utopsnnei  24064  isusp  24076  isucn  24093  ucncn  24100  iscfilu  24103  neipcfilu  24111  iscusp  24114  cnextucn  24118  ispsmet  24120  ismet  24139  isxmet  24140  elblps  24203  elbl  24204  elmopn  24258  prdsbl  24310  neibl  24320  met1stc  24340  metrest  24343  prdsxmslem2  24348  txmetcnp  24366  txmetcn  24367  metustsym  24374  cfilucfil2  24380  elbl4  24382  metuel  24383  psmetutop  24386  restmetu  24389  metucn  24390  tngngp  24481  isnmhm  24573  zcld  24639  metnrmlem1a  24684  elcncf  24719  cncfcnvcn  24756  cnheibor  24791  lebnumlem1  24797  ishtpy  24808  isphtpy  24817  om1elbas  24869  elpi1  24882  pi1xfr  24892  pi1coghm  24898  tcphcph  25075  lmmbrf  25100  iscfil  25103  iscau  25114  iscauf  25118  caucfil  25121  iscmet  25122  cmetcaulem  25126  iscmet3lem1  25129  iscmet3lem2  25130  iscmet3  25131  bcthlem1  25162  cmsss  25189  cmetcusp1  25191  cmetcusp  25192  cmscsscms  25211  rrxcph  25230  minveclem3b  25266  ovolfioo  25306  ovolficc  25307  ovolctb  25329  ovoliunnul  25346  ovolshftlem1  25348  sca2rab  25351  ovolscalem1  25352  ovolicc2lem1  25356  ovolicc2lem2  25357  ovolicc2lem4  25359  ovolicc2lem5  25360  iundisj  25387  iunmbl2  25396  uniioombllem3  25424  vitalilem2  25448  vitalilem3  25449  mbfss  25485  i1faddlem  25532  i1fmullem  25533  mbfi1fseqlem2  25556  mbfi1fseqlem4  25558  mbfi1fseq  25561  itg2splitlem  25588  itg2split  25589  itg2monolem1  25590  itg2gt0  25600  isibl  25605  iblss2  25645  itgss3  25654  itgsplit  25675  ellimc  25712  limcmo  25721  cnlimc  25727  limciun  25733  limcun  25734  eldv  25737  dvbsss  25741  dvreslem  25748  elcpn  25774  dvaddf  25783  dvmulf  25784  dvcof  25790  rolle  25832  dvlip2  25838  dvivthlem1  25851  lhop1  25857  lhop2  25858  ftc1cn  25888  fta1glem2  26012  plyco0  26034  elply  26037  ply1termlem  26045  eltayl  26201  tayl0  26203  taylplem1  26204  taylplem2  26205  dvtaylp  26211  taylthlem1  26214  taylthlem2  26215  abelth  26283  cxpcn3  26587  rlimcnp  26801  fsumharmonic  26848  dchrelbas  27073  pntrsumbnd2  27404  ostth2lem2  27471  nolesgn2ores  27509  nogesgn1ores  27511  nosupprefixmo  27537  noinfprefixmo  27538  nosupcbv  27539  nosupdm  27541  nosupfv  27543  nosupres  27544  nosupbnd1lem1  27545  nosupbnd1lem3  27547  nosupbnd1lem5  27549  nosupbnd2lem1  27552  noinfcbv  27554  noinfdm  27556  noinffv  27558  noinfres  27559  noinfbnd1lem1  27560  noinfbnd1lem3  27562  noinfbnd1lem5  27564  noinfbnd2lem1  27567  elmade  27698  elold  27700  ssltleft  27701  ssltright  27702  oldlim  27717  madebday  27730  newbday  27732  sltlpss  27737  cofcutr  27748  cofcutrtime  27751  lrrecval  27760  lrrecval2  27761  addsval  27783  precsexlem9  28017  precsexlem11  28019  sltonold  28057  istrkgb  28130  istrkgcb  28131  istrkge  28132  istrkgl  28133  istrkgld  28134  axtgsegcon  28139  axtg5seg  28140  axtgbtwnid  28141  axtgpasch  28142  axtgupdim2  28146  axtgeucl  28147  tgdim01  28182  iscgrg  28187  isismt  28209  tglnunirn  28223  tglngval  28226  tgellng  28228  legval  28259  legov  28260  legov2  28261  ishlg  28277  mirreu3  28329  mirval  28330  mirfv  28331  mircgr  28332  mirbtwn  28333  ismir  28334  mireq  28340  symquadlem  28364  israg  28372  perpln1  28385  perpln2  28386  isperp  28387  islnopp  28414  outpasch  28430  ishpg  28434  iscgra  28484  dfcgra2  28505  isinag  28513  isleag  28522  iseqlg  28542  f1otrgitv  28545  f1otrg  28546  f1otrge  28547  ttgval  28550  ttgvalOLD  28551  ttgelitv  28564  elee  28576  brbtwn  28581  brcgr  28582  axlowdimlem16  28639  ebtwntg  28664  elntg2  28667  upgrex  28776  edgupgr  28818  upgredg  28821  edglnl  28827  numedglnl  28828  uhgr2edg  28889  umgr2edg1  28892  usgredg2vlem1  28906  usgredg2vlem2  28907  ushgredgedg  28910  ushgredgedgloop  28912  uhgrspansubgrlem  28971  fusgrfisstep  29010  nbgrval  29017  nbgrel  29021  nbupgrel  29026  nbgr2vtx1edg  29031  nbuhgr2vtx1edgblem  29032  nbuhgr2vtx1edgb  29033  nbusgreledg  29034  usgrnbcnvfv  29046  uvtxval  29068  uvtxel  29069  uvtx01vtx  29078  uvtxusgrel  29084  nbcplgr  29115  cplgr3v  29116  cusgrexi  29124  structtocusgr  29127  vtxdgfval  29148  vtxdg0v  29154  vtxdeqd  29158  vtxdun  29162  1loopgrnb0  29183  1loopgrvd0  29185  1hevtxdg0  29186  1hevtxdg1  29187  1egrvtxdg1  29190  umgr2v2evtxel  29203  umgr2v2enb1  29207  umgr2v2evd2  29208  vtxdginducedm1lem4  29223  vtxdginducedm1  29224  finsumvtxdg2sstep  29230  ewlksfval  29282  isewlk  29283  wksfval  29290  iswlk  29291  uspgr2wlkeq  29327  wlkres  29351  usgr2pthlem  29444  clwlkcompim  29461  uspgrn2crct  29486  wwlks  29513  iswwlksn  29516  wwlknvtx  29523  wlkiswwlks2  29553  wwlksm1edg  29559  wwlksnred  29570  wwlksnext  29571  wwlksnredwwlkn  29573  wwlksnredwwlkn0  29574  wwlksnwwlksnon  29593  wspn0  29602  usgr2wspthons3  29642  rusgrnumwwlkb0  29649  clwwlk  29660  clwwlkccatlem  29666  clwlkclwwlklem2a4  29674  clwlkclwwlk  29679  clwwisshclwwslem  29691  clwwlkinwwlk  29717  clwwlkel  29723  clwwlkf  29724  clwwlkext2edg  29733  wwlksext2clwwlk  29734  wwlksubclwwlk  29735  clwwnisshclwwsn  29736  eleclclwwlknlem2  29738  erclwwlknsym  29747  erclwwlkntr  29748  umgrhashecclwwlk  29755  clwwlkvbij  29790  eupth2lem3lem3  29907  eupth2lem3lem4  29908  eupth2lem3lem6  29910  eupth2lemb  29914  eucrct2eupth  29922  fusgreg2wsplem  30010  2clwwlklem  30020  2clwwlk2clwwlklem  30023  2clwwlkel  30026  2clwwlk2clwwlk  30027  extwwlkfabel  30030  clwwlknonclwlknonf1o  30039  dlwwlknondlwlknonf1olem1  30041  numclwwlk2lem1  30053  numclwlk2lem2f  30054  numclwlk2lem2f1o  30056  ex-res  30118  isssp  30401  sspn  30413  islno  30430  isblo  30459  nmlno0  30472  ishmo  30488  dipdir  30519  dipass  30522  ubthlem1  30547  ubthlem2  30548  htthlem  30594  htth  30595  ocel  30958  ocnel  30975  shsel  30991  shsel2  30999  shmodsi  31066  pjhtheu  31071  pjeq  31076  axpjpj  31097  pjoc2  31116  elspani  31220  h1de2ctlem  31232  elspansn  31243  elspansn2  31244  elnlfn  31605  eleigvec  31634  riesz3i  31739  cbviunf  32211  iuneq12daf  32212  iunrdx  32219  iunrnmptss  32221  cbvdisjf  32226  disjorf  32234  disjabrex  32237  disjabrexf  32238  iundisjf  32244  disjrdx  32246  elimampt  32286  2ndresdju  32298  abfmpunirn  32301  abfmpeld  32303  abfmpel  32304  fmptcof2  32306  acunirnmpt2  32309  acunirnmpt2f  32310  aciunf1lem  32311  funcnvmpt  32316  suppss3  32373  fpwrelmap  32382  xrofsup  32404  iundisjfi  32431  eliccioo  32521  s3f1  32537  ccatf1  32539  swrdrn3  32543  ismnt  32577  mgcoval  32580  gsummpt2co  32627  gsumpart  32634  gsumhashmul  32635  xrge0tsmsbi  32637  cycpmco2  32719  cyc3co2  32726  inftmrel  32753  isinftm  32754  isslmd  32774  urpropd  32805  isdrng4  32822  resv1r  32883  eqg0el  32904  ellspds  32912  lbslsp  32924  rhmimaidl  32981  isprmidl  32987  qsidomlem1  33002  qsidomlem2  33003  ismxidl  33009  crngmxidl  33016  drng0mxidl  33023  opprqus0g  33035  qsfld  33043  isrprm  33065  dimpropd  33138  lbslsat  33146  extdg1id  33187  elirng  33196  ply1annidllem  33208  smatrcl  33231  smatcl  33237  ist0cld  33268  txomap  33269  locfinreflem  33275  zarclsiin  33306  zart0  33314  rhmpreimacnlem  33319  metidval  33325  cnre2csqima  33346  ordtrest2NEW  33358  fmcncfil  33366  fsumcvg4  33385  ofcfval  33551  measvuni  33667  meascnbl  33672  faeval  33699  ismbfm  33704  elunirnmbfm  33705  imambfm  33716  elcarsg  33759  itgeq12dv  33780  issibf  33787  eulerpartlems  33814  eulerpartlemgc  33816  eulerpartlemgvv  33830  eulerpartlemgu  33831  eulerpart  33836  rrvmbfm  33896  elorvc  33913  elorrvc  33917  dstfrvunirn  33928  ballotlemfc0  33946  ballotlemfcc  33947  ballotlemsima  33969  ballotlemrv  33973  fzssfzo  34005  signstfvn  34035  signstfvneq0  34038  signstres  34041  repr0  34078  reprinrn  34085  reprdifc  34094  hgt750lemg  34121  hgt750lemb  34123  istrkg2d  34133  axtgupdim2ALTV  34135  afsval  34138  brafs  34139  bnj945  34239  bnj1400  34301  bnj18eq1  34393  bnj916  34399  bnj1014  34427  bnj1015  34428  bnj1110  34448  bnj1417  34507  revpfxsfxrev  34561  cplgredgex  34566  pfxwlk  34569  revwlk  34570  subfacp1lem2b  34627  subfacp1lem4  34629  subfacp1lem5  34630  subfacp1lem6  34631  ptpconn  34679  cvmscbv  34704  iscvm  34705  cvmsi  34711  cvmsval  34712  cvmliftmolem1  34727  cvmlift2lem12  34760  cvmlift2lem13  34761  cvmlift3lem7  34771  snmlval  34777  satfv1  34809  satfvsucsuc  34811  satfrnmapom  34816  satf0op  34823  satf0n0  34824  sat1el2xp  34825  fmlafvel  34831  isfmlasuc  34834  fmlaomn0  34836  gonan0  34838  goaln0  34839  gonar  34841  goalr  34843  satffunlem1lem2  34849  satffunlem2lem2  34852  satfv0fvfmla0  34859  satef  34862  satefvfmla0  34864  sategoelfvb  34865  satfv1fvfmla1  34869  mrsubfval  34954  mrsubvrs  34968  mclsrcl  35007  mclsval  35009  mppsval  35018  mclsppslem  35029  opelco3  35207  wsuclem  35258  funtransport  35464  fvtransport  35465  brcolinear  35492  colineardim1  35494  funray  35573  fvray  35574  funline  35575  fvline  35577  lineelsb2  35581  fwddifval  35595  fwddifnval  35596  rankelg  35601  rankeq1o  35604  elhf2  35608  0hf  35610  gg-taylthlem2  35623  neibastop2lem  35701  neibastop3  35703  eltail  35715  bj-projeq  36329  bj-projval  36333  bj-restsn  36419  opelopabbv  36480  brabd0  36484  bj-eldiag  36513  bj-eldiag2  36514  mptsnunlem  36675  dissneqlem  36677  iooelexlt  36699  relowlssretop  36700  rdgellim  36713  exrecfnlem  36716  finxpeq1  36723  finxpreclem6  36733  pibp21  36752  curf  36922  uncf  36923  curunc  36926  unccur  36927  fin2so  36931  lindsadd  36937  lindsdom  36938  lindsenlbs  36939  matunitlindflem1  36940  matunitlindflem2  36941  matunitlindf  36942  ptrest  36943  ptrecube  36944  poimirlem2  36946  poimirlem8  36952  poimirlem17  36961  poimirlem18  36962  poimirlem20  36964  poimirlem21  36965  poimirlem22  36966  poimirlem24  36968  poimirlem26  36970  poimirlem29  36973  heicant  36979  mblfinlem1  36981  mblfinlem2  36982  volsupnfl  36989  itg2addnclem  36995  itg2gt0cn  36999  indexdom  37058  incsequz  37072  istotbnd  37093  istotbnd3  37095  0totbnd  37097  sstotbnd  37099  sstotbnd3  37100  isbnd  37104  prdstotbnd  37118  cntotbnd  37120  isismty  37125  heibor1lem  37133  heiborlem2  37136  heiborlem3  37137  heibor  37145  isass  37170  exidcl  37200  exidreslem  37201  elghomlem2OLD  37210  rngoidmlem  37260  rngo1cl  37263  divrngcl  37281  isdrngo2  37282  isrngohom  37289  isrngoiso  37302  isriscg  37308  iscom2  37319  iscringd  37322  isidl  37338  ispridl  37358  ismaxidl  37364  ac6s6  37496  dmecd  37629  releldmqs  37984  releldmqscoss  37986  erimeq2  38004  eldisjlem19  38136  membpartlem19  38137  prter3  38208  islshp  38305  islsat  38317  lcvfbr  38346  islfl  38386  ellkr  38415  islshpkrN  38446  ldual1dim  38492  isopos  38506  cmtfvalN  38536  cvrfval  38594  isat  38612  islln  38833  islpln  38857  islvol  38900  isline  39066  ispointN  39069  ispsubsp  39072  elpmap  39085  elpmapat  39091  elpadd  39126  paddclN  39169  elpclN  39219  elpcliN  39220  pclfinN  39227  pclcmpatN  39228  ispsubclN  39264  iswatN  39321  islhp  39323  islaut  39410  ispautN  39426  isldil  39437  isltrn  39446  isdilN  39481  istrnN  39484  istendo  40087  dvhb1dimN  40313  erng1lem  40314  erngdvlem4-rN  40326  diaelval  40360  diaeldm  40363  dia1dimid  40390  cdlemm10N  40445  dibopelvalN  40470  dibopelval2  40472  dibelval3  40474  dibelval1st  40476  dibelval2nd  40479  dibeldmN  40485  dibvalrel  40490  dibglbN  40493  dicffval  40501  dicfval  40502  dicopelval  40504  dicelvalN  40505  dicelval3  40507  dicvalrelN  40512  dicelval1sta  40514  diclspsn  40521  dihopelvalbN  40565  dihopelvalcqat  40573  dihopelvalcpre  40575  dihvalrel  40606  dih1  40613  dihmeetlem4preN  40633  dihmeetlem13N  40646  dih1dimatlem  40656  dochnel2  40719  dihjatcclem4  40748  dvh2dim  40772  dvh3dim  40773  dvh4dimN  40774  dochfln0  40804  lpolsetN  40809  islpolN  40810  lcfrvalsnN  40868  lcfrlem21  40890  lcfrlem27  40896  lcfrlem37  40906  lcfr  40912  lcdlss  40946  mapdcv  40987  hdmap1fval  41123  hdmapffval  41153  hdmapfval  41154  hdmapval  41155  hgmapffval  41212  hgmapfval  41213  hdmapellkr  41241  hlhilhillem  41291  fzsplitnd  41307  sticksstones11  41431  sticksstones12a  41432  fzosumm1  41527  frlmfielbas  41533  frlmsnic  41565  isnacs  41897  mrefg2  41900  elmzpcl  41919  mzpcompact2  41945  eldiophb  41950  elpell1qr  42040  elpell14qr  42042  elpell1234qr  42044  pw2f1ocnv  42231  pw2f1o2val2  42234  aomclem4  42254  aomclem6  42256  islssfg2  42268  imasgim  42297  lnr2i  42313  elmnc  42333  rngunsnply  42370  onexomgt  42445  onexlimgt  42447  onexoegt  42448  oaordnr  42501  omnord1  42510  oenord1  42521  cantnfresb  42529  tfsconcatun  42542  tfsconcat0i  42550  ofoaf  42560  naddcnff  42567  naddcnffo  42569  naddcnfcom  42571  naddcnfid1  42572  naddcnfid2  42573  naddcnfass  42574  naddwordnexlem4  42607  fiinfi  42779  sqrtcvallem1  42837  elintima  42859  eliunov2  42885  ov2ssiunov2  42906  brtrclfv2  42933  rfovcnvf1od  43210  rfovcnvfvd  43213  fsovrfovd  43215  fsovfvd  43216  fsovcnvlem  43219  ntrclsfv1  43261  ntrclselnel1  43263  ntrclsneine0lem  43270  ntrneifv1  43285  ntrneifv2  43286  ntrneiel  43287  gneispace2  43338  gneispacess2  43352  extoimad  43371  mnringelbased  43428  dvconstbi  43548  bccbc  43559  eliin2f  44247  rabbida2  44275  disjinfi  44342  unirnmap  44358  elmptima  44413  iuneqfzuzlem  44495  iooiinioc  44720  fsumiunss  44742  fsumsupp0  44745  lptre2pt  44807  icccncfext  45054  cncfiooicclem1  45060  dvnprodlem2  45114  stoweidlem27  45194  stoweidlem29  45196  stoweidlem31  45198  stoweidlem34  45201  stoweidlem48  45215  stoweidlem59  45226  dirkercncflem2  45271  dirkercncflem4  45273  fourierdlem2  45276  fourierdlem3  45277  fourierdlem25  45299  fourierdlem32  45306  fourierdlem33  45307  fourierdlem41  45315  fourierdlem48  45321  fourierdlem49  45322  fourierdlem62  45335  fourierdlem70  45343  fourierdlem80  45353  fourierdlem92  45365  fourierdlem93  45366  fourierdlem101  45374  etransclem37  45438  sge0val  45533  sge0f1o  45549  sge0iunmptlemre  45582  sge0iunmpt  45585  iundjiun  45627  caragenel  45662  ovncvrrp  45731  ovnsubaddlem1  45737  ovnsubadd  45739  hoidmvlelem2  45763  hoidmvlelem3  45764  hoidmvlelem4  45765  hoidmvle  45767  ovncvr2  45778  hspdifhsp  45783  hoiqssbl  45792  hspmbllem2  45794  hspmbl  45796  opnvonmbllem1  45799  isvonmbl  45805  ovnovollem1  45823  issmflem  45894  smflimlem3  45940  smflimlem4  45941  smflim  45944  smfmullem2  45959  smflimmpt  45977  smfsuplem1  45978  smflimsuplem1  45987  smflimsuplem3  45989  smflimsuplem4  45990  smflimsuplem7  45993  smflimsup  45995  tworepnotupword  46051  fcores  46228  fcoresf1  46230  afvelrnb  46322  afvelrnb0  46323  afv2co2  46416  el1fzopredsuc  46484  iccpart  46535  iccpartgtprec  46539  iccpartiltu  46541  iccpartigtl  46542  iccpartltu  46544  iccpartgtl  46545  iccpartgt  46546  iccpartleu  46547  iccpartgel  46548  iccelpart  46552  iccpartiun  46553  icceuelpart  46555  fargshiftfv  46558  fargshiftfo  46561  sprel  46603  prprelb  46635  prprelprb  46636  fpprel  46847  sbgoldbo  46906  wtgoldbnnsum4prm  46921  bgoldbnnsum3prm  46923  bgoldbtbndlem3  46926  bgoldbtbnd  46928  upwlksfval  46964  isupwlk  46965  intop  47032  isclintop  47036  assintop  47038  isassintop  47039  assintopcllaw  47041  uzlidlring  47064  elrngchomALTV  47098  rngccatidALTV  47101  rngcsectALTV  47104  rngcisoALTV  47106  rhmsubcALTVlem3  47112  rhmsubcALTVlem4  47113  funcringcsetcALTV2lem7  47125  funcringcsetcALTV2lem9  47127  elringchomALTV  47132  ringccatidALTV  47135  ringcsectALTV  47138  ringcisoALTV  47140  ringcbasbasALTV  47141  funcringcsetclem7ALTV  47148  funcringcsetclem9ALTV  47150  srhmsubcALTV  47154  opeliun2xp  47163  cbvmpox2  47166  ply1sclrmsm  47218  dmatALTbasel  47237  lcoval  47247  lindslinindsimp1  47292  lindslinindsimp2  47298  lmod1  47327  elbigo  47391  elbigo2  47392  elbigolo1  47397  dig2nn0ld  47444  naryfvalel  47470  rrxlines  47573  rrxlinesc  47575  rrxlinec  47576  eenglngeehlnm  47579  elrrx2linest2  47585  rrxsphere  47588  itsclc0  47611  itsclc0b  47612  itsclinecirc0  47613  itsclinecirc0b  47614  itscnhlinecirc02p  47625  f1omo  47681  lubeldm2d  47745  glbeldm2d  47746  catprs  47785  isthinc  47795  isthincd2lem1  47801  thincmoALT  47804  thincmod  47805  isthincd  47811  prsthinc  47828  elsetrecslem  47898