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  3318  rexeqbidv  3319  reueqbidv  3390  rabeqbidva  3417  elabd2  3626  sbcbid  3797  csbeq2d  3857  csbeq2dv  3858  cbvcsbw  3861  cbvcsb  3862  cbvcsbv  3863  csbie  3886  csbied  3887  csbie2g  3891  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  sbcel12  4365  sbcel1g  4370  sbcel2  4372  prel12g  4822  eliuni  4954  iuneqconst  4960  iuneq12df  4975  iuneq12d  4978  cbviun  4992  cbviin  4993  cbviung  4994  cbviing  4995  cbviunv  4996  cbviinv  4997  iinxsng  5045  iinxprg  5046  iunxsng  5047  iunxsngf  5049  cbvdisj  5077  cbvdisjv  5078  disjor  5082  disjiund  5091  mpteq12da  5183  mpteq12f  5185  mpteq12dva  5186  axpweq  5298  rabxfrd  5364  rbropapd  5518  opeliunxp  5699  opeliun2xp  5700  opeliunxp2  5795  iunxpf  5805  elimampt  6010  elrelimasn  6053  elimasni  6058  imadifssran  6117  xpdifid  6134  ressn  6251  funfni  6606  fnbr  6608  dffv3  6838  elfv2ex  6885  fvelrnb  6902  foelcdmi  6903  fvun1  6933  fvco2  6939  funcnvmpt  6951  elfvmptrab1w  6977  elfvmptrab1  6978  elfvmptrab  6979  elpreima  7012  dff3  7054  fmptco  7084  fnelfp  7131  fnelnfp  7133  tpres  7157  fnprb  7164  fntpb  7165  funfvima3  7192  eluniima  7206  dff13  7210  f1ounsn  7228  f1eqcocnv  7257  isoini  7294  riotaeqdv  7326  mpoeq123dva  7442  cbvmpox  7461  elimampo  7505  ovelrn  7544  elovmpod  7612  elovmpo  7613  elovmporab  7614  elovmporab1w  7615  elovmporab1  7616  elovmpt3rab1  7628  fiun  7897  f1iun  7898  zfrep6  7909  fmpox  8021  el2mpocsbcl  8037  el2mpocl  8038  bropopvvv  8042  bropfvvvv  8044  xpord2indlem  8099  xpord3inddlem  8106  elsuppfng  8121  elsuppfn  8122  suppfnss  8141  opeliunxp2f  8162  mpoxopn0yelv  8165  mpoxopovel  8172  rntpos  8191  mpocurryd  8221  fpr2  8256  wfr2  8279  onoviun  8285  smoel  8302  smoiso  8304  smoel2  8305  smo11  8306  tfrlem9  8326  oalimcl  8497  oaass  8498  omordi  8503  omordlim  8514  omlimcl  8515  odi  8516  omeulem1  8519  omeulem2  8520  oen0  8524  oeordi  8525  oeordsuc  8532  oelimcl  8538  oeeulem  8539  oeeui  8540  nnmordi  8569  oaabs2  8587  omabs  8589  omsmolem  8595  ereldm  8699  iiner  8738  elmapg  8788  elpmg  8792  elixpsn  8887  ixpsnf1o  8888  boxriin  8890  omxpenlem  9018  pw2f1olem  9021  phplem2  9141  php3  9145  infn0  9214  elfi  9328  dffi3  9346  marypha2lem2  9351  ordiso2  9432  wemapsolem  9467  elharval  9478  inf3lemd  9548  inf3lem1  9549  inf3lem2  9550  inf3lem3  9551  cantnfs  9587  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1  9610  ttrclselem2  9647  trcl  9649  frr2  9684  r1sdom  9698  r1ordg  9702  r1pwss  9708  tz9.12lem3  9713  tz9.12  9714  r1elwf  9720  rankr1ai  9722  rankidb  9724  rankr1bg  9727  rankval2  9742  rankunb  9774  tcrank  9808  acni  9967  acni2  9968  acndom  9973  infpwfien  9984  alephnbtwn  9993  cardaleph  10011  cardinfima  10019  iunfictbso  10036  dfac3  10043  dfac5lem5  10049  dfac5  10051  dfac9  10059  dfac12r  10069  kmlem2  10074  kmlem12  10084  kmlem13  10085  kmlem14  10086  ackbij2lem3  10162  ackbij2  10164  cofsmo  10191  alephsing  10198  fin23lem30  10264  isf32lem9  10283  itunisuc  10341  axcc2lem  10358  axcc3  10360  domtriomlem  10364  axdc2lem  10370  axdc2  10371  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  ac6c4  10403  zorn2lem1  10418  ttukeylem6  10436  pwcfsdom  10506  axregndlem2  10526  axinfndlem1  10528  axacndlem4  10533  axacnd  10535  pwfseqlem1  10581  inar1  10698  inatsk  10701  gruurn  10721  grur1  10743  eltskm  10766  genpelv  10923  eluz1  12767  elixx1  13282  elixx3g  13286  elioo2  13314  elfz1  13440  elfz2  13442  elfzp1  13502  fzpr  13507  fzsuc2  13510  fzrev3  13518  elfzp12  13531  fzm1  13535  elfzo  13589  fz0add1fz1  13663  elfzo0l  13684  elfzom1b  13694  fzosplitsni  13707  elfzr  13709  elfzlmr  13710  zmodidfzo  13832  seqp1  13951  seqf1o  13978  bcval  14239  bcpasc  14256  hashf1lem1  14390  fundmge2nop0  14437  wrdmap  14481  elovmpowrd  14493  ccatfval  14508  elfzelfzccat  14515  ccatlid  14522  ccatass  14524  ccatrn  14525  ccatalpha  14529  swrdfv2  14597  ccatswrd  14604  swrdccat2  14605  pfxfv  14618  pfxeq  14631  ccatpfx  14636  swrdswrd  14640  swrdpfx  14642  pfxpfx  14643  cats1un  14656  swrdccatfn  14659  swrdccatin1  14660  pfxccatin12lem4  14661  pfxccatin12lem1  14663  swrdccatin2  14664  pfxccatin12lem2c  14665  pfxccatin12lem2  14666  swrdccat3blem  14674  swrdccatin1d  14678  swrdccatin2d  14679  pfxccatin12d  14680  revccat  14701  revrev  14702  repswpfx  14720  repswccat  14721  cshwidxmod  14738  2cshw  14748  cshwcshid  14762  cshwcsh2id  14763  cshimadifsn  14764  cshimadifsn0  14765  revco  14769  ccatco  14770  cshco  14771  swrdco  14772  ofccat  14904  shftfn  15008  shftval  15009  limsupgle  15412  ello12  15451  elo12  15462  isercolllem3  15602  sumeq1  15624  fsumsplit  15676  sumsplit  15703  fsum2dlem  15705  fsumcom2  15709  fsumparts  15741  explecnv  15800  pwdif  15803  fprodser  15884  fprodsplit  15901  fprod2dlem  15915  fprodcom2  15919  eftlub  16046  divalgmod  16345  bitsval  16363  bitsp1e  16371  bitsp1o  16372  sadfval  16391  sadcp1  16394  sadval  16395  sadcadd  16397  sadadd2  16399  saddisjlem  16403  sadadd  16406  sadass  16410  smufval  16416  smuval  16420  smuval2  16421  smupvallem  16422  smu01lem  16424  smueqlem  16429  smumul  16432  bezoutlem2  16479  bezoutlem4  16481  algfx  16519  eucalgcvga  16525  reumodprminv  16744  nnnn0modprm0  16746  unbenlem  16848  prmreclem5  16860  vdwapval  16913  vdwapun  16914  vdwnnlem1  16935  vdwnn  16938  ramval  16948  0ram  16960  ramub1lem2  16967  prmgaplem7  16997  prmlem0  17045  elrest  17359  prdsbasmpt  17402  prdsleval  17409  prdsbasmpt2  17414  pwselbasb  17420  imasaddfnlem  17461  imasvscafn  17470  divsfval  17480  ismre  17521  mreunirn  17532  mrisval  17565  ismri  17566  isacs  17586  catidd  17615  iscatd2  17616  ismon  17669  isepi  17676  sectffval  17686  sectfval  17687  dfiso2  17708  cicsym  17740  issubc  17771  catsubcat  17775  isfunc  17800  funcres  17832  funcpropd  17838  ffthiso  17867  isnat  17886  isnat2  17887  fuciso  17914  initoval  17929  termoval  17930  isinito  17932  istermo  17933  iszeroo  17934  isinitoi  17935  istermoi  17936  initoid  17937  termoid  17938  iszeroi  17945  2initoinv  17946  initoeu1  17947  initoeu2  17952  2termoinv  17953  termoeu1  17954  arwhoma  17981  elsetchom  18017  setcmon  18023  setcepi  18024  setciso  18027  catciso  18047  elestrchom  18063  estrcbasbas  18066  funcestrcsetclem7  18081  funcestrcsetclem8  18082  funcestrcsetclem9  18083  fthestrcsetc  18085  fullestrcsetc  18086  equivestrcsetc  18087  setc1strwun  18088  funcsetcestrclem7  18096  funcsetcestrclem8  18097  funcsetcestrclem9  18098  fthsetcestrc  18100  fullsetcestrc  18101  hofcl  18194  hofpropd  18202  yonedalem4c  18212  yonedainv  18216  yonffthlem  18217  lubeldm  18286  glbeldm  18299  joindef  18309  meetdef  18323  poslubdg  18347  acsficl2d  18487  acsmapd  18489  psref  18509  psss  18515  dirge  18538  chnccats1  18560  chnccat  18561  chnrev  18562  mgmpropd  18588  issstrmgm  18590  grpidval  18598  grpidpropd  18599  grpidd  18608  ismgmhm  18633  issubmgm  18639  issgrpd  18667  sgrppropd  18668  ismndd  18693  mndpropd  18696  imasmnd2  18711  imasmnd  18712  xpsmnd0  18715  ismhm  18722  issubm  18740  gsumsgrpccat  18777  elefmndbas2  18811  smndex1mndlem  18846  imasgrp2  18997  imasgrp  18998  issubg  19068  subginv  19075  isnsg  19096  eqg0el  19124  quselbas  19125  isghm  19156  isghmOLD  19157  resghm2b  19175  conjnmzb  19194  conjnsg  19195  ghmpropd  19197  isga  19232  elcntz  19263  elcntzsn  19266  cntzrcl  19268  resscntz  19274  symgextf1  19362  gsmsymgreqlem2  19372  f1otrspeq  19388  pmtrfrn  19399  pmtrdifellem3  19419  pmtrdifellem4  19420  psgnunilem1  19434  psgnunilem5  19435  psgnunilem2  19436  psgnunilem3  19437  psgneldm2  19445  psgnfitr  19458  psgnsn  19461  gexdvds  19525  gex1  19532  isslw  19549  sylow3lem2  19569  lsmelvalx  19581  pj1ghm  19644  efgtlen  19667  efgsfo  19680  efgredlemc  19686  frgp0  19701  frgpmhm  19706  qusabl  19806  frgpnabllem1  19814  imasabl  19817  cycsubmcmn  19830  0cyg  19834  cycsubgcyg  19842  gsumval3  19848  gsumcllem  19849  gsumzaddlem  19862  gsumzsplit  19868  gsummptfzcl  19910  eldprd  19947  dprdcntz2  19981  dprd2d2  19987  dmdprdsplit2lem  19988  dmdprdsplit2  19989  dprdsplit  19991  ablfac2  20032  isrngd  20120  rngpropd  20121  imasrng  20124  qusrng  20127  ringurd  20132  isringd  20238  imasring  20278  xpsring1d  20281  dvdsrval  20309  isunit  20321  dvdsrpropd  20364  isirred  20367  isrnghm  20389  isrngim  20393  c0ghm  20409  c0snghm  20412  isrhm  20426  isrim0  20430  islring  20485  issubrng  20492  opprsubrng  20504  issubrg  20516  opprsubrg  20538  resrhm2b  20547  rhmpropd  20554  rnghmresel  20565  elrngchom  20569  rnghmsubcsetclem1  20576  rnghmsubcsetclem2  20577  rngcid  20580  rngcsect  20581  rngciso  20583  funcrngcsetcALT  20586  zrinitorngc  20587  zrtermorngc  20588  rhmresel  20594  elringchom  20598  rhmsubcsetclem1  20605  rhmsubcsetclem2  20606  ringcid  20609  rhmsscrnghm  20610  rhmsubcrngclem1  20611  rhmsubcrngclem2  20612  ringcsect  20615  ringciso  20617  ringcbasbas  20618  zrtermoringc  20620  srhmsubc  20625  rhmsubclem3  20632  rhmsubclem4  20633  drngunit  20679  isdrngd  20710  isdrngdOLD  20712  issdrg  20733  sdrgunit  20741  isabv  20756  issrngd  20800  islmod  20827  lmodprop2d  20887  islss  20897  islssd  20898  lssats2  20963  ellspsn  20966  islmhm  20991  lmhmf1o  21010  lmhmima  21011  lmhmpreima  21012  reslmhm  21016  pwssplit3  21025  lmhmpropd  21037  islbs  21040  lspprel  21058  lspfixed  21095  lbsacsbs  21123  lbsextlem1  21125  lbsextlem2  21126  lbsextlem3  21127  lbsextlem4  21128  ixpsnbasval  21172  isridlrng  21186  rnglidlmmgm  21212  isridl  21219  quscrng  21250  rngqiprngimfolem  21257  rngqiprngimf1lem  21261  rngqiprngimfo  21268  islpidl  21292  lidldvgen  21301  irinitoringc  21446  pzriprnglem13  21460  pzriprnglem14  21461  zrhrhmb  21477  znf1o  21518  frgpcyg  21540  psgnevpmb  21554  isphld  21621  phlssphl  21626  elocv  21635  iscss  21650  isobs  21687  obs2ss  21696  dsmmfi  21705  dsmmelbas  21706  dsmmlss  21711  frlmelbas  21723  frlmlbs  21764  frlmup1  21765  ellspd  21769  islinds  21776  islindf2  21781  f1lindf  21789  islindf4  21805  assamulgscmlem2  21868  psrgrp  21924  mplsubglem  21966  mpllsslem  21967  mplmonmul  22003  subrgascl  22033  subrgasclcl  22034  mpfind  22082  ismhp  22095  gsumply1subr  22186  lply1binomsc  22267  matbas2d  22379  matecl  22381  matvscl  22387  mat1  22403  mat0dim0  22423  mat0dimid  22424  mat0dimscm  22425  mat1dimelbas  22427  dmatel  22449  scmatel  22461  scmateALT  22468  scmataddcl  22472  scmatsubcl  22473  smatvscl  22480  scmatghm  22489  mat1scmat  22495  mdetunilem7  22574  mdetunilem9  22576  smadiadetr  22631  cramerimplem2  22640  cramer0  22646  pmatcoe1fsupp  22657  cpmatpmat  22666  cpmatel  22667  cpmatacl  22672  cpmatinvcl  22673  mat2pmatghm  22686  mat2pmatmul  22687  decpmatmullem  22727  pmatcollpwlem  22736  pmatcollpw3fi1lem1  22742  pmatcollpwscmatlem1  22745  monmat2matmon  22780  chfacfscmul0  22814  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  cayhamlem1  22822  cpmadugsumlemB  22830  cpmadugsumlemC  22831  cpmadugsumlemF  22832  cayhamlem2  22840  istopon  22868  eltg  22913  eltg2  22914  eltop  22930  eltop2  22931  eltop3  22932  pptbas  22964  iscld  22983  neiss2  23057  isnei  23059  neiptopnei  23088  neiptopreu  23089  lpfval  23094  lpval  23095  islp  23096  maxlp  23103  islpi  23105  neitr  23136  restlp  23139  ordtbas2  23147  ordtrest2  23160  lmfval  23188  cnfval  23189  iscn  23191  iscnp  23193  tgcn  23208  tgcnp  23209  lmbrf  23216  cnpresti  23244  ist1  23277  ist1-2  23303  cnt1  23306  haust1  23308  cmpfi  23364  cmpfii  23365  1stcfb  23401  2ndc1stc  23407  1stcrest  23409  2ndcdisj  23412  1stcelcls  23417  nllyi  23431  subislly  23437  islocfin  23473  lfinpfin  23480  locfindis  23486  locfincf  23487  comppfsc  23488  kgenval  23491  elkgen  23492  kgencn2  23513  txbas  23523  eltx  23524  ptval  23526  ptpjpre1  23527  ptopn2  23540  ptpjopn  23568  ptclsg  23571  xkoccn  23575  txdis  23588  txdis1cn  23591  ptrescn  23595  hausdiag  23601  hauseqlcld  23602  txhaus  23603  xkohaus  23609  elqtop  23653  qtopeu  23672  kqcldsat  23689  hmeofval  23714  ptuncnv  23763  ptunhmeo  23764  elmptrab  23783  fbdmn0  23790  elfg  23827  elfilss  23832  filunirn  23838  fixufil  23878  elfm  23903  rnelfmlem  23908  rnelfm  23909  fmfnfmlem4  23913  elflim2  23920  flimtopon  23926  elflim  23927  hausflim  23937  flimcls  23941  flfnei  23947  isflf  23949  hausflf  23953  cnpflf  23957  cnflf  23958  txflf  23962  isfcls  23965  fclstopon  23968  isfcls2  23969  fclssscls  23974  fclsnei  23975  fclsfnflim  23983  flimfnfcls  23984  isfcf  23990  fcfelbas  23992  cnpfcf  23997  cnfcf  23998  flfcntr  23999  alexsublem  24000  alexsubALTlem3  24005  cnextfun  24020  cnextfvval  24021  cnextf  24022  cnextcn  24023  tmdgsum2  24052  tgpconncomp  24069  ghmcnp  24071  qustgplem  24077  eltsms  24089  haustsms  24092  tsmsgsum  24095  tsmssubm  24099  tsmssplit  24108  isust  24160  ustbas  24183  elutop  24189  ustuqtoplem  24195  ustuqtop4  24200  ustuqtop  24202  utopsnneiplem  24203  utopsnneip  24204  utopsnnei  24205  isusp  24217  isucn  24233  ucncn  24240  iscfilu  24243  neipcfilu  24251  iscusp  24254  cnextucn  24258  ispsmet  24260  ismet  24279  isxmet  24280  elblps  24343  elbl  24344  elmopn  24398  prdsbl  24447  neibl  24457  met1stc  24477  metrest  24480  prdsxmslem2  24485  txmetcnp  24503  txmetcn  24504  metustsym  24511  cfilucfil2  24517  elbl4  24519  metuel  24520  psmetutop  24523  restmetu  24526  metucn  24527  tngngp  24610  isnmhm  24702  zcld  24770  metnrmlem1a  24815  elcncf  24850  cncfcnvcn  24887  cnheibor  24922  lebnumlem1  24928  ishtpy  24939  isphtpy  24948  om1elbas  25000  elpi1  25013  pi1xfr  25023  pi1coghm  25029  tcphcph  25205  lmmbrf  25230  iscfil  25233  iscau  25244  iscauf  25248  caucfil  25251  iscmet  25252  cmetcaulem  25256  iscmet3lem1  25259  iscmet3lem2  25260  iscmet3  25261  bcthlem1  25292  cmsss  25319  cmetcusp1  25321  cmetcusp  25322  cmscsscms  25341  rrxcph  25360  minveclem3b  25396  ovolfioo  25436  ovolficc  25437  ovolctb  25459  ovoliunnul  25476  ovolshftlem1  25478  sca2rab  25481  ovolscalem1  25482  ovolicc2lem1  25486  ovolicc2lem2  25487  ovolicc2lem4  25489  ovolicc2lem5  25490  iundisj  25517  iunmbl2  25526  uniioombllem3  25554  vitalilem2  25578  vitalilem3  25579  mbfss  25615  i1faddlem  25662  i1fmullem  25663  mbfi1fseqlem2  25685  mbfi1fseqlem4  25687  mbfi1fseq  25690  itg2splitlem  25717  itg2split  25718  itg2monolem1  25719  itg2gt0  25729  isibl  25734  iblss2  25775  itgss3  25784  itgsplit  25805  ellimc  25842  limcmo  25851  cnlimc  25857  limciun  25863  limcun  25864  eldv  25867  dvbsss  25871  dvreslem  25878  elcpn  25904  dvaddf  25913  dvmulf  25914  dvcof  25920  rolle  25962  dvlip2  25968  dvivthlem1  25981  lhop1  25987  lhop2  25988  ftc1cn  26018  fta1glem2  26142  plyco0  26165  elply  26168  ply1termlem  26176  eltayl  26335  tayl0  26337  taylplem1  26338  taylplem2  26339  dvtaylp  26346  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  abelth  26419  cxpcn3  26726  rlimcnp  26943  fsumharmonic  26990  dchrelbas  27215  pntrsumbnd2  27546  ostth2lem2  27613  nolesgn2ores  27652  nogesgn1ores  27654  nosupprefixmo  27680  noinfprefixmo  27681  nosupcbv  27682  nosupdm  27684  nosupfv  27686  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1lem3  27690  nosupbnd1lem5  27692  nosupbnd2lem1  27695  noinfcbv  27697  noinfdm  27699  noinffv  27701  noinfres  27702  noinfbnd1lem1  27703  noinfbnd1lem3  27705  noinfbnd1lem5  27707  noinfbnd2lem1  27710  elmade  27865  elold  27867  sltsleft  27868  sltsright  27869  oldlim  27895  madebday  27908  newbday  27910  ltslpss  27916  bdayiun  27923  cofcutr  27932  cofcutrtime  27935  lrrecval  27947  lrrecval2  27948  addsval  27970  precsexlem9  28223  precsexlem11  28225  ltonold  28269  onnolt  28274  onlts  28275  noseqrdgfn  28314  istrkgb  28539  istrkgcb  28540  istrkge  28541  istrkgl  28542  istrkgld  28543  axtgsegcon  28548  axtg5seg  28549  axtgbtwnid  28550  axtgpasch  28551  axtgupdim2  28555  axtgeucl  28556  tgdim01  28591  iscgrg  28596  isismt  28618  tglnunirn  28632  tglngval  28635  tgellng  28637  legval  28668  legov  28669  legov2  28670  ishlg  28686  mirreu3  28738  mirval  28739  mirfv  28740  mircgr  28741  mirbtwn  28742  ismir  28743  mireq  28749  symquadlem  28773  israg  28781  perpln1  28794  perpln2  28795  isperp  28796  islnopp  28823  outpasch  28839  ishpg  28843  iscgra  28893  dfcgra2  28914  isinag  28922  isleag  28931  iseqlg  28951  f1otrgitv  28954  f1otrg  28955  f1otrge  28956  ttgval  28959  ttgelitv  28967  elee  28978  brbtwn  28984  brcgr  28985  axlowdimlem16  29042  ebtwntg  29067  elntg2  29070  upgrex  29177  edgupgr  29219  upgredg  29222  edglnl  29228  numedglnl  29229  uhgr2edg  29293  umgr2edg1  29296  usgredg2vlem1  29310  usgredg2vlem2  29311  ushgredgedg  29314  ushgredgedgloop  29316  uhgrspansubgrlem  29375  fusgrfisstep  29414  nbgrval  29421  nbgrel  29425  nbupgrel  29430  nbgr2vtx1edg  29435  nbuhgr2vtx1edgblem  29436  nbuhgr2vtx1edgb  29437  nbusgreledg  29438  usgrnbcnvfv  29450  uvtxval  29472  uvtxel  29473  uvtx01vtx  29482  uvtxusgrel  29488  nbcplgr  29519  cplgr3v  29520  cusgrexi  29528  structtocusgr  29531  vtxdgfval  29553  vtxdg0v  29559  vtxdeqd  29563  vtxdun  29567  1loopgrnb0  29588  1loopgrvd0  29590  1hevtxdg0  29591  1hevtxdg1  29592  1egrvtxdg1  29595  umgr2v2evtxel  29608  umgr2v2enb1  29612  umgr2v2evd2  29613  vtxdginducedm1lem4  29628  vtxdginducedm1  29629  finsumvtxdg2sstep  29635  ewlksfval  29687  isewlk  29688  wksfval  29695  iswlk  29696  uspgr2wlkeq  29731  wlkres  29754  dfpth2  29814  usgr2pthlem  29848  clwlkcompim  29865  uspgrn2crct  29893  wwlks  29920  iswwlksn  29923  wwlknvtx  29930  wlkiswwlks2  29960  wwlksm1edg  29966  wwlksnred  29977  wwlksnext  29978  wwlksnredwwlkn  29980  wwlksnredwwlkn0  29981  wwlksnwwlksnon  30000  wspn0  30009  usgr2wspthons3  30052  rusgrnumwwlkb0  30059  clwwlk  30070  clwwlkccatlem  30076  clwlkclwwlklem2a4  30084  clwlkclwwlk  30089  clwwisshclwwslem  30101  clwwlkinwwlk  30127  clwwlkel  30133  clwwlkf  30134  clwwlkext2edg  30143  wwlksext2clwwlk  30144  wwlksubclwwlk  30145  clwwnisshclwwsn  30146  eleclclwwlknlem2  30148  erclwwlknsym  30157  erclwwlkntr  30158  umgrhashecclwwlk  30165  clwwlkvbij  30200  eupth2lem3lem3  30317  eupth2lem3lem4  30318  eupth2lem3lem6  30320  eupth2lemb  30324  eucrct2eupth  30332  fusgreg2wsplem  30420  2clwwlklem  30430  2clwwlk2clwwlklem  30433  2clwwlkel  30436  2clwwlk2clwwlk  30437  extwwlkfabel  30440  clwwlknonclwlknonf1o  30449  dlwwlknondlwlknonf1olem1  30451  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  ex-res  30528  isssp  30812  sspn  30824  islno  30841  isblo  30870  nmlno0  30883  ishmo  30899  dipdir  30930  dipass  30933  ubthlem1  30958  ubthlem2  30959  htthlem  31005  htth  31006  ocel  31369  ocnel  31386  shsel  31402  shsel2  31410  shmodsi  31477  pjhtheu  31482  pjeq  31487  axpjpj  31508  pjoc2  31527  elspani  31631  h1de2ctlem  31643  elspansn  31654  elspansn2  31655  elnlfn  32016  eleigvec  32045  riesz3i  32150  cbviunf  32642  iuneq12daf  32643  iunrdx  32650  iunrnmptss  32652  cbvdisjf  32658  disjorf  32666  disjabrex  32669  disjabrexf  32670  iundisjf  32676  disjrdx  32678  brab2d  32695  fresunsn  32715  2ndresdju  32739  abfmpunirn  32742  abfmpeld  32744  abfmpel  32745  fmptcof2  32747  acunirnmpt2  32750  acunirnmpt2f  32751  aciunf1lem  32752  suppss3  32813  fpwrelmap  32823  xrofsup  32858  iundisjfi  32887  eliccioo  33023  s3f1  33040  ccatf1  33042  ccatws1f1o  33044  swrdrn3  33048  ismnt  33076  mgcoval  33079  gsummpt2co  33142  gsumpart  33157  gsumhashmul  33161  gsummulsubdishift1  33162  xrge0tsmsbi  33168  gsumwrd2dccatlem  33171  gsumwrd2dccat  33172  cycpmco2  33227  cyc3co2  33234  isfxp  33262  cntrval2  33265  inftmrel  33274  isinftm  33275  isslmd  33296  urpropd  33325  elrgspn  33340  erlval  33352  rlocval  33353  rloccring  33364  rloc1r  33366  domnprodeq0  33370  domnpropd  33371  isdrng4  33389  fracfld  33402  resv1r  33432  ellspds  33461  ellpi  33466  lbslsp  33470  rhmimaidl  33525  isprmidl  33531  qsidomlem1  33545  qsidomlem2  33546  ismxidl  33555  crngmxidl  33562  drng0mxidl  33569  opprqus0g  33583  qsfld  33591  isrprm  33610  rsprprmprmidlb  33616  ressply1evls1  33658  ply1mulrtss  33675  ply1coedeg  33682  psrmonmul  33727  dimpropd  33786  lbslsat  33794  extdg1id  33844  fldextrspunlsplem  33851  fldextrspunlsp  33852  elirng  33864  ply1annidllem  33879  constrsuc  33916  constrconj  33923  constrllcllem  33930  constrlccllem  33931  constrcccllem  33932  nn0constr  33939  smatrcl  33974  smatcl  33980  ist0cld  34011  txomap  34012  locfinreflem  34018  zarclsiin  34049  zart0  34057  rhmpreimacnlem  34062  metidval  34068  cnre2csqima  34089  ordtrest2NEW  34101  fmcncfil  34109  fsumcvg4  34128  ofcfval  34276  measvuni  34392  meascnbl  34397  faeval  34424  ismbfm  34429  elunirnmbfm  34430  imambfm  34440  elcarsg  34483  itgeq12dv  34504  issibf  34511  eulerpartlems  34538  eulerpartlemgc  34540  eulerpartlemgvv  34554  eulerpartlemgu  34555  eulerpart  34560  rrvmbfm  34620  elorvc  34638  elorrvc  34642  dstfrvunirn  34653  ballotlemfc0  34671  ballotlemfcc  34672  ballotlemsima  34694  ballotlemrv  34698  fzssfzo  34717  signstfvn  34747  signstfvneq0  34750  signstres  34753  repr0  34789  reprinrn  34796  reprdifc  34805  hgt750lemg  34832  hgt750lemb  34834  istrkg2d  34844  axtgupdim2ALTV  34846  afsval  34849  brafs  34850  bnj945  34950  bnj1400  35011  bnj18eq1  35103  bnj916  35109  bnj1014  35137  bnj1015  35138  bnj1110  35158  bnj1417  35217  rankval2b  35276  r1filimi  35280  r1ssel  35284  onvf1odlem3  35321  vonf1owev  35324  revpfxsfxrev  35332  cplgredgex  35337  pfxwlk  35340  revwlk  35341  subfacp1lem2b  35397  subfacp1lem4  35399  subfacp1lem5  35400  subfacp1lem6  35401  ptpconn  35449  cvmscbv  35474  iscvm  35475  cvmsi  35481  cvmsval  35482  cvmliftmolem1  35497  cvmlift2lem12  35530  cvmlift2lem13  35531  cvmlift3lem7  35541  snmlval  35547  satfv1  35579  satfvsucsuc  35581  satfrnmapom  35586  satf0op  35593  satf0n0  35594  sat1el2xp  35595  fmlafvel  35601  isfmlasuc  35604  fmlaomn0  35606  gonan0  35608  goaln0  35609  gonar  35611  goalr  35613  satffunlem1lem2  35619  satffunlem2lem2  35622  satfv0fvfmla0  35629  satef  35632  satefvfmla0  35634  sategoelfvb  35635  satfv1fvfmla1  35639  mrsubfval  35724  mrsubvrs  35738  mclsrcl  35777  mclsval  35779  mppsval  35788  mclsppslem  35799  opelco3  35991  wsuclem  36039  funtransport  36247  fvtransport  36248  brcolinear  36275  colineardim1  36277  funray  36356  fvray  36357  funline  36358  fvline  36360  lineelsb2  36364  fwddifval  36378  fwddifnval  36379  rankelg  36384  rankeq1o  36387  elhf2  36391  0hf  36393  rmoeqbidv  36429  disjeq12dv  36431  ixpeq12dv  36432  prodeq12sdv  36434  itgeq12sdv  36435  cbvralvw2  36442  cbvrexvw2  36443  cbvrmovw2  36444  cbvreuvw2  36445  cbvcsbvw2  36447  cbviunvw2  36448  cbviinvw2  36449  cbvmptvw2  36450  cbvdisjvw2  36451  cbvmpo1vw2  36459  cbvmpo2vw2  36460  cbvsbcdavw  36473  cbvcsbdavw  36475  cbvcsbdavw2  36476  cbviundavw  36478  cbviindavw  36479  cbvdisjdavw  36484  cbvrabdavw2  36501  cbviundavw2  36502  cbviindavw2  36503  cbvmptdavw2  36504  cbvdisjdavw2  36505  cbvriotadavw2  36506  cbvmpo1davw2  36508  cbvmpo2davw2  36509  cbvsumdavw2  36511  neibastop2lem  36576  neibastop3  36578  eltail  36590  bj-projeq  37240  bj-projval  37244  bj-restsn  37335  opelopabbv  37398  brabd0  37402  bj-eldiag  37431  bj-eldiag2  37432  mptsnunlem  37593  dissneqlem  37595  iooelexlt  37617  relowlssretop  37618  rdgellim  37631  exrecfnlem  37634  finxpeq1  37641  finxpreclem6  37651  pibp21  37670  curf  37849  uncf  37850  curunc  37853  unccur  37854  fin2so  37858  lindsadd  37864  lindsdom  37865  lindsenlbs  37866  matunitlindflem1  37867  matunitlindflem2  37868  matunitlindf  37869  ptrest  37870  ptrecube  37871  poimirlem2  37873  poimirlem8  37879  poimirlem17  37888  poimirlem18  37889  poimirlem20  37891  poimirlem21  37892  poimirlem22  37893  poimirlem24  37895  poimirlem26  37897  poimirlem29  37900  heicant  37906  mblfinlem1  37908  mblfinlem2  37909  volsupnfl  37916  itg2addnclem  37922  itg2gt0cn  37926  indexdom  37985  incsequz  37999  istotbnd  38020  istotbnd3  38022  0totbnd  38024  sstotbnd  38026  sstotbnd3  38027  isbnd  38031  prdstotbnd  38045  cntotbnd  38047  isismty  38052  heibor1lem  38060  heiborlem2  38063  heiborlem3  38064  heibor  38072  isass  38097  exidcl  38127  exidreslem  38128  elghomlem2OLD  38137  rngoidmlem  38187  rngo1cl  38190  divrngcl  38208  isdrngo2  38209  isrngohom  38216  isrngoiso  38229  isriscg  38235  iscom2  38246  iscringd  38249  isidl  38265  ispridl  38285  ismaxidl  38291  ac6s6  38423  dmecd  38561  dfpre4  38731  releldmqs  38994  releldmqscoss  38996  erimeq2  39014  qmapeldisjsim  39111  eldisjlem19  39164  membpartlem19  39165  prter3  39258  islshp  39355  islsat  39367  lcvfbr  39396  islfl  39436  ellkr  39465  islshpkrN  39496  ldual1dim  39542  isopos  39556  cmtfvalN  39586  cvrfval  39644  isat  39662  islln  39882  islpln  39906  islvol  39949  isline  40115  ispointN  40118  ispsubsp  40121  elpmap  40134  elpmapat  40140  elpadd  40175  paddclN  40218  elpclN  40268  elpcliN  40269  pclfinN  40276  pclcmpatN  40277  ispsubclN  40313  iswatN  40370  islhp  40372  islaut  40459  ispautN  40475  isldil  40486  isltrn  40495  isdilN  40530  istrnN  40533  istendo  41136  dvhb1dimN  41362  erng1lem  41363  erngdvlem4-rN  41375  diaelval  41409  diaeldm  41412  dia1dimid  41439  cdlemm10N  41494  dibopelvalN  41519  dibopelval2  41521  dibelval3  41523  dibelval1st  41525  dibelval2nd  41528  dibeldmN  41534  dibvalrel  41539  dibglbN  41542  dicffval  41550  dicfval  41551  dicopelval  41553  dicelvalN  41554  dicelval3  41556  dicvalrelN  41561  dicelval1sta  41563  diclspsn  41570  dihopelvalbN  41614  dihopelvalcqat  41622  dihopelvalcpre  41624  dihvalrel  41655  dih1  41662  dihmeetlem4preN  41682  dihmeetlem13N  41695  dih1dimatlem  41705  dochnel2  41768  dihjatcclem4  41797  dvh2dim  41821  dvh3dim  41822  dvh4dimN  41823  dochfln0  41853  lpolsetN  41858  islpolN  41859  lcfrvalsnN  41917  lcfrlem21  41939  lcfrlem27  41945  lcfrlem37  41955  lcfr  41961  lcdlss  41995  mapdcv  42036  hdmap1fval  42172  hdmapffval  42202  hdmapfval  42203  hdmapval  42204  hgmapffval  42261  hgmapfval  42262  hdmapellkr  42290  hlhilhillem  42336  fzsplitnd  42352  isprimroot  42463  primrootsunit1  42467  primrootscoprmpow  42469  primrootscoprbij  42472  aks6d1c1p2  42479  aks6d1c1p3  42480  aks6d1c1p4  42481  aks6d1c1p5  42482  aks6d1c1p6  42484  aks6d1c1  42486  evl1gprodd  42487  sticksstones11  42526  sticksstones12a  42527  rhmqusspan  42555  grpods  42564  fzosumm1  42620  frlmfielbas  42870  frlmsnic  42910  psrmnd  42913  isnacs  43061  mrefg2  43064  elmzpcl  43083  mzpcompact2  43109  eldiophb  43114  elpell1qr  43204  elpell14qr  43206  elpell1234qr  43208  pw2f1ocnv  43394  pw2f1o2val2  43397  aomclem4  43414  aomclem6  43416  islssfg2  43428  imasgim  43457  lnr2i  43473  elmnc  43493  rngunsnply  43526  onexomgt  43598  onexlimgt  43600  onexoegt  43601  oaordnr  43653  omnord1  43662  oenord1  43673  cantnfresb  43681  tfsconcatun  43694  tfsconcat0i  43702  ofoaf  43712  naddcnff  43719  naddcnffo  43721  naddcnfcom  43723  naddcnfid1  43724  naddcnfid2  43725  naddcnfass  43726  naddwordnexlem4  43758  fiinfi  43929  sqrtcvallem1  43987  elintima  44009  eliunov2  44035  ov2ssiunov2  44056  brtrclfv2  44083  rfovcnvf1od  44360  rfovcnvfvd  44363  fsovrfovd  44365  fsovfvd  44366  fsovcnvlem  44369  ntrclsfv1  44411  ntrclselnel1  44413  ntrclsneine0lem  44420  ntrneifv1  44435  ntrneifv2  44436  ntrneiel  44437  gneispace2  44488  gneispacess2  44502  extoimad  44520  mnringelbased  44573  dvconstbi  44690  bccbc  44701  wfac8prim  45358  permaxrep  45362  permac8prim  45370  eliin2f  45463  iineq12dv  45465  rabbida2  45491  disjinfi  45551  unirnmap  45566  elmptima  45616  iuneqfzuzlem  45693  iooiinioc  45916  fsumiunss  45935  fsumsupp0  45938  lptre2pt  45998  icccncfext  46245  cncfiooicclem1  46251  dvnprodlem2  46305  stoweidlem27  46385  stoweidlem29  46387  stoweidlem31  46389  stoweidlem34  46392  stoweidlem48  46406  stoweidlem59  46417  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem2  46467  fourierdlem3  46468  fourierdlem25  46490  fourierdlem32  46497  fourierdlem33  46498  fourierdlem41  46506  fourierdlem48  46512  fourierdlem49  46513  fourierdlem62  46526  fourierdlem70  46534  fourierdlem80  46544  fourierdlem92  46556  fourierdlem93  46557  fourierdlem101  46565  etransclem37  46629  sge0val  46724  sge0f1o  46740  sge0iunmptlemre  46773  sge0iunmpt  46776  iundjiun  46818  caragenel  46853  ovncvrrp  46922  ovnsubaddlem1  46928  ovnsubadd  46930  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvlelem4  46956  hoidmvle  46958  ovncvr2  46969  hspdifhsp  46974  hoiqssbl  46983  hspmbllem2  46985  hspmbl  46987  opnvonmbllem1  46990  isvonmbl  46996  ovnovollem1  47014  issmflem  47085  smflimlem3  47131  smflimlem4  47132  smflim  47135  smfmullem2  47150  smflimmpt  47168  smfsuplem1  47169  smflimsuplem1  47178  smflimsuplem3  47180  smflimsuplem4  47181  smflimsuplem7  47184  smflimsup  47186  chnsubseq  47238  fcores  47427  fcoresf1  47429  afvelrnb  47523  afvelrnb0  47524  afv2co2  47617  el1fzopredsuc  47685  iccpart  47776  iccpartgtprec  47780  iccpartiltu  47782  iccpartigtl  47783  iccpartltu  47785  iccpartgtl  47786  iccpartgt  47787  iccpartleu  47788  iccpartgel  47789  iccelpart  47793  iccpartiun  47794  icceuelpart  47796  fargshiftfv  47799  fargshiftfo  47802  sprel  47844  prprelb  47876  prprelprb  47877  fpprel  48088  sbgoldbo  48147  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  bgoldbtbndlem3  48167  bgoldbtbnd  48169  clnbgrval  48182  elclnbgrelnbgr  48185  clnbgrel  48188  clnbupgrel  48194  vopnbgrel  48214  isubgredg  48226  upgrimwlklem3  48259  upgrimwlklem5  48261  upgrimpths  48269  grtriprop  48301  isgrtri  48303  grtriclwlk3  48305  stgredgel  48317  gpgvtxel  48407  gpgiedgdmel  48409  gpgedgel  48410  opgpgvtx  48415  gpg5nbgrvtx13starlem1  48431  gpg5nbgrvtx13starlem2  48432  gpg5nbgrvtx13starlem3  48433  gpg3kgrtriex  48449  grlimedgnedg  48491  upwlksfval  48495  isupwlk  48496  intop  48563  isclintop  48567  assintop  48569  isassintop  48570  assintopcllaw  48572  uzlidlring  48595  elrngchomALTV  48629  rngccatidALTV  48632  rngcsectALTV  48635  rngcisoALTV  48637  rhmsubcALTVlem3  48643  rhmsubcALTVlem4  48644  funcringcsetcALTV2lem7  48656  funcringcsetcALTV2lem9  48658  elringchomALTV  48663  ringccatidALTV  48666  ringcsectALTV  48669  ringcisoALTV  48671  ringcbasbasALTV  48672  funcringcsetclem7ALTV  48679  funcringcsetclem9ALTV  48681  srhmsubcALTV  48685  cbvmpox2  48696  ply1sclrmsm  48744  dmatALTbasel  48762  lcoval  48772  lindslinindsimp1  48817  lindslinindsimp2  48823  lmod1  48852  elbigo  48911  elbigo2  48912  elbigolo1  48917  dig2nn0ld  48964  naryfvalel  48990  rrxlines  49093  rrxlinesc  49095  rrxlinec  49096  eenglngeehlnm  49099  elrrx2linest2  49105  rrxsphere  49108  itsclc0  49131  itsclc0b  49132  itsclinecirc0  49133  itsclinecirc0b  49134  itscnhlinecirc02p  49145  brab2dd  49187  f1omo  49252  f1omoOLD  49253  lubeldm2d  49317  glbeldm2d  49318  catprs  49370  sectpropdlem  49395  nelsubc3lem  49429  initc  49450  imaid  49513  upfval  49535  upfval2  49536  upfval3  49537  uppropd  49540  oppcinito  49594  oppctermo  49595  oppczeroo  49596  initopropd  49602  termopropd  49603  isthinc  49778  isthincd2lem1  49784  thincmoALT  49788  thincmod  49789  isthincd  49795  thincpropd  49801  indcthing  49819  discthing  49820  prsthinc  49823  termcterm  49872  termc2  49877  isinito4  49906  2arwcatlem1  49954  setc1onsubc  49961  cnelsubclem  49962  ranval3  49990  lmdfval2  50014  cmdfval2  50015  termolmd  50029  elsetrecslem  50058