Theorem eleq2d 2823

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eleq2  2826  eleq12d  2831  eleqtrd  2839  neleqtrd  2859  eqabrd  2878  raleqbidv  3312  rexeqbidv  3313  reueqbidv  3379  rabeqbidva  3406  elabd2  3613  sbcbid  3784  csbeq2d  3844  csbeq2dv  3845  cbvcsbw  3848  cbvcsb  3849  cbvcsbv  3850  csbie  3873  csbied  3874  csbie2g  3878  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  sbcel12  4352  sbcel1g  4357  sbcel2  4359  prel12g  4808  eliuni  4940  iuneqconst  4946  iuneq12df  4961  iuneq12d  4964  cbviun  4978  cbviin  4979  cbviung  4980  cbviing  4981  cbviunv  4982  cbviinv  4983  iinxsng  5031  iinxprg  5032  iunxsng  5033  iunxsngf  5035  cbvdisj  5063  cbvdisjv  5064  disjor  5068  disjiund  5077  mpteq12da  5169  mpteq12f  5171  mpteq12dva  5172  axpweq  5286  rabxfrd  5352  rbropapd  5508  opeliunxp  5689  opeliun2xp  5690  opeliunxp2  5785  iunxpf  5795  elimampt  6000  elrelimasn  6043  elimasni  6048  imadifssran  6107  xpdifid  6124  ressn  6241  funfni  6596  fnbr  6598  dffv3  6828  elfv2ex  6875  fvelrnb  6892  foelcdmi  6893  fvun1  6923  fvco2  6929  funcnvmpt  6941  elfvmptrab1w  6967  elfvmptrab1  6968  elfvmptrab  6969  elpreima  7002  dff3  7044  fmptco  7074  fnelfp  7121  fnelnfp  7123  tpres  7147  fnprb  7154  fntpb  7155  funfvima3  7182  eluniima  7196  dff13  7200  f1ounsn  7218  f1eqcocnv  7247  isoini  7284  riotaeqdv  7316  mpoeq123dva  7432  cbvmpox  7451  elimampo  7495  ovelrn  7534  elovmpod  7602  elovmpo  7603  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  elovmpt3rab1  7618  fiun  7887  f1iun  7888  zfrep6OLD  7899  fmpox  8011  el2mpocsbcl  8026  el2mpocl  8027  bropopvvv  8031  bropfvvvv  8033  xpord2indlem  8088  xpord3inddlem  8095  elsuppfng  8110  elsuppfn  8111  suppfnss  8130  opeliunxp2f  8151  mpoxopn0yelv  8154  mpoxopovel  8161  rntpos  8180  mpocurryd  8210  fpr2  8245  wfr2  8268  onoviun  8274  smoel  8291  smoiso  8293  smoel2  8294  smo11  8295  tfrlem9  8315  oalimcl  8486  oaass  8487  omordi  8492  omordlim  8503  omlimcl  8504  odi  8505  omeulem1  8508  omeulem2  8509  oen0  8513  oeordi  8514  oeordsuc  8521  oelimcl  8527  oeeulem  8528  oeeui  8529  nnmordi  8558  oaabs2  8576  omabs  8578  omsmolem  8584  ereldm  8688  iiner  8727  elmapg  8777  elpmg  8781  elixpsn  8876  ixpsnf1o  8877  boxriin  8879  omxpenlem  9007  pw2f1olem  9010  phplem2  9130  php3  9134  infn0  9203  elfi  9317  dffi3  9335  marypha2lem2  9340  ordiso2  9421  wemapsolem  9456  elharval  9467  inf3lemd  9537  inf3lem1  9538  inf3lem2  9539  inf3lem3  9540  cantnfs  9576  cantnfp1lem3  9590  cantnflem1b  9596  cantnflem1  9599  ttrclselem2  9636  trcl  9638  frr2  9673  r1sdom  9687  r1ordg  9691  r1pwss  9697  tz9.12lem3  9702  tz9.12  9703  r1elwf  9709  rankr1ai  9711  rankidb  9713  rankr1bg  9716  rankval2  9731  rankunb  9763  tcrank  9797  acni  9956  acni2  9957  acndom  9962  infpwfien  9973  alephnbtwn  9982  cardaleph  10000  cardinfima  10008  iunfictbso  10025  dfac3  10032  dfac5lem5  10038  dfac5  10040  dfac9  10048  dfac12r  10058  kmlem2  10063  kmlem12  10073  kmlem13  10074  kmlem14  10075  ackbij2lem3  10151  ackbij2  10153  cofsmo  10180  alephsing  10187  fin23lem30  10253  isf32lem9  10272  itunisuc  10330  axcc2lem  10347  axcc3  10349  domtriomlem  10353  axdc2lem  10359  axdc2  10360  axdc3lem2  10362  axdc3lem4  10364  axdc4lem  10366  ac6c4  10392  zorn2lem1  10407  ttukeylem6  10425  pwcfsdom  10495  axregndlem2  10515  axinfndlem1  10517  axacndlem4  10522  axacnd  10524  pwfseqlem1  10570  inar1  10687  inatsk  10690  gruurn  10710  grur1  10732  eltskm  10755  genpelv  10912  eluz1  12781  elixx1  13296  elixx3g  13300  elioo2  13328  elfz1  13455  elfz2  13457  elfzp1  13517  fzpr  13522  fzsuc2  13525  fzrev3  13533  elfzp12  13546  fzm1  13550  elfzo  13604  fz0add1fz1  13679  elfzo0l  13700  elfzom1b  13710  fzosplitsni  13723  elfzr  13725  elfzlmr  13726  zmodidfzo  13848  seqp1  13967  seqf1o  13994  bcval  14255  bcpasc  14272  hashf1lem1  14406  fundmge2nop0  14453  wrdmap  14497  elovmpowrd  14509  ccatfval  14524  elfzelfzccat  14531  ccatlid  14538  ccatass  14540  ccatrn  14541  ccatalpha  14545  swrdfv2  14613  ccatswrd  14620  swrdccat2  14621  pfxfv  14634  pfxeq  14647  ccatpfx  14652  swrdswrd  14656  swrdpfx  14658  pfxpfx  14659  cats1un  14672  swrdccatfn  14675  swrdccatin1  14676  pfxccatin12lem4  14677  pfxccatin12lem1  14679  swrdccatin2  14680  pfxccatin12lem2c  14681  pfxccatin12lem2  14682  swrdccat3blem  14690  swrdccatin1d  14694  swrdccatin2d  14695  pfxccatin12d  14696  revccat  14717  revrev  14718  repswpfx  14736  repswccat  14737  cshwidxmod  14754  2cshw  14764  cshwcshid  14778  cshwcsh2id  14779  cshimadifsn  14780  cshimadifsn0  14781  revco  14785  ccatco  14786  cshco  14787  swrdco  14788  ofccat  14920  shftfn  15024  shftval  15025  limsupgle  15428  ello12  15467  elo12  15478  isercolllem3  15618  sumeq1  15640  fsumsplit  15692  sumsplit  15719  fsum2dlem  15721  fsumcom2  15725  fsumparts  15758  explecnv  15819  pwdif  15822  fprodser  15903  fprodsplit  15920  fprod2dlem  15934  fprodcom2  15938  eftlub  16065  divalgmod  16364  bitsval  16382  bitsp1e  16390  bitsp1o  16391  sadfval  16410  sadcp1  16413  sadval  16414  sadcadd  16416  sadadd2  16418  saddisjlem  16422  sadadd  16425  sadass  16429  smufval  16435  smuval  16439  smuval2  16440  smupvallem  16441  smu01lem  16443  smueqlem  16448  smumul  16451  bezoutlem2  16498  bezoutlem4  16500  algfx  16538  eucalgcvga  16544  reumodprminv  16764  nnnn0modprm0  16766  unbenlem  16868  prmreclem5  16880  vdwapval  16933  vdwapun  16934  vdwnnlem1  16955  vdwnn  16958  ramval  16968  0ram  16980  ramub1lem2  16987  prmgaplem7  17017  prmlem0  17065  elrest  17379  prdsbasmpt  17422  prdsleval  17429  prdsbasmpt2  17434  pwselbasb  17440  imasaddfnlem  17481  imasvscafn  17490  divsfval  17500  ismre  17541  mreunirn  17552  mrisval  17585  ismri  17586  isacs  17606  catidd  17635  iscatd2  17636  ismon  17689  isepi  17696  sectffval  17706  sectfval  17707  dfiso2  17728  cicsym  17760  issubc  17791  catsubcat  17795  isfunc  17820  funcres  17852  funcpropd  17858  ffthiso  17887  isnat  17906  isnat2  17907  fuciso  17934  initoval  17949  termoval  17950  isinito  17952  istermo  17953  iszeroo  17954  isinitoi  17955  istermoi  17956  initoid  17957  termoid  17958  iszeroi  17965  2initoinv  17966  initoeu1  17967  initoeu2  17972  2termoinv  17973  termoeu1  17974  arwhoma  18001  elsetchom  18037  setcmon  18043  setcepi  18044  setciso  18047  catciso  18067  elestrchom  18083  estrcbasbas  18086  funcestrcsetclem7  18101  funcestrcsetclem8  18102  funcestrcsetclem9  18103  fthestrcsetc  18105  fullestrcsetc  18106  equivestrcsetc  18107  setc1strwun  18108  funcsetcestrclem7  18116  funcsetcestrclem8  18117  funcsetcestrclem9  18118  fthsetcestrc  18120  fullsetcestrc  18121  hofcl  18214  hofpropd  18222  yonedalem4c  18232  yonedainv  18236  yonffthlem  18237  lubeldm  18306  glbeldm  18319  joindef  18329  meetdef  18343  poslubdg  18367  acsficl2d  18507  acsmapd  18509  psref  18529  psss  18535  dirge  18558  chnccats1  18580  chnccat  18581  chnrev  18582  mgmpropd  18608  issstrmgm  18610  grpidval  18618  grpidpropd  18619  grpidd  18628  ismgmhm  18653  issubmgm  18659  issgrpd  18687  sgrppropd  18688  ismndd  18713  mndpropd  18716  imasmnd2  18731  imasmnd  18732  xpsmnd0  18735  ismhm  18742  issubm  18760  gsumsgrpccat  18797  elefmndbas2  18831  smndex1mndlem  18869  imasgrp2  19020  imasgrp  19021  issubg  19091  subginv  19098  isnsg  19119  eqg0el  19147  quselbas  19148  isghm  19179  isghmOLD  19180  resghm2b  19198  conjnmzb  19217  conjnsg  19218  ghmpropd  19220  isga  19255  elcntz  19286  elcntzsn  19289  cntzrcl  19291  resscntz  19297  symgextf1  19385  gsmsymgreqlem2  19395  f1otrspeq  19411  pmtrfrn  19422  pmtrdifellem3  19442  pmtrdifellem4  19443  psgnunilem1  19457  psgnunilem5  19458  psgnunilem2  19459  psgnunilem3  19460  psgneldm2  19468  psgnfitr  19481  psgnsn  19484  gexdvds  19548  gex1  19555  isslw  19572  sylow3lem2  19592  lsmelvalx  19604  pj1ghm  19667  efgtlen  19690  efgsfo  19703  efgredlemc  19709  frgp0  19724  frgpmhm  19729  qusabl  19829  frgpnabllem1  19837  imasabl  19840  cycsubmcmn  19853  0cyg  19857  cycsubgcyg  19865  gsumval3  19871  gsumcllem  19872  gsumzaddlem  19885  gsumzsplit  19891  gsummptfzcl  19933  eldprd  19970  dprdcntz2  20004  dprd2d2  20010  dmdprdsplit2lem  20011  dmdprdsplit2  20012  dprdsplit  20014  ablfac2  20055  isrngd  20143  rngpropd  20144  imasrng  20147  qusrng  20150  ringurd  20155  isringd  20261  imasring  20299  xpsring1d  20302  dvdsrval  20330  isunit  20342  dvdsrpropd  20385  isirred  20388  isrnghm  20410  isrngim  20414  c0ghm  20430  c0snghm  20433  isrhm  20447  isrim0  20451  islring  20506  issubrng  20513  opprsubrng  20525  issubrg  20537  opprsubrg  20559  resrhm2b  20568  rhmpropd  20575  rnghmresel  20586  elrngchom  20590  rnghmsubcsetclem1  20597  rnghmsubcsetclem2  20598  rngcid  20601  rngcsect  20602  rngciso  20604  funcrngcsetcALT  20607  zrinitorngc  20608  zrtermorngc  20609  rhmresel  20615  elringchom  20619  rhmsubcsetclem1  20626  rhmsubcsetclem2  20627  ringcid  20630  rhmsscrnghm  20631  rhmsubcrngclem1  20632  rhmsubcrngclem2  20633  ringcsect  20636  ringciso  20638  ringcbasbas  20639  zrtermoringc  20641  srhmsubc  20646  rhmsubclem3  20653  rhmsubclem4  20654  drngunit  20700  isdrngd  20731  isdrngdOLD  20733  issdrg  20754  sdrgunit  20762  isabv  20777  issrngd  20821  islmod  20848  lmodprop2d  20908  islss  20918  islssd  20919  lssats2  20984  ellspsn  20987  islmhm  21012  lmhmf1o  21031  lmhmima  21032  lmhmpreima  21033  reslmhm  21037  pwssplit3  21046  lmhmpropd  21058  islbs  21061  lspprel  21079  lspfixed  21116  lbsacsbs  21144  lbsextlem1  21146  lbsextlem2  21147  lbsextlem3  21148  lbsextlem4  21149  ixpsnbasval  21193  isridlrng  21207  rnglidlmmgm  21233  isridl  21240  quscrng  21271  rngqiprngimfolem  21278  rngqiprngimf1lem  21282  rngqiprngimfo  21289  islpidl  21313  lidldvgen  21322  irinitoringc  21467  pzriprnglem13  21481  pzriprnglem14  21482  zrhrhmb  21498  znf1o  21539  frgpcyg  21561  psgnevpmb  21575  isphld  21642  phlssphl  21647  elocv  21656  iscss  21671  isobs  21708  obs2ss  21717  dsmmfi  21726  dsmmelbas  21727  dsmmlss  21732  frlmelbas  21744  frlmlbs  21785  frlmup1  21786  ellspd  21790  islinds  21797  islindf2  21802  f1lindf  21810  islindf4  21826  assamulgscmlem2  21888  psrgrp  21944  mplsubglem  21986  mpllsslem  21987  mplmonmul  22023  subrgascl  22053  subrgasclcl  22054  mpfind  22102  ismhp  22115  gsumply1subr  22206  lply1binomsc  22285  matbas2d  22397  matecl  22399  matvscl  22405  mat1  22421  mat0dim0  22441  mat0dimid  22442  mat0dimscm  22443  mat1dimelbas  22445  dmatel  22467  scmatel  22479  scmateALT  22486  scmataddcl  22490  scmatsubcl  22491  smatvscl  22498  scmatghm  22507  mat1scmat  22513  mdetunilem7  22592  mdetunilem9  22594  smadiadetr  22649  cramerimplem2  22658  cramer0  22664  pmatcoe1fsupp  22675  cpmatpmat  22684  cpmatel  22685  cpmatacl  22690  cpmatinvcl  22691  mat2pmatghm  22704  mat2pmatmul  22705  decpmatmullem  22745  pmatcollpwlem  22754  pmatcollpw3fi1lem1  22760  pmatcollpwscmatlem1  22763  monmat2matmon  22798  chfacfscmul0  22832  chfacfscmulgsum  22834  chfacfpmmulgsum  22838  cayhamlem1  22840  cpmadugsumlemB  22848  cpmadugsumlemC  22849  cpmadugsumlemF  22850  cayhamlem2  22858  istopon  22886  eltg  22931  eltg2  22932  eltop  22948  eltop2  22949  eltop3  22950  pptbas  22982  iscld  23001  neiss2  23075  isnei  23077  neiptopnei  23106  neiptopreu  23107  lpfval  23112  lpval  23113  islp  23114  maxlp  23121  islpi  23123  neitr  23154  restlp  23157  ordtbas2  23165  ordtrest2  23178  lmfval  23206  cnfval  23207  iscn  23209  iscnp  23211  tgcn  23226  tgcnp  23227  lmbrf  23234  cnpresti  23262  ist1  23295  ist1-2  23321  cnt1  23324  haust1  23326  cmpfi  23382  cmpfii  23383  1stcfb  23419  2ndc1stc  23425  1stcrest  23427  2ndcdisj  23430  1stcelcls  23435  nllyi  23449  subislly  23455  islocfin  23491  lfinpfin  23498  locfindis  23504  locfincf  23505  comppfsc  23506  kgenval  23509  elkgen  23510  kgencn2  23531  txbas  23541  eltx  23542  ptval  23544  ptpjpre1  23545  ptopn2  23558  ptpjopn  23586  ptclsg  23589  xkoccn  23593  txdis  23606  txdis1cn  23609  ptrescn  23613  hausdiag  23619  hauseqlcld  23620  txhaus  23621  xkohaus  23627  elqtop  23671  qtopeu  23690  kqcldsat  23707  hmeofval  23732  ptuncnv  23781  ptunhmeo  23782  elmptrab  23801  fbdmn0  23808  elfg  23845  elfilss  23850  filunirn  23856  fixufil  23896  elfm  23921  rnelfmlem  23926  rnelfm  23927  fmfnfmlem4  23931  elflim2  23938  flimtopon  23944  elflim  23945  hausflim  23955  flimcls  23959  flfnei  23965  isflf  23967  hausflf  23971  cnpflf  23975  cnflf  23976  txflf  23980  isfcls  23983  fclstopon  23986  isfcls2  23987  fclssscls  23992  fclsnei  23993  fclsfnflim  24001  flimfnfcls  24002  isfcf  24008  fcfelbas  24010  cnpfcf  24015  cnfcf  24016  flfcntr  24017  alexsublem  24018  alexsubALTlem3  24023  cnextfun  24038  cnextfvval  24039  cnextf  24040  cnextcn  24041  tmdgsum2  24070  tgpconncomp  24087  ghmcnp  24089  qustgplem  24095  eltsms  24107  haustsms  24110  tsmsgsum  24113  tsmssubm  24117  tsmssplit  24126  isust  24178  ustbas  24201  elutop  24207  ustuqtoplem  24213  ustuqtop4  24218  ustuqtop  24220  utopsnneiplem  24221  utopsnneip  24222  utopsnnei  24223  isusp  24235  isucn  24251  ucncn  24258  iscfilu  24261  neipcfilu  24269  iscusp  24272  cnextucn  24276  ispsmet  24278  ismet  24297  isxmet  24298  elblps  24361  elbl  24362  elmopn  24416  prdsbl  24465  neibl  24475  met1stc  24495  metrest  24498  prdsxmslem2  24503  txmetcnp  24521  txmetcn  24522  metustsym  24529  cfilucfil2  24535  elbl4  24537  metuel  24538  psmetutop  24541  restmetu  24544  metucn  24545  tngngp  24628  isnmhm  24720  zcld  24788  metnrmlem1a  24833  elcncf  24865  cncfcnvcn  24901  cnheibor  24931  lebnumlem1  24937  ishtpy  24948  isphtpy  24957  om1elbas  25008  elpi1  25021  pi1xfr  25031  pi1coghm  25037  tcphcph  25213  lmmbrf  25238  iscfil  25241  iscau  25252  iscauf  25256  caucfil  25259  iscmet  25260  cmetcaulem  25264  iscmet3lem1  25267  iscmet3lem2  25268  iscmet3  25269  bcthlem1  25300  cmsss  25327  cmetcusp1  25329  cmetcusp  25330  cmscsscms  25349  rrxcph  25368  minveclem3b  25404  ovolfioo  25443  ovolficc  25444  ovolctb  25466  ovoliunnul  25483  ovolshftlem1  25485  sca2rab  25488  ovolscalem1  25489  ovolicc2lem1  25493  ovolicc2lem2  25494  ovolicc2lem4  25496  ovolicc2lem5  25497  iundisj  25524  iunmbl2  25533  uniioombllem3  25561  vitalilem2  25585  vitalilem3  25586  mbfss  25622  i1faddlem  25669  i1fmullem  25670  mbfi1fseqlem2  25692  mbfi1fseqlem4  25694  mbfi1fseq  25697  itg2splitlem  25724  itg2split  25725  itg2monolem1  25726  itg2gt0  25736  isibl  25741  iblss2  25782  itgss3  25791  itgsplit  25812  ellimc  25849  limcmo  25858  cnlimc  25864  limciun  25870  limcun  25871  eldv  25874  dvbsss  25878  dvreslem  25885  elcpn  25910  dvaddf  25918  dvmulf  25919  dvcof  25924  rolle  25966  dvlip2  25972  dvivthlem1  25985  lhop1  25991  lhop2  25992  ftc1cn  26022  fta1glem2  26146  plyco0  26169  elply  26172  ply1termlem  26180  eltayl  26338  tayl0  26340  taylplem1  26341  taylplem2  26342  dvtaylp  26349  taylthlem1  26352  taylthlem2  26353  taylthlem2OLD  26354  abelth  26422  cxpcn3  26729  rlimcnp  26946  fsumharmonic  26993  dchrelbas  27218  pntrsumbnd2  27549  ostth2lem2  27616  nolesgn2ores  27655  nogesgn1ores  27657  nosupprefixmo  27683  noinfprefixmo  27684  nosupcbv  27685  nosupdm  27687  nosupfv  27689  nosupres  27690  nosupbnd1lem1  27691  nosupbnd1lem3  27693  nosupbnd1lem5  27695  nosupbnd2lem1  27698  noinfcbv  27700  noinfdm  27702  noinffv  27704  noinfres  27705  noinfbnd1lem1  27706  noinfbnd1lem3  27708  noinfbnd1lem5  27710  noinfbnd2lem1  27713  elmade  27868  elold  27870  sltsleft  27871  sltsright  27872  oldlim  27898  madebday  27911  newbday  27913  ltslpss  27919  bdayiun  27926  cofcutr  27935  cofcutrtime  27938  lrrecval  27950  lrrecval2  27951  addsval  27973  precsexlem9  28226  precsexlem11  28228  ltonold  28272  onnolt  28277  onlts  28278  noseqrdgfn  28317  istrkgb  28542  istrkgcb  28543  istrkge  28544  istrkgl  28545  istrkgld  28546  axtgsegcon  28551  axtg5seg  28552  axtgbtwnid  28553  axtgpasch  28554  axtgupdim2  28558  axtgeucl  28559  tgdim01  28594  iscgrg  28599  isismt  28621  tglnunirn  28635  tglngval  28638  tgellng  28640  legval  28671  legov  28672  legov2  28673  ishlg  28689  mirreu3  28741  mirval  28742  mirfv  28743  mircgr  28744  mirbtwn  28745  ismir  28746  mireq  28752  symquadlem  28776  israg  28784  perpln1  28797  perpln2  28798  isperp  28799  islnopp  28826  outpasch  28842  ishpg  28846  iscgra  28896  dfcgra2  28917  isinag  28925  isleag  28934  iseqlg  28954  f1otrgitv  28957  f1otrg  28958  f1otrge  28959  ttgval  28962  ttgelitv  28970  elee  28981  brbtwn  28987  brcgr  28988  axlowdimlem16  29045  ebtwntg  29070  elntg2  29073  upgrex  29180  edgupgr  29222  upgredg  29225  edglnl  29231  numedglnl  29232  uhgr2edg  29296  umgr2edg1  29299  usgredg2vlem1  29313  usgredg2vlem2  29314  ushgredgedg  29317  ushgredgedgloop  29319  uhgrspansubgrlem  29378  fusgrfisstep  29417  nbgrval  29424  nbgrel  29428  nbupgrel  29433  nbgr2vtx1edg  29438  nbuhgr2vtx1edgblem  29439  nbuhgr2vtx1edgb  29440  nbusgreledg  29441  usgrnbcnvfv  29453  uvtxval  29475  uvtxel  29476  uvtx01vtx  29485  uvtxusgrel  29491  nbcplgr  29522  cplgr3v  29523  cusgrexi  29531  structtocusgr  29534  vtxdgfval  29556  vtxdg0v  29562  vtxdeqd  29566  vtxdun  29570  1loopgrnb0  29591  1loopgrvd0  29593  1hevtxdg0  29594  1hevtxdg1  29595  1egrvtxdg1  29598  umgr2v2evtxel  29611  umgr2v2enb1  29615  umgr2v2evd2  29616  vtxdginducedm1lem4  29631  vtxdginducedm1  29632  finsumvtxdg2sstep  29638  ewlksfval  29690  isewlk  29691  wksfval  29698  iswlk  29699  uspgr2wlkeq  29734  wlkres  29757  dfpth2  29817  usgr2pthlem  29851  clwlkcompim  29868  uspgrn2crct  29896  wwlks  29923  iswwlksn  29926  wwlknvtx  29933  wlkiswwlks2  29963  wwlksm1edg  29969  wwlksnred  29980  wwlksnext  29981  wwlksnredwwlkn  29983  wwlksnredwwlkn0  29984  wwlksnwwlksnon  30003  wspn0  30012  usgr2wspthons3  30055  rusgrnumwwlkb0  30062  clwwlk  30073  clwwlkccatlem  30079  clwlkclwwlklem2a4  30087  clwlkclwwlk  30092  clwwisshclwwslem  30104  clwwlkinwwlk  30130  clwwlkel  30136  clwwlkf  30137  clwwlkext2edg  30146  wwlksext2clwwlk  30147  wwlksubclwwlk  30148  clwwnisshclwwsn  30149  eleclclwwlknlem2  30151  erclwwlknsym  30160  erclwwlkntr  30161  umgrhashecclwwlk  30168  clwwlkvbij  30203  eupth2lem3lem3  30320  eupth2lem3lem4  30321  eupth2lem3lem6  30323  eupth2lemb  30327  eucrct2eupth  30335  fusgreg2wsplem  30423  2clwwlklem  30433  2clwwlk2clwwlklem  30436  2clwwlkel  30439  2clwwlk2clwwlk  30440  extwwlkfabel  30443  clwwlknonclwlknonf1o  30452  dlwwlknondlwlknonf1olem1  30454  numclwwlk2lem1  30466  numclwlk2lem2f  30467  numclwlk2lem2f1o  30469  ex-res  30531  isssp  30815  sspn  30827  islno  30844  isblo  30873  nmlno0  30886  ishmo  30902  dipdir  30933  dipass  30936  ubthlem1  30961  ubthlem2  30962  htthlem  31008  htth  31009  ocel  31372  ocnel  31389  shsel  31405  shsel2  31413  shmodsi  31480  pjhtheu  31485  pjeq  31490  axpjpj  31511  pjoc2  31530  elspani  31634  h1de2ctlem  31646  elspansn  31657  elspansn2  31658  elnlfn  32019  eleigvec  32048  riesz3i  32153  cbviunf  32645  iuneq12daf  32646  iunrdx  32653  iunrnmptss  32655  cbvdisjf  32661  disjorf  32669  disjabrex  32672  disjabrexf  32673  iundisjf  32679  disjrdx  32681  brab2d  32698  fresunsn  32718  2ndresdju  32742  abfmpunirn  32745  abfmpeld  32747  abfmpel  32748  fmptcof2  32750  acunirnmpt2  32753  acunirnmpt2f  32754  aciunf1lem  32755  suppss3  32816  fpwrelmap  32826  xrofsup  32860  iundisjfi  32889  eliccioo  33010  s3f1  33027  ccatf1  33029  ccatws1f1o  33031  swrdrn3  33035  ismnt  33063  mgcoval  33066  gsummpt2co  33129  gsumpart  33144  gsumhashmul  33148  gsummulsubdishift1  33149  xrge0tsmsbi  33155  gsumwrd2dccatlem  33158  gsumwrd2dccat  33159  cycpmco2  33214  cyc3co2  33221  isfxp  33249  cntrval2  33252  inftmrel  33261  isinftm  33262  isslmd  33283  urpropd  33312  elrgspn  33327  erlval  33339  rlocval  33340  rloccring  33351  rloc1r  33353  domnprodeq0  33357  domnpropd  33358  isdrng4  33376  fracfld  33389  resv1r  33419  ellspds  33448  ellpi  33453  lbslsp  33457  rhmimaidl  33512  isprmidl  33518  qsidomlem1  33532  qsidomlem2  33533  ismxidl  33542  crngmxidl  33549  drng0mxidl  33556  opprqus0g  33570  qsfld  33578  isrprm  33597  rsprprmprmidlb  33603  ressply1evls1  33645  ply1mulrtss  33662  ply1coedeg  33669  psrmonmul  33714  dimpropd  33773  lbslsat  33781  extdg1id  33831  fldextrspunlsplem  33838  fldextrspunlsp  33839  elirng  33851  ply1annidllem  33866  constrsuc  33903  constrconj  33910  constrllcllem  33917  constrlccllem  33918  constrcccllem  33919  nn0constr  33926  smatrcl  33961  smatcl  33967  ist0cld  33998  txomap  33999  locfinreflem  34005  zarclsiin  34036  zart0  34044  rhmpreimacnlem  34049  metidval  34055  cnre2csqima  34076  ordtrest2NEW  34088  fmcncfil  34096  fsumcvg4  34115  ofcfval  34263  measvuni  34379  meascnbl  34384  faeval  34411  ismbfm  34416  elunirnmbfm  34417  imambfm  34427  elcarsg  34470  itgeq12dv  34491  issibf  34498  eulerpartlems  34525  eulerpartlemgc  34527  eulerpartlemgvv  34541  eulerpartlemgu  34542  eulerpart  34547  rrvmbfm  34607  elorvc  34625  elorrvc  34629  dstfrvunirn  34640  ballotlemfc0  34658  ballotlemfcc  34659  ballotlemsima  34681  ballotlemrv  34685  fzssfzo  34704  signstfvn  34734  signstfvneq0  34737  signstres  34740  repr0  34776  reprinrn  34783  reprdifc  34792  hgt750lemg  34819  hgt750lemb  34821  istrkg2d  34831  axtgupdim2ALTV  34833  afsval  34836  brafs  34837  bnj945  34937  bnj1400  34998  bnj18eq1  35090  bnj916  35096  bnj1014  35124  bnj1015  35125  bnj1110  35145  bnj1417  35204  rankval2b  35263  r1filimi  35267  r1ssel  35271  onvf1odlem3  35308  vonf1owev  35311  revpfxsfxrev  35319  cplgredgex  35324  pfxwlk  35327  revwlk  35328  subfacp1lem2b  35384  subfacp1lem4  35386  subfacp1lem5  35387  subfacp1lem6  35388  ptpconn  35436  cvmscbv  35461  iscvm  35462  cvmsi  35468  cvmsval  35469  cvmliftmolem1  35484  cvmlift2lem12  35517  cvmlift2lem13  35518  cvmlift3lem7  35528  snmlval  35534  satfv1  35566  satfvsucsuc  35568  satfrnmapom  35573  satf0op  35580  satf0n0  35581  sat1el2xp  35582  fmlafvel  35588  isfmlasuc  35591  fmlaomn0  35593  gonan0  35595  goaln0  35596  gonar  35598  goalr  35600  satffunlem1lem2  35606  satffunlem2lem2  35609  satfv0fvfmla0  35616  satef  35619  satefvfmla0  35621  sategoelfvb  35622  satfv1fvfmla1  35626  mrsubfval  35711  mrsubvrs  35725  mclsrcl  35764  mclsval  35766  mppsval  35775  mclsppslem  35786  opelco3  35978  wsuclem  36026  funtransport  36234  fvtransport  36235  brcolinear  36262  colineardim1  36264  funray  36343  fvray  36344  funline  36345  fvline  36347  lineelsb2  36351  fwddifval  36365  fwddifnval  36366  rankelg  36371  rankeq1o  36374  elhf2  36378  0hf  36380  rmoeqbidv  36416  disjeq12dv  36418  ixpeq12dv  36419  prodeq12sdv  36421  itgeq12sdv  36422  cbvralvw2  36429  cbvrexvw2  36430  cbvrmovw2  36431  cbvreuvw2  36432  cbvcsbvw2  36434  cbviunvw2  36435  cbviinvw2  36436  cbvmptvw2  36437  cbvdisjvw2  36438  cbvmpo1vw2  36446  cbvmpo2vw2  36447  cbvsbcdavw  36460  cbvcsbdavw  36462  cbvcsbdavw2  36463  cbviundavw  36465  cbviindavw  36466  cbvdisjdavw  36471  cbvrabdavw2  36488  cbviundavw2  36489  cbviindavw2  36490  cbvmptdavw2  36491  cbvdisjdavw2  36492  cbvriotadavw2  36493  cbvmpo1davw2  36495  cbvmpo2davw2  36496  cbvsumdavw2  36498  neibastop2lem  36563  neibastop3  36565  eltail  36577  ttctr  36696  dfttc2g  36709  bj-projeq  37312  bj-projval  37316  bj-restsn  37407  opelopabbv  37470  brabd0  37474  bj-eldiag  37503  bj-eldiag2  37504  mptsnunlem  37665  dissneqlem  37667  iooelexlt  37689  relowlssretop  37690  rdgellim  37703  exrecfnlem  37706  finxpeq1  37713  finxpreclem6  37723  pibp21  37742  curf  37930  uncf  37931  curunc  37934  unccur  37935  fin2so  37939  lindsadd  37945  lindsdom  37946  lindsenlbs  37947  matunitlindflem1  37948  matunitlindflem2  37949  matunitlindf  37950  ptrest  37951  ptrecube  37952  poimirlem2  37954  poimirlem8  37960  poimirlem17  37969  poimirlem18  37970  poimirlem20  37972  poimirlem21  37973  poimirlem22  37974  poimirlem24  37976  poimirlem26  37978  poimirlem29  37981  heicant  37987  mblfinlem1  37989  mblfinlem2  37990  volsupnfl  37997  itg2addnclem  38003  itg2gt0cn  38007  indexdom  38066  incsequz  38080  istotbnd  38101  istotbnd3  38103  0totbnd  38105  sstotbnd  38107  sstotbnd3  38108  isbnd  38112  prdstotbnd  38126  cntotbnd  38128  isismty  38133  heibor1lem  38141  heiborlem2  38144  heiborlem3  38145  heibor  38153  isass  38178  exidcl  38208  exidreslem  38209  elghomlem2OLD  38218  rngoidmlem  38268  rngo1cl  38271  divrngcl  38289  isdrngo2  38290  isrngohom  38297  isrngoiso  38310  isriscg  38316  iscom2  38327  iscringd  38330  isidl  38346  ispridl  38366  ismaxidl  38372  ac6s6  38504  dmecd  38642  dfpre4  38812  releldmqs  39075  releldmqscoss  39077  erimeq2  39095  qmapeldisjsim  39192  eldisjlem19  39245  membpartlem19  39246  prter3  39339  islshp  39436  islsat  39448  lcvfbr  39477  islfl  39517  ellkr  39546  islshpkrN  39577  ldual1dim  39623  isopos  39637  cmtfvalN  39667  cvrfval  39725  isat  39743  islln  39963  islpln  39987  islvol  40030  isline  40196  ispointN  40199  ispsubsp  40202  elpmap  40215  elpmapat  40221  elpadd  40256  paddclN  40299  elpclN  40349  elpcliN  40350  pclfinN  40357  pclcmpatN  40358  ispsubclN  40394  iswatN  40451  islhp  40453  islaut  40540  ispautN  40556  isldil  40567  isltrn  40576  isdilN  40611  istrnN  40614  istendo  41217  dvhb1dimN  41443  erng1lem  41444  erngdvlem4-rN  41456  diaelval  41490  diaeldm  41493  dia1dimid  41520  cdlemm10N  41575  dibopelvalN  41600  dibopelval2  41602  dibelval3  41604  dibelval1st  41606  dibelval2nd  41609  dibeldmN  41615  dibvalrel  41620  dibglbN  41623  dicffval  41631  dicfval  41632  dicopelval  41634  dicelvalN  41635  dicelval3  41637  dicvalrelN  41642  dicelval1sta  41644  diclspsn  41651  dihopelvalbN  41695  dihopelvalcqat  41703  dihopelvalcpre  41705  dihvalrel  41736  dih1  41743  dihmeetlem4preN  41763  dihmeetlem13N  41776  dih1dimatlem  41786  dochnel2  41849  dihjatcclem4  41878  dvh2dim  41902  dvh3dim  41903  dvh4dimN  41904  dochfln0  41934  lpolsetN  41939  islpolN  41940  lcfrvalsnN  41998  lcfrlem21  42020  lcfrlem27  42026  lcfrlem37  42036  lcfr  42042  lcdlss  42076  mapdcv  42117  hdmap1fval  42253  hdmapffval  42283  hdmapfval  42284  hdmapval  42285  hgmapffval  42342  hgmapfval  42343  hdmapellkr  42371  hlhilhillem  42417  fzsplitnd  42432  isprimroot  42543  primrootsunit1  42547  primrootscoprmpow  42549  primrootscoprbij  42552  aks6d1c1p2  42559  aks6d1c1p3  42560  aks6d1c1p4  42561  aks6d1c1p5  42562  aks6d1c1p6  42564  aks6d1c1  42566  evl1gprodd  42567  sticksstones11  42606  sticksstones12a  42607  rhmqusspan  42635  grpods  42644  fzosumm1  42700  frlmfielbas  42956  frlmsnic  42996  psrmnd  42999  isnacs  43147  mrefg2  43150  elmzpcl  43169  mzpcompact2  43195  eldiophb  43200  elpell1qr  43290  elpell14qr  43292  elpell1234qr  43294  pw2f1ocnv  43480  pw2f1o2val2  43483  aomclem4  43500  aomclem6  43502  islssfg2  43514  imasgim  43543  lnr2i  43559  elmnc  43579  rngunsnply  43612  onexomgt  43684  onexlimgt  43686  onexoegt  43687  oaordnr  43739  omnord1  43748  oenord1  43759  cantnfresb  43767  tfsconcatun  43780  tfsconcat0i  43788  ofoaf  43798  naddcnff  43805  naddcnffo  43807  naddcnfcom  43809  naddcnfid1  43810  naddcnfid2  43811  naddcnfass  43812  naddwordnexlem4  43844  fiinfi  44015  sqrtcvallem1  44073  elintima  44095  eliunov2  44121  ov2ssiunov2  44142  brtrclfv2  44169  rfovcnvf1od  44446  rfovcnvfvd  44449  fsovrfovd  44451  fsovfvd  44452  fsovcnvlem  44455  ntrclsfv1  44497  ntrclselnel1  44499  ntrclsneine0lem  44506  ntrneifv1  44521  ntrneifv2  44522  ntrneiel  44523  gneispace2  44574  gneispacess2  44588  extoimad  44606  mnringelbased  44659  dvconstbi  44776  bccbc  44787  wfac8prim  45444  permaxrep  45448  permac8prim  45456  eliin2f  45549  iineq12dv  45551  rabbida2  45577  disjinfi  45637  unirnmap  45652  elmptima  45702  iuneqfzuzlem  45779  iooiinioc  46001  fsumiunss  46020  fsumsupp0  46023  lptre2pt  46083  icccncfext  46330  cncfiooicclem1  46336  dvnprodlem2  46390  stoweidlem27  46470  stoweidlem29  46472  stoweidlem31  46474  stoweidlem34  46477  stoweidlem48  46491  stoweidlem59  46502  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem2  46552  fourierdlem3  46553  fourierdlem25  46575  fourierdlem32  46582  fourierdlem33  46583  fourierdlem41  46591  fourierdlem48  46597  fourierdlem49  46598  fourierdlem62  46611  fourierdlem70  46619  fourierdlem80  46629  fourierdlem92  46641  fourierdlem93  46642  fourierdlem101  46650  etransclem37  46714  sge0val  46809  sge0f1o  46825  sge0iunmptlemre  46858  sge0iunmpt  46861  iundjiun  46903  caragenel  46938  ovncvrrp  47007  ovnsubaddlem1  47013  ovnsubadd  47015  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  hoidmvle  47043  ovncvr2  47054  hspdifhsp  47059  hoiqssbl  47068  hspmbllem2  47070  hspmbl  47072  opnvonmbllem1  47075  isvonmbl  47081  ovnovollem1  47099  issmflem  47170  smflimlem3  47216  smflimlem4  47217  smflim  47220  smfmullem2  47235  smflimmpt  47253  smfsuplem1  47254  smflimsuplem1  47263  smflimsuplem3  47265  smflimsuplem4  47266  smflimsuplem7  47269  smflimsup  47271  chnsubseq  47323  fcores  47512  fcoresf1  47514  afvelrnb  47608  afvelrnb0  47609  afv2co2  47702  el1fzopredsuc  47771  muldvdsfacm1  47832  iccpart  47873  iccpartgtprec  47877  iccpartiltu  47879  iccpartigtl  47880  iccpartltu  47882  iccpartgtl  47883  iccpartgt  47884  iccpartleu  47885  iccpartgel  47886  iccelpart  47890  iccpartiun  47891  icceuelpart  47893  fargshiftfv  47896  fargshiftfo  47899  sprel  47941  prprelb  47973  prprelprb  47974  nprmdvdsfacm1lem4  48083  fpprel  48201  sbgoldbo  48260  wtgoldbnnsum4prm  48275  bgoldbnnsum3prm  48277  bgoldbtbndlem3  48280  bgoldbtbnd  48282  clnbgrval  48295  elclnbgrelnbgr  48298  clnbgrel  48301  clnbupgrel  48307  vopnbgrel  48327  isubgredg  48339  upgrimwlklem3  48372  upgrimwlklem5  48374  upgrimpths  48382  grtriprop  48414  isgrtri  48416  grtriclwlk3  48418  stgredgel  48430  gpgvtxel  48520  gpgiedgdmel  48522  gpgedgel  48523  opgpgvtx  48528  gpg5nbgrvtx13starlem1  48544  gpg5nbgrvtx13starlem2  48545  gpg5nbgrvtx13starlem3  48546  gpg3kgrtriex  48562  grlimedgnedg  48604  upwlksfval  48608  isupwlk  48609  intop  48676  isclintop  48680  assintop  48682  isassintop  48683  assintopcllaw  48685  uzlidlring  48708  elrngchomALTV  48742  rngccatidALTV  48745  rngcsectALTV  48748  rngcisoALTV  48750  rhmsubcALTVlem3  48756  rhmsubcALTVlem4  48757  funcringcsetcALTV2lem7  48769  funcringcsetcALTV2lem9  48771  elringchomALTV  48776  ringccatidALTV  48779  ringcsectALTV  48782  ringcisoALTV  48784  ringcbasbasALTV  48785  funcringcsetclem7ALTV  48792  funcringcsetclem9ALTV  48794  srhmsubcALTV  48798  cbvmpox2  48809  ply1sclrmsm  48857  dmatALTbasel  48875  lcoval  48885  lindslinindsimp1  48930  lindslinindsimp2  48936  lmod1  48965  elbigo  49024  elbigo2  49025  elbigolo1  49030  dig2nn0ld  49077  naryfvalel  49103  rrxlines  49206  rrxlinesc  49208  rrxlinec  49209  eenglngeehlnm  49212  elrrx2linest2  49218  rrxsphere  49221  itsclc0  49244  itsclc0b  49245  itsclinecirc0  49246  itsclinecirc0b  49247  itscnhlinecirc02p  49258  brab2dd  49300  f1omo  49365  f1omoOLD  49366  lubeldm2d  49430  glbeldm2d  49431  catprs  49483  sectpropdlem  49508  nelsubc3lem  49542  initc  49563  imaid  49626  upfval  49648  upfval2  49649  upfval3  49650  uppropd  49653  oppcinito  49707  oppctermo  49708  oppczeroo  49709  initopropd  49715  termopropd  49716  isthinc  49891  isthincd2lem1  49897  thincmoALT  49901  thincmod  49902  isthincd  49908  thincpropd  49914  indcthing  49932  discthing  49933  prsthinc  49936  termcterm  49985  termc2  49990  isinito4  50019  2arwcatlem1  50067  setc1onsubc  50074  cnelsubclem  50075  ranval3  50103  lmdfval2  50127  cmdfval2  50128  termolmd  50142  elsetrecslem  50171