Theorem eleq2d 2855

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1565   = wceq 1567  ∃wex 1806   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  eleq2  2858  eleq12d  2863  eleqtrd  2871  neleqtrd  2891  eqabrd  2910  raleqbidv  3345  rexeqbidv  3346  reueqbidv  3412  rabeqbidva  3439  elabd2  3638  sbcbid  3807  sbcbi2  3811  csbeq2d  3867  csbeq2dv  3868  cbvcsbw  3871  cbvcsb  3872  cbvcsbv  3873  csbie  3896  csbied  3897  csbie2g  3901  cbvralcsf  3903  cbvreucsf  3905  cbvrabcsf  3906  sbcel12  4382  sbcel1g  4387  sbcel2  4389  prel12g  4833  eliuni  4966  iuneqconst  4972  iuneq12df  4987  iuneq12d  4990  cbviun  5003  cbviin  5004  cbviung  5005  cbviing  5006  cbviunv  5007  cbviinv  5008  iinxsng  5058  iinxprg  5059  iunxsng  5060  iunxsngf  5062  cbvdisj  5090  cbvdisjv  5091  disjor  5095  disjiund  5104  mpteq12da  5198  mpteq12f  5200  mpteq12dva  5201  axpweq  5322  rabxfrd  5389  brab2d  5523  rbropapd  5548  opeliunxp  5729  opeliun2xp  5730  opeliunxp2  5825  iunxpf  5835  elimampt  6046  elrelimasn  6089  elimasni  6094  xpdifid  6166  xpdifcnvepel  6167  imadifssranOLD  6204  ressn  6287  funfni  6642  fnbr  6644  dffv3  6878  elfv2ex  6925  fvelrnb  6942  foelcdmi  6943  fvun1  6973  fvco2  6979  funcnvmpt  6992  elfvmptrab1w  7018  elfvmptrab1  7019  elfvmptrab  7020  elpreima  7054  dff3  7096  fmptco  7126  fnelfp  7174  fnelnfp  7176  tpres  7200  fnprb  7207  fntpb  7208  funfvima3  7235  eluniima  7249  dff13  7253  f1ounsn  7271  f1eqcocnv  7300  isoini  7337  riotaeqdv  7369  mpoeq123dva  7485  cbvmpox  7504  elimampo  7548  ovelrn  7587  elovmpod  7655  elovmpo  7656  elovmporab  7657  elovmporab1w  7658  elovmporab1  7659  elovmpt3rab1  7671  fiun  7940  f1iun  7941  zfrep6OLD  7952  fmpox  8064  el2mpocsbcl  8080  el2mpocl  8081  bropopvvv  8085  bropfvvvv  8087  xpord2indlem  8143  xpord3inddlem  8150  elsuppfng  8165  elsuppfn  8166  suppfnss  8185  opeliunxp2f  8206  mpoxopn0yelv  8209  mpoxopovel  8216  rntpos  8235  mpocurryd  8265  fpr2  8301  wfr2  8324  onoviun  8330  smoel  8347  smoiso  8349  smoel2  8350  smo11  8351  tfrlem9  8372  oalimcl  8545  oaass  8546  omordi  8551  omordlim  8562  omlimcl  8563  odi  8564  omeulem1  8567  omeulem2  8568  oen0  8572  oeordi  8573  oeordsuc  8580  oelimcl  8586  oeeulem  8587  oeeui  8588  nnmordi  8617  oaabs2  8635  omabs  8637  omsmolem  8643  ereldm  8748  iiner  8787  elmapg  8836  elpmg  8840  elixpsn  8935  ixpsnf1o  8936  boxriin  8938  omxpenlem  9066  pw2f1olem  9069  phplem2  9189  php3  9193  infn0  9262  elfi  9373  dffi3  9391  marypha2lem2  9396  ordiso2  9477  wemapsolem  9512  elharval  9523  inf3lemd  9596  inf3lem1  9597  inf3lem2  9598  inf3lem3  9599  cantnfs  9635  cantnfp1lem3  9649  cantnflem1b  9655  cantnflem1  9658  ttrclselem2  9695  trcl  9697  frr2  9732  r1sdom  9746  r1ordg  9750  r1pwss  9756  tz9.12lem3  9761  tz9.12  9762  r1elwf  9768  rankr1ai  9770  rankidb  9772  rankr1bg  9775  rankval2  9790  rankunb  9822  tcrank  9856  acni  10029  acni2  10030  acndom  10035  infpwfien  10046  alephnbtwn  10055  cardaleph  10073  cardinfima  10081  iunfictbso  10098  dfac3  10105  dfac5lem5  10111  dfac5  10112  dfac9  10120  dfac12r  10130  kmlem2  10135  kmlem12  10145  kmlem13  10146  kmlem14  10147  ackbij2lem3  10223  ackbij2  10225  cofsmo  10253  alephsing  10260  fin23lem30  10326  isf32lem9  10345  itunisuc  10403  axcc2lem  10420  axcc3  10422  domtriomlem  10426  axdc2lem  10432  axdc2  10433  axdc3lem2  10435  axdc3lem4  10437  axdc4lem  10439  ac6c4  10465  zorn2lem1  10480  ttukeylem6  10498  pwcfsdom  10568  axregndlem2  10588  axinfndlem1  10590  axacndlem4  10595  axacnd  10597  pwfseqlem1  10643  inar1  10760  inatsk  10763  gruurn  10783  grur1  10805  eltskm  10828  genpelv  10985  eluz1  12866  elixx1  13381  elixx3g  13385  elioo2  13413  elfz1  13540  elfz2  13542  elfzp1  13602  fzpr  13607  fzsuc2  13610  fzrev3  13618  elfzp12  13631  fzm1  13635  elfzo  13689  fz0add1fz1  13764  elfzo0l  13785  elfzom1b  13795  fzosplitsni  13808  elfzr  13810  elfzlmr  13811  zmodidfzo  13933  seqp1  14052  seqf1o  14079  bcval  14340  bcpasc  14357  hashf1lem1  14492  fundmge2nop0  14539  wrdmap  14583  elovmpowrd  14595  ccatfval  14610  elfzelfzccat  14617  ccatlid  14624  ccatass  14626  ccatrn  14627  ccatalpha  14631  swrdfv2  14699  ccatswrd  14706  swrdccat2  14707  pfxfv  14720  pfxeq  14733  ccatpfx  14738  swrdswrd  14742  swrdpfx  14744  pfxpfx  14745  cats1un  14758  swrdccatfn  14761  swrdccatin1  14762  pfxccatin12lem4  14763  pfxccatin12lem1  14765  swrdccatin2  14766  pfxccatin12lem2c  14767  pfxccatin12lem2  14768  swrdccat3blem  14776  swrdccatin1d  14780  swrdccatin2d  14781  pfxccatin12d  14782  revccat  14803  revrev  14804  repswpfx  14822  repswccat  14823  cshwidxmod  14840  2cshw  14850  cshwcshid  14864  cshwcsh2id  14865  cshimadifsn  14866  cshimadifsn0  14867  revco  14871  ccatco  14872  cshco  14873  swrdco  14874  ofccat  15006  shftfn  15110  shftval  15111  limsupgle  15528  ello12  15567  elo12  15578  isercolllem3  15718  sumeq1  15740  fsumsplit  15792  sumsplit  15819  fsum2dlem  15821  fsumcom2  15825  fsumparts  15858  explecnv  15919  pwdif  15922  fprodser  16003  fprodsplit  16020  fprod2dlem  16034  fprodcom2  16038  eftlub  16165  divalgmod  16464  bitsval  16482  bitsp1e  16490  bitsp1o  16491  sadfval  16510  sadcp1  16513  sadval  16514  sadcadd  16516  sadadd2  16518  saddisjlem  16522  sadadd  16525  sadass  16529  smufval  16535  smuval  16539  smuval2  16540  smupvallem  16541  smu01lem  16543  smueqlem  16548  smumul  16551  bezoutlem2  16598  bezoutlem4  16600  algfx  16638  eucalgcvga  16644  reumodprminv  16864  nnnn0modprm0  16866  unbenlem  16968  prmreclem5  16980  vdwapval  17033  vdwapun  17034  vdwnnlem1  17055  vdwnn  17058  ramval  17068  0ram  17080  ramub1lem2  17087  prmgaplem7  17117  prmlem0  17165  elrest  17480  prdsbasmpt  17523  prdsleval  17530  prdsbasmpt2  17535  pwselbasb  17541  imasaddfnlem  17582  imasvscafn  17591  divsfval  17601  ismre  17642  mreunirn  17653  mrisval  17686  ismri  17687  isacs  17707  catidd  17736  iscatd2  17737  ismon  17790  isepi  17797  sectffval  17807  sectfval  17808  dfiso2  17829  cicsym  17861  issubc  17892  catsubcat  17896  isfunc  17921  funcres  17953  funcpropd  17959  ffthiso  17988  isnat  18007  isnat2  18008  fuciso  18035  initoval  18050  termoval  18051  isinito  18053  istermo  18054  iszeroo  18055  isinitoi  18056  istermoi  18057  initoid  18058  termoid  18059  iszeroi  18066  2initoinv  18067  initoeu1  18068  initoeu2  18073  2termoinv  18074  termoeu1  18075  arwhoma  18102  elsetchom  18138  setcmon  18144  setcepi  18145  setciso  18148  catciso  18168  elestrchom  18184  estrcbasbas  18187  funcestrcsetclem7  18202  funcestrcsetclem8  18203  funcestrcsetclem9  18204  fthestrcsetc  18206  fullestrcsetc  18207  equivestrcsetc  18208  setc1strwun  18209  funcsetcestrclem7  18217  funcsetcestrclem8  18218  funcsetcestrclem9  18219  fthsetcestrc  18221  fullsetcestrc  18222  hofcl  18315  hofpropd  18323  yonedalem4c  18333  yonedainv  18337  yonffthlem  18338  lubeldm  18407  glbeldm  18420  joindef  18430  meetdef  18444  poslubdg  18468  acsficl2d  18608  acsmapd  18610  psref  18630  psss  18636  dirge  18659  chnccats1  18681  chnccat  18682  chnrev  18683  mgmpropd  18709  issstrmgm  18711  grpidval  18719  grpidpropd  18720  grpidd  18729  ismgmhm  18754  issubmgm  18760  issgrpd  18788  sgrppropd  18789  ismndd  18814  mndpropd  18817  imasmnd2  18832  imasmnd  18833  xpsmnd0  18836  ismhm  18843  issubm  18861  gsumsgrpccat  18899  elefmndbas2  18933  smndex1mndlem  18971  imasgrp2  19121  imasgrp  19122  issubg  19192  subginv  19199  isnsg  19221  eqg0el  19254  quselbas  19255  isghm  19286  resghm2b  19304  conjnmzb  19323  conjnsg  19324  ghmpropd  19326  isga  19361  elcntz  19392  elcntzsn  19395  cntzrcl  19397  resscntz  19403  symgextf1  19491  gsmsymgreqlem2  19501  f1otrspeq  19517  pmtrfrn  19528  pmtrdifellem3  19548  pmtrdifellem4  19549  psgnunilem1  19563  psgnunilem5  19564  psgnunilem2  19565  psgnunilem3  19566  psgneldm2  19574  psgnfitr  19587  psgnsn  19590  gexdvds  19654  gex1  19661  isslw  19678  sylow3lem2  19698  lsmelvalx  19710  pj1ghm  19773  efgtlen  19796  efgsfo  19809  efgredlemc  19815  frgp0  19830  frgpmhm  19835  qusabl  19935  frgpnabllem1  19943  imasabl  19946  cycsubmcmn  19959  0cyg  19963  cycsubgcyg  19971  gsumval3  19977  gsumcllem  19978  gsumzaddlem  19991  gsumzsplit  19997  gsummptfzcl  20039  eldprd  20076  dprdcntz2  20110  dprd2d2  20116  dmdprdsplit2lem  20117  dmdprdsplit2  20118  dprdsplit  20120  ablfac2  20161  isrngd  20251  rngpropd  20252  imasrng  20255  qusrng  20258  ringurd  20267  isringd  20374  imasring  20412  xpsring1d  20415  dvdsrval  20443  isunit  20455  dvdsrpropd  20498  isirred  20501  isrnghm  20523  isrngim  20527  c0ghm  20543  c0snghm  20546  isrhm  20560  isrim0  20564  islring  20625  issubrng  20632  opprsubrng  20644  issubrg  20656  opprsubrg  20678  resrhm2b  20687  rhmpropd  20694  rnghmresel  20705  elrngchom  20709  rnghmsubcsetclem1  20716  rnghmsubcsetclem2  20717  rngcid  20720  rngcsect  20721  rngciso  20723  funcrngcsetcALT  20726  zrinitorngc  20727  zrtermorngc  20728  rhmresel  20734  elringchom  20738  rhmsubcsetclem1  20745  rhmsubcsetclem2  20746  ringcid  20749  rhmsscrnghm  20750  rhmsubcrngclem1  20751  rhmsubcrngclem2  20752  ringcsect  20755  ringciso  20757  ringcbasbas  20758  zrtermoringc  20760  srhmsubc  20765  rhmsubclem3  20772  rhmsubclem4  20773  drngunit  20818  isdrngd  20847  isdrngdOLD  20849  issdrg  20869  sdrgunit  20877  isabv  20892  issrngd  20936  islmod  20963  lmodprop2d  21023  islss  21033  islssd  21034  lssats2  21099  ellspsn  21102  islmhm  21126  lmhmf1o  21145  lmhmima  21146  lmhmpreima  21147  reslmhm  21151  pwssplit3  21160  lmhmpropd  21172  islbs  21175  lspprel  21193  lspfixed  21230  lbsacsbs  21258  lbsextlem1  21260  lbsextlem2  21261  lbsextlem3  21262  lbsextlem4  21263  ixpsnbasval  21307  isridlrng  21322  rnglidlmmgm  21353  isridl  21362  quscrng  21394  rngqiprngimfolem  21401  rngqiprngimf1lem  21405  rngqiprngimfo  21412  isprmidl  21434  qsidomlem1  21449  qsidomlem2  21450  islpidl  21462  lidldvgen  21471  irinitoringc  21598  pzriprnglem13  21612  pzriprnglem14  21613  zrhrhmb  21629  znf1o  21670  frgpcyg  21692  psgnevpmb  21706  isphld  21773  phlssphl  21778  elocv  21787  iscss  21802  isobs  21839  obs2ss  21848  dsmmfi  21857  dsmmelbas  21858  dsmmlss  21863  frlmelbas  21875  frlmlbs  21916  frlmup1  21917  ellspd  21921  islinds  21928  islindf2  21933  f1lindf  21941  islindf4  21957  assamulgscmlem2  22019  psrgrp  22075  mplsubglem  22117  mpllsslem  22118  mplmonmul  22156  subrgascl  22186  subrgasclcl  22187  mpfind  22235  ismhp  22272  gsumply1subr  22362  lply1binomsc  22440  matbas2d  22549  matecl  22551  matvscl  22557  mat1  22573  mat0dim0  22593  mat0dimid  22594  mat0dimscm  22595  mat1dimelbas  22597  dmatel  22619  scmatel  22631  scmateALT  22638  scmataddcl  22642  scmatsubcl  22643  smatvscl  22650  scmatghm  22659  mat1scmat  22665  mdetunilem7  22744  mdetunilem9  22746  smadiadetr  22801  cramerimplem2  22810  cramer0  22816  pmatcoe1fsupp  22827  cpmatpmat  22836  cpmatel  22837  cpmatacl  22842  cpmatinvcl  22843  mat2pmatghm  22856  mat2pmatmul  22857  decpmatmullem  22897  pmatcollpwlem  22906  pmatcollpw3fi1lem1  22912  pmatcollpwscmatlem1  22915  monmat2matmon  22950  chfacfscmul0  22984  chfacfscmulgsum  22986  chfacfpmmulgsum  22990  cayhamlem1  22992  cpmadugsumlemB  23000  cpmadugsumlemC  23001  cpmadugsumlemF  23002  cayhamlem2  23010  istopon  23038  eltg  23083  eltg2  23084  eltop  23100  eltop2  23101  eltop3  23102  pptbas  23134  iscld  23153  neiss2  23227  isnei  23229  neiptopnei  23258  neiptopreu  23259  lpfval  23264  lpval  23265  islp  23266  maxlp  23273  islpi  23275  neitr  23306  restlp  23309  ordtbas2  23317  ordtrest2  23330  lmfval  23358  cnfval  23359  iscn  23361  iscnp  23363  tgcn  23378  tgcnp  23379  lmbrf  23386  cnpresti  23414  ist1  23447  ist1-2  23473  cnt1  23476  haust1  23478  cmpfi  23534  cmpfii  23535  1stcfb  23571  2ndc1stc  23577  1stcrest  23579  2ndcdisj  23582  1stcelcls  23587  nllyi  23601  subislly  23607  islocfin  23643  lfinpfin  23650  locfindis  23656  locfincf  23657  comppfsc  23658  kgenval  23661  elkgen  23662  kgencn2  23683  txbas  23693  eltx  23694  ptval  23696  ptpjpre1  23697  ptopn2  23710  ptpjopn  23738  ptclsg  23741  xkoccn  23745  txdis  23758  txdis1cn  23761  ptrescn  23765  hausdiag  23771  hauseqlcld  23772  txhaus  23773  xkohaus  23779  elqtop  23823  qtopeu  23842  kqcldsat  23859  hmeofval  23884  ptuncnv  23933  ptunhmeo  23934  elmptrab  23953  fbdmn0  23960  elfg  23997  elfilss  24002  filunirn  24008  fixufil  24048  elfm  24073  rnelfmlem  24078  rnelfm  24079  fmfnfmlem4  24083  elflim2  24090  flimtopon  24096  elflim  24097  hausflim  24107  flimcls  24111  flfnei  24117  isflf  24119  hausflf  24123  cnpflf  24127  cnflf  24128  txflf  24132  isfcls  24135  fclstopon  24138  isfcls2  24139  fclssscls  24144  fclsnei  24145  fclsfnflim  24153  flimfnfcls  24154  isfcf  24160  fcfelbas  24162  cnpfcf  24167  cnfcf  24168  flfcntr  24169  alexsublem  24170  alexsubALTlem3  24175  cnextfun  24190  cnextfvval  24191  cnextf  24192  cnextcn  24193  tmdgsum2  24222  tgpconncomp  24239  ghmcnp  24241  qustgplem  24247  eltsms  24259  haustsms  24262  tsmsgsum  24265  tsmssubm  24269  tsmssplit  24278  isust  24330  ustbas  24353  elutop  24359  ustuqtoplem  24365  ustuqtop4  24370  ustuqtop  24372  utopsnneiplem  24373  utopsnneip  24374  utopsnnei  24375  isusp  24387  isucn  24403  ucncn  24410  iscfilu  24413  neipcfilu  24421  iscusp  24424  cnextucn  24428  ispsmet  24430  ismet  24449  isxmet  24450  elblps  24513  elbl  24514  elmopn  24568  prdsbl  24617  neibl  24627  met1stc  24647  metrest  24650  prdsxmslem2  24655  txmetcnp  24673  txmetcn  24674  metustsym  24681  cfilucfil2  24687  elbl4  24689  metuel  24690  psmetutop  24693  restmetu  24696  metucn  24697  tngngp  24780  isnmhm  24872  zcld  24940  metnrmlem1a  24985  elcncf  25017  cncfcnvcn  25053  cnheibor  25083  lebnumlem1  25089  ishtpy  25100  isphtpy  25109  om1elbas  25160  elpi1  25173  pi1xfr  25183  pi1coghm  25189  tcphcph  25365  lmmbrf  25390  iscfil  25393  iscau  25404  iscauf  25408  caucfil  25411  iscmet  25412  cmetcaulem  25416  iscmet3lem1  25419  iscmet3lem2  25420  iscmet3  25421  bcthlem1  25452  cmsss  25479  cmetcusp1  25481  cmetcusp  25482  cmscsscms  25501  rrxcph  25520  minveclem3b  25556  ovolfioo  25595  ovolficc  25596  ovolctb  25618  ovoliunnul  25635  ovolshftlem1  25637  sca2rab  25640  ovolscalem1  25641  ovolicc2lem1  25645  ovolicc2lem2  25646  ovolicc2lem4  25648  ovolicc2lem5  25649  iundisj  25676  iunmbl2  25685  uniioombllem3  25713  vitalilem2  25737  vitalilem3  25738  mbfss  25774  i1faddlem  25821  i1fmullem  25822  mbfi1fseqlem2  25844  mbfi1fseqlem4  25846  mbfi1fseq  25849  itg2splitlem  25876  itg2split  25877  itg2monolem1  25878  itg2gt0  25888  isibl  25893  iblss2  25934  itgss3  25943  itgsplit  25964  ellimc  26001  limcmo  26010  cnlimc  26016  limciun  26022  limcun  26023  eldv  26026  dvbsss  26030  dvreslem  26037  elcpn  26062  dvaddf  26070  dvmulf  26071  dvcof  26076  rolle  26118  dvlip2  26123  dvivthlem1  26136  lhop1  26142  lhop2  26143  ftc1cn  26171  fta1glem2  26295  plyco0  26318  elply  26321  ply1termlem  26329  eltayl  26489  tayl0  26491  taylplem1  26492  taylplem2  26493  dvtaylp  26499  taylthlem1  26502  taylthlem2  26503  abelth  26570  cxpcn3  26879  rlimcnp  27096  fsumharmonic  27142  dchrelbas  27366  pntrsumbnd2  27697  ostth2lem2  27764  nolesgn2ores  27802  nogesgn1ores  27804  nosupprefixmo  27830  noinfprefixmo  27831  nosupcbv  27832  nosupdm  27834  nosupfv  27836  nosupres  27837  nosupbnd1lem1  27838  nosupbnd1lem3  27840  nosupbnd1lem5  27842  nosupbnd2lem1  27845  noinfcbv  27847  noinfdm  27849  noinffv  27851  noinfres  27852  noinfbnd1lem1  27853  noinfbnd1lem3  27855  noinfbnd1lem5  27857  noinfbnd2lem1  27860  elmade  28016  elold  28018  sltsleft  28019  sltsright  28020  oldlim  28046  madebday  28059  newbday  28061  ltslpss  28067  bdayiun  28074  cofcutr  28083  cofcutrtime  28086  lrrecval  28098  lrrecval2  28099  addsval  28121  precsexlem9  28374  precsexlem11  28376  ltonold  28420  onnolt  28425  onlts  28426  noseqrdgfn  28465  istrkgb  28690  istrkgcb  28691  istrkge  28692  istrkgl  28693  istrkgld  28694  axtgsegcon  28699  axtg5seg  28700  axtgbtwnid  28701  axtgpasch  28702  axtgupdim2  28706  axtgeucl  28707  tgdim01  28742  iscgrg  28747  isismt  28769  tglnunirn  28783  tglngval  28786  tgellng  28788  legval  28819  legov  28820  legov2  28821  ishlg  28837  mirreu3  28893  mirval  28894  mirfv  28895  mircgr  28896  mirbtwn  28897  ismir  28898  mireq  28904  symquadlem  28928  israg  28936  perpln1  28949  perpln2  28950  isperp  28951  islnopp  28979  outpasch  28996  ishpg  29000  tgplnfn  29015  plngval  29017  isplng  29018  elplng  29020  elplngid  29022  lnincplng  29024  plngcplem  29025  plngcp  29026  plngrot  29030  nhpmirhp  29038  lnperpexs  29071  iscgra  29077  dfcgra2  29098  ragraghl  29104  isinag  29110  isleag  29119  iseqlg  29139  brprlng  29143  prlnghpg  29151  prlngmo  29157  f1otrgitv  29160  f1otrg  29161  f1otrge  29162  ttgval  29165  ttgelitv  29173  elee  29184  brbtwn  29190  brcgr  29191  axlowdimlem16  29248  ebtwntg  29273  elntg2  29276  upgrex  29383  edgupgr  29425  upgredg  29428  edglnl  29434  numedglnl  29435  uhgr2edg  29499  umgr2edg1  29502  usgredg2vlem1  29516  usgredg2vlem2  29517  ushgredgedg  29520  ushgredgedgloop  29522  uhgrspansubgrlem  29581  fusgrfisstep  29620  nbgrval  29627  nbgrel  29631  nbupgrel  29636  nbgr2vtx1edg  29641  nbuhgr2vtx1edgblem  29642  nbuhgr2vtx1edgb  29643  nbusgreledg  29644  usgrnbcnvfv  29656  uvtxval  29678  uvtxel  29679  uvtx01vtx  29688  uvtxusgrel  29694  nbcplgr  29725  cplgr3v  29726  cusgrexi  29734  structtocusgr  29737  vtxdgfval  29758  vtxdg0v  29764  vtxdeqd  29768  vtxdun  29772  1loopgrnb0  29793  1loopgrvd0  29795  1hevtxdg0  29796  1hevtxdg1  29797  1egrvtxdg1  29800  umgr2v2evtxel  29813  umgr2v2enb1  29817  umgr2v2evd2  29818  vtxdginducedm1lem4  29833  vtxdginducedm1  29834  finsumvtxdg2sstep  29840  ewlksfval  29892  isewlk  29893  wksfval  29900  iswlk  29901  uspgr2wlkeq  29936  wlkres  29959  dfpth2  30019  usgr2pthlem  30053  clwlkcompim  30070  uspgrn2crct  30098  wwlks  30125  iswwlksn  30128  wwlknvtx  30135  wlkiswwlks2  30165  wwlksm1edg  30171  wwlksnred  30182  wwlksnext  30183  wwlksnredwwlkn  30185  wwlksnredwwlkn0  30186  wwlksnwwlksnon  30205  wspn0  30214  usgr2wspthons3  30257  rusgrnumwwlkb0  30264  clwwlk  30275  clwwlkccatlem  30281  clwlkclwwlklem2a4  30289  clwlkclwwlk  30294  clwwisshclwwslem  30306  clwwlkinwwlk  30332  clwwlkel  30338  clwwlkf  30339  clwwlkext2edg  30348  wwlksext2clwwlk  30349  wwlksubclwwlk  30350  clwwnisshclwwsn  30351  eleclclwwlknlem2  30353  erclwwlknsym  30362  erclwwlkntr  30363  umgrhashecclwwlk  30370  clwwlkvbij  30405  eupth2lem3lem3  30522  eupth2lem3lem4  30523  eupth2lem3lem6  30525  eupth2lemb  30529  eucrct2eupth  30537  fusgreg2wsplem  30625  2clwwlklem  30635  2clwwlk2clwwlklem  30638  2clwwlkel  30641  2clwwlk2clwwlk  30642  extwwlkfabel  30645  clwwlknonclwlknonf1o  30654  dlwwlknondlwlknonf1olem1  30656  numclwwlk2lem1  30668  numclwlk2lem2f  30669  numclwlk2lem2f1o  30671  ex-res  30733  isssp  31017  sspn  31029  islno  31046  isblo  31075  nmlno0  31088  ishmo  31104  dipdir  31135  dipass  31138  ubthlem1  31163  ubthlem2  31164  htthlem  31210  htth  31211  ocel  31574  ocnel  31591  shsel  31607  shsel2  31615  shmodsi  31682  pjhtheu  31687  pjeq  31692  axpjpj  31713  pjoc2  31732  elspani  31836  h1de2ctlem  31848  elspansn  31859  elspansn2  31860  elnlfn  32221  eleigvec  32250  riesz3i  32355  cbviunf  32841  iuneq12daf  32842  iunrdx  32849  iunrnmptss  32851  cbvdisjf  32857  disjorf  32865  disjabrex  32868  disjabrexf  32869  iundisjf  32875  disjrdx  32877  fresunsn  32911  2ndresdju  32935  abfmpunirn  32938  abfmpeld  32940  abfmpel  32941  fmptcof2  32943  acunirnmpt2  32946  acunirnmpt2f  32947  aciunf1lem  32948  suppss3  33009  fpwrelmap  33019  xrofsup  33053  iundisjfi  33082  eliccioo  33191  s3f1  33208  ccatf1  33210  ccatws1f1o  33212  swrdrn3  33216  ismnt  33244  mgcoval  33247  gsummpt2co  33309  gsumpart  33324  gsumhashmul  33328  gsummulsubdishift1  33329  xrge0tsmsbi  33335  gsumwrd2dccatlem  33338  gsumwrd2dccat  33339  cycpmco2  33394  cyc3co2  33401  isfxp  33429  cntrval2  33432  inftmrel  33441  isinftm  33442  isslmd  33463  urpropd  33491  elrgspn  33507  erlval  33519  rlocval  33520  rloccring  33532  rloc1r  33534  rlocisunit  33537  domnprodeq0  33540  domnpropd  33541  isdrng4  33559  fracfld  33572  resv1r  33602  ellspds  33626  ellpi  33630  lbslsp  33634  rhmimaidl  33684  ismxidl  33690  crngmxidl  33697  drng0mxidl  33703  opprqus0g  33717  qsfld  33725  isrprm  33752  rsprprmprmidlb  33758  ressply1evls1  33800  ply1mulrtss  33817  ply1coedeg  33824  psrmonmul  33885  dimpropd  33944  lbslsat  33951  extdg1id  34001  fldextrspunlsplem  34008  fldextrspunlsp  34009  elirng  34021  ply1annidllem  34036  constrsuc  34073  constrconj  34080  constrllcllem  34087  constrlccllem  34088  constrcccllem  34089  nn0constr  34096  smatrcl  34131  smatcl  34137  ist0cld  34168  txomap  34169  locfinreflem  34175  zarclsiin  34206  zart0  34214  rhmpreimacnlem  34219  metidval  34225  cnre2csqima  34246  ordtrest2NEW  34258  fmcncfil  34266  fsumcvg4  34285  ofcfval  34433  measvuni  34549  meascnbl  34554  faeval  34581  ismbfm  34586  elunirnmbfm  34587  imambfm  34597  elcarsg  34640  itgeq12dv  34661  issibf  34668  eulerpartlems  34695  eulerpartlemgc  34697  eulerpartlemgvv  34711  eulerpartlemgu  34712  eulerpart  34717  rrvmbfm  34777  elorvc  34795  elorrvc  34799  dstfrvunirn  34810  ballotlemfc0  34828  ballotlemfcc  34829  ballotlemsima  34851  ballotlemrv  34855  fzssfzo  34874  signstfvn  34901  signstfvneq0  34904  signstres  34907  repr0  34943  reprinrn  34950  reprdifc  34959  hgt750lemg  34986  hgt750lemb  34988  istrkg2d  34998  axtgupdim2ALTV  35000  afsval  35006  brafs  35007  bnj945  35107  bnj1400  35168  bnj18eq1  35260  bnj916  35266  bnj1014  35294  bnj1015  35295  bnj1110  35315  bnj1417  35374  rankval2b  35435  r1filimi  35439  r1ssel  35443  onvf1odlem3  35488  vonf1wev  35491  vonf1owevOLD  35493  vonf1osev  35495  revpfxsfxrev  35506  cplgredgex  35512  pfxwlk  35515  revwlk  35516  subfacp1lem2b  35572  subfacp1lem4  35574  subfacp1lem5  35575  subfacp1lem6  35576  ptpconn  35624  cvmscbv  35649  iscvm  35650  cvmsi  35656  cvmsval  35657  cvmliftmolem1  35672  cvmlift2lem12  35705  cvmlift2lem13  35706  cvmlift3lem7  35716  snmlval  35722  satfv1  35754  satfvsucsuc  35756  satfrnmapom  35761  satf0op  35768  satf0n0  35769  sat1el2xp  35770  fmlafvel  35776  isfmlasuc  35779  fmlaomn0  35781  gonan0  35783  goaln0  35784  gonar  35786  goalr  35788  satffunlem1lem2  35794  satffunlem2lem2  35797  satfv0fvfmla0  35804  satef  35807  satefvfmla0  35809  sategoelfvb  35810  satfv1fvfmla1  35814  mrsubfval  35899  mrsubvrs  35913  mclsrcl  35952  mclsval  35954  mppsval  35963  mclsppslem  35974  opelco3  36166  wsuclem  36214  funtransport  36422  fvtransport  36423  brcolinear  36450  colineardim1  36452  funray  36531  fvray  36532  funline  36533  fvline  36535  lineelsb2  36539  fwddifval  36553  fwddifnval  36554  rankelg  36559  rankeq1o  36562  elhf2  36566  0hf  36568  nmulprop  36581  nmulr0  36586  rmoeqbidv  36614  disjeq12dv  36616  ixpeq12dv  36617  prodeq12sdv  36619  itgeq12sdv  36620  cbvralvw2  36627  cbvrexvw2  36628  cbvrmovw2  36629  cbvreuvw2  36630  cbvcsbvw2  36632  cbviunvw2  36633  cbviinvw2  36634  cbvmptvw2  36635  cbvdisjvw2  36636  cbvmpo1vw2  36644  cbvmpo2vw2  36645  cbvsbcdavw  36658  cbvcsbdavw  36660  cbvcsbdavw2  36661  cbviundavw  36663  cbviindavw  36664  cbvdisjdavw  36669  cbvrabdavw2  36686  cbviundavw2  36687  cbviindavw2  36688  cbvmptdavw2  36689  cbvdisjdavw2  36690  cbvriotadavw2  36691  cbvmpo1davw2  36693  cbvmpo2davw2  36694  cbvsumdavw2  36696  neibastop2lem  36760  neibastop3  36762  eltail  36774  ttctr  36893  dfttc2g  36906  mh-infprim2bi  36947  bj-projeq  37516  bj-projval  37520  bj-restsn  37612  opelopabbv  37675  brabd0  37679  bj-eldiag  37708  bj-eldiag2  37709  mptsnunlem  37872  dissneqlem  37874  iooelexlt  37896  relowlssretop  37897  rdgellim  37910  exrecfnlem  37913  finxpeq1  37920  finxpreclem6  37930  pibp21  37949  curf  38137  uncf  38138  curunc  38141  unccur  38142  fin2so  38146  lindsadd  38152  lindsdom  38153  lindsenlbs  38154  matunitlindflem1  38155  matunitlindflem2  38156  matunitlindf  38157  ptrest  38158  ptrecube  38159  poimirlem2  38161  poimirlem8  38167  poimirlem17  38176  poimirlem18  38177  poimirlem20  38179  poimirlem21  38180  poimirlem22  38181  poimirlem24  38183  poimirlem26  38185  poimirlem29  38188  heicant  38194  mblfinlem1  38196  mblfinlem2  38197  volsupnfl  38204  itg2addnclem  38210  itg2gt0cn  38214  indexdom  38273  incsequz  38287  istotbnd  38308  istotbnd3  38310  0totbnd  38312  sstotbnd  38314  sstotbnd3  38315  isbnd  38319  prdstotbnd  38333  cntotbnd  38335  isismty  38340  heibor1lem  38348  heiborlem2  38351  heiborlem3  38352  heibor  38360  isass  38385  exidcl  38415  exidreslem  38416  elghomlem2OLD  38425  rngoidmlem  38475  rngo1cl  38478  divrngcl  38496  isdrngo2  38497  isrngohom  38504  isrngoiso  38517  isriscg  38523  iscom2  38534  iscringd  38537  isidl  38553  ispridl  38573  ismaxidl  38579  ac6s6  38711  dmecd  38849  dfpre4  39019  releldmqs  39282  releldmqscoss  39284  erimeq2  39302  qmapeldisjsim  39399  eldisjlem19  39452  membpartlem19  39453  prter3  39546  islshp  39643  islsat  39655  lcvfbr  39684  islfl  39724  ellkr  39753  islshpkrN  39784  ldual1dim  39830  isopos  39844  cmtfvalN  39874  cvrfval  39932  isat  39950  islln  40170  islpln  40194  islvol  40237  isline  40403  ispointN  40406  ispsubsp  40409  elpmap  40422  elpmapat  40428  elpadd  40463  paddclN  40506  elpclN  40556  elpcliN  40557  pclfinN  40564  pclcmpatN  40565  ispsubclN  40601  iswatN  40658  islhp  40660  islaut  40747  ispautN  40763  isldil  40774  isltrn  40783  isdilN  40818  istrnN  40821  istendo  41424  dvhb1dimN  41650  erng1lem  41651  erngdvlem4-rN  41663  diaelval  41697  diaeldm  41700  dia1dimid  41727  cdlemm10N  41782  dibopelvalN  41807  dibopelval2  41809  dibelval3  41811  dibelval1st  41813  dibelval2nd  41816  dibeldmN  41822  dibvalrel  41827  dibglbN  41830  dicffval  41838  dicfval  41839  dicopelval  41841  dicelvalN  41842  dicelval3  41844  dicvalrelN  41849  dicelval1sta  41851  diclspsn  41858  dihopelvalbN  41902  dihopelvalcqat  41910  dihopelvalcpre  41912  dihvalrel  41943  dih1  41950  dihmeetlem4preN  41970  dihmeetlem13N  41983  dih1dimatlem  41993  dochnel2  42056  dihjatcclem4  42085  dvh2dim  42109  dvh3dim  42110  dvh4dimN  42111  dochfln0  42141  lpolsetN  42146  islpolN  42147  lcfrvalsnN  42205  lcfrlem21  42227  lcfrlem27  42233  lcfrlem37  42243  lcfr  42249  lcdlss  42283  mapdcv  42324  hdmap1fval  42460  hdmapffval  42490  hdmapfval  42491  hdmapval  42492  hgmapffval  42549  hgmapfval  42550  hdmapellkr  42578  hlhilhillem  42624  fzsplitnd  42639  isprimroot  42750  primrootsunit1  42754  primrootscoprmpow  42756  primrootscoprbij  42759  aks6d1c1p2  42766  aks6d1c1p3  42767  aks6d1c1p4  42768  aks6d1c1p5  42769  aks6d1c1p6  42771  aks6d1c1  42773  evl1gprodd  42774  sticksstones11  42813  sticksstones12a  42814  rhmqusspan  42842  grpods  42851  fzosumm1  42908  frlmfielbas  43164  frlmsnic  43200  psrmnd  43203  isnacs  43327  mrefg2  43330  elmzpcl  43349  mzpcompact2  43375  eldiophb  43380  elpell1qr  43466  elpell14qr  43468  elpell1234qr  43470  pw2f1ocnv  43656  pw2f1o2val2  43659  aomclem4  43676  aomclem6  43678  islssfg2  43690  imasgim  43719  lnr2i  43735  elmnc  43755  rngunsnply  43788  onexomgt  43860  onexlimgt  43862  onexoegt  43863  oaordnr  43915  omnord1  43924  oenord1  43935  cantnfresb  43943  tfsconcatun  43956  tfsconcat0i  43964  ofoaf  43974  naddcnff  43981  naddcnffo  43983  naddcnfcom  43985  naddcnfid1  43986  naddcnfid2  43987  naddcnfass  43988  naddwordnexlem4  44020  fiinfi  44191  sqrtcvallem1  44249  elintima  44271  eliunov2  44297  ov2ssiunov2  44318  brtrclfv2  44345  rfovcnvf1od  44622  rfovcnvfvd  44625  fsovrfovd  44627  fsovfvd  44628  fsovcnvlem  44631  ntrclsfv1  44673  ntrclselnel1  44675  ntrclsneine0lem  44682  ntrneifv1  44697  ntrneifv2  44698  ntrneiel  44699  gneispace2  44750  gneispacess2  44764  extoimad  44782  mnringelbased  44833  dvconstbi  44936  bccbc  44947  wfac8prim  45603  permaxrep  45607  permac8prim  45615  eliin2f  45714  iineq12dv  45716  rabbida2  45742  disjinfi  45802  unirnmap  45816  elmptima  45865  iuneqfzuzlem  45942  iooiinioc  46164  fsumiunss  46183  fsumsupp0  46186  lptre2pt  46246  icccncfext  46493  cncfiooicclem1  46499  dvnprodlem2  46553  stoweidlem27  46633  stoweidlem29  46635  stoweidlem31  46637  stoweidlem34  46640  stoweidlem48  46654  stoweidlem59  46665  dirkercncflem2  46710  dirkercncflem4  46712  fourierdlem2  46715  fourierdlem3  46716  fourierdlem25  46738  fourierdlem32  46745  fourierdlem33  46746  fourierdlem41  46754  fourierdlem48  46760  fourierdlem49  46761  fourierdlem62  46774  fourierdlem70  46782  fourierdlem80  46792  fourierdlem92  46804  fourierdlem93  46805  fourierdlem101  46813  etransclem37  46877  sge0val  46972  sge0f1o  46988  sge0iunmptlemre  47021  sge0iunmpt  47024  iundjiun  47066  caragenel  47101  ovncvrrp  47170  ovnsubaddlem1  47176  ovnsubadd  47178  hoidmvlelem2  47202  hoidmvlelem3  47203  hoidmvlelem4  47204  hoidmvle  47206  ovncvr2  47217  hspdifhsp  47222  hoiqssbl  47231  hspmbllem2  47233  hspmbl  47235  opnvonmbllem1  47238  isvonmbl  47244  ovnovollem1  47262  issmflem  47333  smflimlem3  47379  smflimlem4  47380  smflim  47383  smfmullem2  47398  smflimmpt  47416  smfsuplem1  47417  smflimsuplem1  47426  smflimsuplem3  47428  smflimsuplem4  47429  smflimsuplem7  47432  smflimsup  47434  chnsubseq  47488  fcores  47693  fcoresf1  47695  afvelrnb  47789  afvelrnb0  47790  afv2co2  47883  el1fzopredsuc  47952  muldvdsfacm1  48013  iccpart  48054  iccpartgtprec  48058  iccpartiltu  48060  iccpartigtl  48061  iccpartltu  48063  iccpartgtl  48064  iccpartgt  48065  iccpartleu  48066  iccpartgel  48067  iccelpart  48071  iccpartiun  48072  icceuelpart  48074  fargshiftfv  48077  fargshiftfo  48080  sprel  48122  prprelb  48154  prprelprb  48155  nprmdvdsfacm1lem4  48264  fpprel  48382  sbgoldbo  48441  wtgoldbnnsum4prm  48456  bgoldbnnsum3prm  48458  bgoldbtbndlem3  48461  bgoldbtbnd  48463  clnbgrval  48476  elclnbgrelnbgr  48479  clnbgrel  48482  clnbupgrel  48488  vopnbgrel  48508  isubgredg  48520  upgrimwlklem3  48553  upgrimwlklem5  48555  upgrimpths  48563  grtriprop  48595  isgrtri  48597  grtriclwlk3  48599  stgredgel  48611  gpgvtxel  48701  gpgiedgdmel  48703  gpgedgel  48704  opgpgvtx  48709  gpg5nbgrvtx13starlem1  48725  gpg5nbgrvtx13starlem2  48726  gpg5nbgrvtx13starlem3  48727  gpg3kgrtriex  48743  grlimedgnedg  48785  upwlksfval  48789  isupwlk  48790  intop  48857  isclintop  48861  assintop  48863  isassintop  48864  assintopcllaw  48866  uzlidlring  48889  elrngchomALTV  48923  rngccatidALTV  48926  rngcsectALTV  48929  rngcisoALTV  48931  rhmsubcALTVlem3  48937  rhmsubcALTVlem4  48938  funcringcsetcALTV2lem7  48950  funcringcsetcALTV2lem9  48952  elringchomALTV  48957  ringccatidALTV  48960  ringcsectALTV  48963  ringcisoALTV  48965  ringcbasbasALTV  48966  funcringcsetclem7ALTV  48973  funcringcsetclem9ALTV  48975  srhmsubcALTV  48979  smprngprmrng  48993  cbvmpox2  49001  ply1sclrmsm  49049  dmatALTbasel  49067  lcoval  49077  lindslinindsimp1  49122  lindslinindsimp2  49128  lmod1  49157  elbigo  49216  elbigo2  49217  elbigolo1  49222  dig2nn0ld  49269  naryfvalel  49295  rrxlines  49398  rrxlinesc  49400  rrxlinec  49401  eenglngeehlnm  49404  elrrx2linest2  49410  rrxsphere  49413  itsclc0  49436  itsclc0b  49437  itsclinecirc0  49438  itsclinecirc0b  49439  itscnhlinecirc02p  49450  brab2dd  49491  f1omo  49556  f1omoOLD  49557  lubeldm2d  49621  glbeldm2d  49622  catprs  49674  sectpropdlem  49699  nelsubc3lem  49733  initc  49754  imaid  49817  upfval  49839  upfval2  49840  upfval3  49841  uppropd  49844  oppcinito  49898  oppctermo  49899  oppczeroo  49900  initopropd  49906  termopropd  49907  isthinc  50082  isthincd2lem1  50088  thincmoALT  50092  thincmod  50093  isthincd  50099  thincpropd  50105  indcthing  50123  discthing  50124  prsthinc  50127  termcterm  50176  termc2  50181  isinito4  50210  2arwcatlem1  50258  setc1onsubc  50265  cnelsubclem  50266  ranval3  50294  lmdfval2  50318  cmdfval2  50319  termolmd  50333  elsetrecslem  50362