Theorem eleq2d 2827

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 634	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1833	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 17	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		dfclel 2817	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		dfclel 2817	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eleq2  2830  eleq12d  2835  eleqtrd  2843  neleqtrd  2863  eqabrd  2884  raleqbidv  3346  rexeqbidv  3347  reueqbidv  3423  rabeqbidva  3453  elabd2  3670  sbcbid  3844  csbeq2d  3905  csbeq2dv  3906  cbvcsbw  3909  cbvcsb  3910  cbvcsbv  3911  csbie  3934  csbied  3935  csbie2g  3939  cbvralcsf  3941  cbvreucsf  3943  cbvrabcsf  3944  sbcel12  4411  sbcel1g  4416  sbcel2  4418  prel12g  4864  eliuni  4997  iuneqconst  5003  iuneq12df  5018  iuneq12d  5021  cbviun  5036  cbviin  5037  cbviung  5038  cbviing  5039  cbviunv  5040  cbviinv  5041  iinxsng  5088  iinxprg  5089  iunxsng  5090  iunxsngf  5092  cbvdisj  5120  cbvdisjv  5121  disjor  5125  disjiund  5134  mpteq12da  5227  mpteq12dfOLD  5229  mpteq12f  5230  mpteq12dva  5231  axpweq  5351  rabxfrd  5417  rbropapd  5569  opeliunxp  5752  opeliun2xp  5753  opeliunxp2  5849  iunxpf  5859  elimampt  6061  elrelimasn  6104  elimasni  6109  imadifssran  6171  xpdifid  6188  ressn  6305  funfni  6674  fnbr  6676  dffv3  6902  elfv2ex  6952  fvelrnb  6969  foelcdmi  6970  fvun1  7000  fvco2  7006  elfvmptrab1w  7043  elfvmptrab1  7044  elfvmptrab  7045  elpreima  7078  dff3  7120  fmptco  7149  fnelfp  7195  fnelnfp  7197  tpres  7221  fnprb  7228  fntpb  7229  funfvima3  7256  eluniima  7270  elunirn2OLD  7273  dff13  7275  f1ounsn  7292  f1eqcocnv  7321  isoini  7358  riotaeqdv  7389  mpoeq123dva  7507  cbvmpox  7526  elimampo  7570  ovelrn  7609  elovmpod  7677  elovmpo  7678  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  elovmpt3rab1  7693  fiun  7967  f1iun  7968  zfrep6  7979  fmpox  8092  el2mpocsbcl  8110  el2mpocl  8111  bropopvvv  8115  bropfvvvv  8117  xpord2indlem  8172  xpord3inddlem  8179  elsuppfng  8194  elsuppfn  8195  suppfnss  8214  opeliunxp2f  8235  mpoxopn0yelv  8238  mpoxopovel  8245  rntpos  8264  mpocurryd  8294  fpr2  8329  wfrdmclOLD  8357  wfrlem12OLD  8360  wfr2  8376  onoviun  8383  smoel  8400  smoiso  8402  smoel2  8403  smo11  8404  tfrlem9  8425  oalimcl  8598  oaass  8599  omordi  8604  omordlim  8615  omlimcl  8616  odi  8617  omeulem1  8620  omeulem2  8621  oen0  8624  oeordi  8625  oeordsuc  8632  oelimcl  8638  oeeulem  8639  oeeui  8640  nnmordi  8669  oaabs2  8687  omabs  8689  omsmolem  8695  ereldm  8795  iiner  8829  elmapg  8879  elpmg  8883  elixpsn  8977  ixpsnf1o  8978  boxriin  8980  omxpenlem  9113  pw2f1olem  9116  phplem2  9245  php3  9249  phplem4OLD  9257  php3OLD  9261  infn0  9340  elfi  9453  dffi3  9471  marypha2lem2  9476  ordiso2  9555  wemapsolem  9590  elharval  9601  inf3lemd  9667  inf3lem1  9668  inf3lem2  9669  inf3lem3  9670  cantnfs  9706  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1  9729  ttrclselem2  9766  trcl  9768  frr2  9800  r1sdom  9814  r1ordg  9818  r1pwss  9824  tz9.12lem3  9829  tz9.12  9830  r1elwf  9836  rankr1ai  9838  rankidb  9840  rankr1bg  9843  rankval2  9858  rankunb  9890  tcrank  9924  acni  10085  acni2  10086  acndom  10091  infpwfien  10102  alephnbtwn  10111  cardaleph  10129  cardinfima  10137  iunfictbso  10154  dfac3  10161  dfac5lem5  10167  dfac5  10169  dfac9  10177  dfac12r  10187  kmlem2  10192  kmlem12  10202  kmlem13  10203  kmlem14  10204  ackbij2lem3  10280  ackbij2  10282  cofsmo  10309  alephsing  10316  fin23lem30  10382  isf32lem9  10401  itunisuc  10459  axcc2lem  10476  axcc3  10478  domtriomlem  10482  axdc2lem  10488  axdc2  10489  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  ac6c4  10521  zorn2lem1  10536  ttukeylem6  10554  pwcfsdom  10623  axregndlem2  10643  axinfndlem1  10645  axacndlem4  10650  axacnd  10652  pwfseqlem1  10698  inar1  10815  inatsk  10818  gruurn  10838  grur1  10860  eltskm  10883  genpelv  11040  eluz1  12882  eluzaddOLD  12913  eluzsubOLD  12914  elixx1  13396  elixx3g  13400  elioo2  13428  elfz1  13552  elfz2  13554  elfzp1  13614  fzpr  13619  fzsuc2  13622  fzrev3  13630  elfzp12  13643  fzm1  13647  elfzo  13701  fz0add1fz1  13774  elfzo0l  13795  elfzom1b  13805  fzosplitsni  13817  elfzr  13819  elfzlmr  13820  zmodidfzo  13940  seqp1  14057  seqf1o  14084  bcval  14343  bcpasc  14360  hashf1lem1  14494  fundmge2nop0  14541  wrdmap  14584  elovmpowrd  14596  ccatfval  14611  elfzelfzccat  14618  ccatlid  14624  ccatass  14626  ccatrn  14627  ccatalpha  14631  swrdfv2  14699  ccatswrd  14706  swrdccat2  14707  pfxfv  14720  pfxeq  14734  ccatpfx  14739  swrdswrd  14743  swrdpfx  14745  pfxpfx  14746  cats1un  14759  swrdccatfn  14762  swrdccatin1  14763  pfxccatin12lem4  14764  pfxccatin12lem1  14766  swrdccatin2  14767  pfxccatin12lem2c  14768  pfxccatin12lem2  14769  swrdccat3blem  14777  swrdccatin1d  14781  swrdccatin2d  14782  pfxccatin12d  14783  revccat  14804  revrev  14805  repswpfx  14823  repswccat  14824  cshwidxmod  14841  2cshw  14851  cshwcshid  14866  cshwcsh2id  14867  cshimadifsn  14868  cshimadifsn0  14869  revco  14873  ccatco  14874  cshco  14875  swrdco  14876  ofccat  15008  shftfn  15112  shftval  15113  limsupgle  15513  ello12  15552  elo12  15563  isercolllem3  15703  sumeq1  15725  fsumsplit  15777  sumsplit  15804  fsum2dlem  15806  fsumcom2  15810  fsumparts  15842  explecnv  15901  pwdif  15904  fprodser  15985  fprodsplit  16002  fprod2dlem  16016  fprodcom2  16020  eftlub  16145  divalgmod  16443  bitsval  16461  bitsp1e  16469  bitsp1o  16470  sadfval  16489  sadcp1  16492  sadval  16493  sadcadd  16495  sadadd2  16497  saddisjlem  16501  sadadd  16504  sadass  16508  smufval  16514  smuval  16518  smuval2  16519  smupvallem  16520  smu01lem  16522  smueqlem  16527  smumul  16530  bezoutlem2  16577  bezoutlem4  16579  algfx  16617  eucalgcvga  16623  reumodprminv  16842  nnnn0modprm0  16844  unbenlem  16946  prmreclem5  16958  vdwapval  17011  vdwapun  17012  vdwnnlem1  17033  vdwnn  17036  ramval  17046  0ram  17058  ramub1lem2  17065  prmgaplem7  17095  prmlem0  17143  elrest  17472  prdsbasmpt  17515  prdsleval  17522  prdsbasmpt2  17527  pwselbasb  17533  imasaddfnlem  17573  imasvscafn  17582  divsfval  17592  ismre  17633  mreunirn  17644  mrisval  17673  ismri  17674  isacs  17694  catidd  17723  iscatd2  17724  ismon  17777  isepi  17784  sectffval  17794  sectfval  17795  dfiso2  17816  cicsym  17848  issubc  17880  catsubcat  17884  isfunc  17909  funcres  17941  funcpropd  17947  ffthiso  17976  isnat  17995  isnat2  17996  fuciso  18023  initoval  18038  termoval  18039  isinito  18041  istermo  18042  iszeroo  18043  isinitoi  18044  istermoi  18045  initoid  18046  termoid  18047  iszeroi  18054  2initoinv  18055  initoeu1  18056  initoeu2  18061  2termoinv  18062  termoeu1  18063  arwhoma  18090  elsetchom  18126  setcmon  18132  setcepi  18133  setciso  18136  catciso  18156  elestrchom  18172  estrcbasbas  18175  funcestrcsetclem7  18191  funcestrcsetclem8  18192  funcestrcsetclem9  18193  fthestrcsetc  18195  fullestrcsetc  18196  equivestrcsetc  18197  setc1strwun  18198  funcsetcestrclem7  18206  funcsetcestrclem8  18207  funcsetcestrclem9  18208  fthsetcestrc  18210  fullsetcestrc  18211  hofcl  18304  hofpropd  18312  yonedalem4c  18322  yonedainv  18326  yonffthlem  18327  lubeldm  18398  glbeldm  18411  joindef  18421  meetdef  18435  poslubdg  18459  acsficl2d  18597  acsmapd  18599  psref  18619  psss  18625  dirge  18648  mgmpropd  18664  issstrmgm  18666  grpidval  18674  grpidpropd  18675  grpidd  18684  ismgmhm  18709  issubmgm  18715  issgrpd  18743  sgrppropd  18744  ismndd  18769  mndpropd  18772  imasmnd2  18787  imasmnd  18788  xpsmnd0  18791  ismhm  18798  issubm  18816  gsumsgrpccat  18853  elefmndbas2  18887  smndex1mndlem  18922  imasgrp2  19073  imasgrp  19074  issubg  19144  subginv  19151  isnsg  19173  eqg0el  19201  quselbas  19202  isghm  19233  isghmOLD  19234  resghm2b  19252  conjnmzb  19271  conjnsg  19272  ghmpropd  19274  isga  19309  elcntz  19340  elcntzsn  19343  cntzrcl  19345  resscntz  19351  symgextf1  19439  gsmsymgreqlem2  19449  f1otrspeq  19465  pmtrfrn  19476  pmtrdifellem3  19496  pmtrdifellem4  19497  psgnunilem1  19511  psgnunilem5  19512  psgnunilem2  19513  psgnunilem3  19514  psgneldm2  19522  psgnfitr  19535  psgnsn  19538  gexdvds  19602  gex1  19609  isslw  19626  sylow3lem2  19646  lsmelvalx  19658  pj1ghm  19721  efgtlen  19744  efgsfo  19757  efgredlemc  19763  frgp0  19778  frgpmhm  19783  qusabl  19883  frgpnabllem1  19891  imasabl  19894  cycsubmcmn  19907  0cyg  19911  cycsubgcyg  19919  gsumval3  19925  gsumcllem  19926  gsumzaddlem  19939  gsumzsplit  19945  gsummptfzcl  19987  eldprd  20024  dprdcntz2  20058  dprd2d2  20064  dmdprdsplit2lem  20065  dmdprdsplit2  20066  dprdsplit  20068  ablfac2  20109  isrngd  20170  rngpropd  20171  imasrng  20174  qusrng  20177  ringurd  20182  isringd  20288  imasring  20327  xpsring1d  20330  dvdsrval  20361  isunit  20373  dvdsrpropd  20416  isirred  20419  isrnghm  20441  isrngim  20445  c0ghm  20461  c0snghm  20464  isrhm  20478  isrim0OLD  20481  isrim0  20483  islring  20540  issubrng  20547  opprsubrng  20559  issubrg  20571  opprsubrg  20593  resrhm2b  20602  rhmpropd  20609  rnghmresel  20620  elrngchom  20624  rnghmsubcsetclem1  20631  rnghmsubcsetclem2  20632  rngcid  20635  rngcsect  20636  rngciso  20638  funcrngcsetcALT  20641  zrinitorngc  20642  zrtermorngc  20643  rhmresel  20649  elringchom  20653  rhmsubcsetclem1  20660  rhmsubcsetclem2  20661  ringcid  20664  rhmsscrnghm  20665  rhmsubcrngclem1  20666  rhmsubcrngclem2  20667  ringcsect  20670  ringciso  20672  ringcbasbas  20673  zrtermoringc  20675  srhmsubc  20680  rhmsubclem3  20687  rhmsubclem4  20688  drngunit  20734  isdrngd  20765  isdrngdOLD  20767  issdrg  20789  sdrgunit  20797  isabv  20812  issrngd  20856  islmod  20862  lmodprop2d  20922  islss  20932  islssd  20933  lssats2  20998  ellspsn  21001  islmhm  21026  lmhmf1o  21045  lmhmima  21046  lmhmpreima  21047  reslmhm  21051  pwssplit3  21060  lmhmpropd  21072  islbs  21075  lspprel  21093  lspfixed  21130  lbsacsbs  21158  lbsextlem1  21160  lbsextlem2  21161  lbsextlem3  21162  lbsextlem4  21163  ixpsnbasval  21215  isridlrng  21229  rnglidlmmgm  21255  isridl  21262  quscrng  21293  rngqiprngimfolem  21300  rngqiprngimf1lem  21304  rngqiprngimfo  21311  islpidl  21335  lidldvgen  21344  irinitoringc  21490  pzriprnglem13  21504  pzriprnglem14  21505  zrhrhmb  21521  znf1o  21570  frgpcyg  21592  psgnevpmb  21605  isphld  21672  phlssphl  21677  elocv  21686  iscss  21701  isobs  21740  obs2ss  21749  dsmmfi  21758  dsmmelbas  21759  dsmmlss  21764  frlmelbas  21776  frlmlbs  21817  frlmup1  21818  ellspd  21822  islinds  21829  islindf2  21834  f1lindf  21842  islindf4  21858  assamulgscmlem2  21920  psrgrp  21976  mplsubglem  22019  mpllsslem  22020  mplmonmul  22054  subrgascl  22090  subrgasclcl  22091  mpfind  22131  ismhp  22144  gsumply1subr  22235  lply1binomsc  22315  matbas2d  22429  matecl  22431  matvscl  22437  mat1  22453  mat0dim0  22473  mat0dimid  22474  mat0dimscm  22475  mat1dimelbas  22477  dmatel  22499  scmatel  22511  scmateALT  22518  scmataddcl  22522  scmatsubcl  22523  smatvscl  22530  scmatghm  22539  mat1scmat  22545  mdetunilem7  22624  mdetunilem9  22626  smadiadetr  22681  cramerimplem2  22690  cramer0  22696  pmatcoe1fsupp  22707  cpmatpmat  22716  cpmatel  22717  cpmatacl  22722  cpmatinvcl  22723  mat2pmatghm  22736  mat2pmatmul  22737  decpmatmullem  22777  pmatcollpwlem  22786  pmatcollpw3fi1lem1  22792  pmatcollpwscmatlem1  22795  monmat2matmon  22830  chfacfscmul0  22864  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  cayhamlem1  22872  cpmadugsumlemB  22880  cpmadugsumlemC  22881  cpmadugsumlemF  22882  cayhamlem2  22890  istopon  22918  eltg  22964  eltg2  22965  eltop  22981  eltop2  22982  eltop3  22983  pptbas  23015  iscld  23035  neiss2  23109  isnei  23111  neiptopnei  23140  neiptopreu  23141  lpfval  23146  lpval  23147  islp  23148  maxlp  23155  islpi  23157  neitr  23188  restlp  23191  ordtbas2  23199  ordtrest2  23212  lmfval  23240  cnfval  23241  iscn  23243  iscnp  23245  tgcn  23260  tgcnp  23261  lmbrf  23268  cnpresti  23296  ist1  23329  ist1-2  23355  cnt1  23358  haust1  23360  cmpfi  23416  cmpfii  23417  1stcfb  23453  2ndc1stc  23459  1stcrest  23461  2ndcdisj  23464  1stcelcls  23469  nllyi  23483  subislly  23489  islocfin  23525  lfinpfin  23532  locfindis  23538  locfincf  23539  comppfsc  23540  kgenval  23543  elkgen  23544  kgencn2  23565  txbas  23575  eltx  23576  ptval  23578  ptpjpre1  23579  ptopn2  23592  ptpjopn  23620  ptclsg  23623  xkoccn  23627  txdis  23640  txdis1cn  23643  ptrescn  23647  hausdiag  23653  hauseqlcld  23654  txhaus  23655  xkohaus  23661  elqtop  23705  qtopeu  23724  kqcldsat  23741  hmeofval  23766  ptuncnv  23815  ptunhmeo  23816  elmptrab  23835  fbdmn0  23842  elfg  23879  elfilss  23884  filunirn  23890  fixufil  23930  elfm  23955  rnelfmlem  23960  rnelfm  23961  fmfnfmlem4  23965  elflim2  23972  flimtopon  23978  elflim  23979  hausflim  23989  flimcls  23993  flfnei  23999  isflf  24001  hausflf  24005  cnpflf  24009  cnflf  24010  txflf  24014  isfcls  24017  fclstopon  24020  isfcls2  24021  fclssscls  24026  fclsnei  24027  fclsfnflim  24035  flimfnfcls  24036  isfcf  24042  fcfelbas  24044  cnpfcf  24049  cnfcf  24050  flfcntr  24051  alexsublem  24052  alexsubALTlem3  24057  cnextfun  24072  cnextfvval  24073  cnextf  24074  cnextcn  24075  tmdgsum2  24104  tgpconncomp  24121  ghmcnp  24123  qustgplem  24129  eltsms  24141  haustsms  24144  tsmsgsum  24147  tsmssubm  24151  tsmssplit  24160  isust  24212  ustbas  24236  elutop  24242  ustuqtoplem  24248  ustuqtop4  24253  ustuqtop  24255  utopsnneiplem  24256  utopsnneip  24257  utopsnnei  24258  isusp  24270  isucn  24287  ucncn  24294  iscfilu  24297  neipcfilu  24305  iscusp  24308  cnextucn  24312  ispsmet  24314  ismet  24333  isxmet  24334  elblps  24397  elbl  24398  elmopn  24452  prdsbl  24504  neibl  24514  met1stc  24534  metrest  24537  prdsxmslem2  24542  txmetcnp  24560  txmetcn  24561  metustsym  24568  cfilucfil2  24574  elbl4  24576  metuel  24577  psmetutop  24580  restmetu  24583  metucn  24584  tngngp  24675  isnmhm  24767  zcld  24835  metnrmlem1a  24880  elcncf  24915  cncfcnvcn  24952  cnheibor  24987  lebnumlem1  24993  ishtpy  25004  isphtpy  25013  om1elbas  25065  elpi1  25078  pi1xfr  25088  pi1coghm  25094  tcphcph  25271  lmmbrf  25296  iscfil  25299  iscau  25310  iscauf  25314  caucfil  25317  iscmet  25318  cmetcaulem  25322  iscmet3lem1  25325  iscmet3lem2  25326  iscmet3  25327  bcthlem1  25358  cmsss  25385  cmetcusp1  25387  cmetcusp  25388  cmscsscms  25407  rrxcph  25426  minveclem3b  25462  ovolfioo  25502  ovolficc  25503  ovolctb  25525  ovoliunnul  25542  ovolshftlem1  25544  sca2rab  25547  ovolscalem1  25548  ovolicc2lem1  25552  ovolicc2lem2  25553  ovolicc2lem4  25555  ovolicc2lem5  25556  iundisj  25583  iunmbl2  25592  uniioombllem3  25620  vitalilem2  25644  vitalilem3  25645  mbfss  25681  i1faddlem  25728  i1fmullem  25729  mbfi1fseqlem2  25751  mbfi1fseqlem4  25753  mbfi1fseq  25756  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itg2gt0  25795  isibl  25800  iblss2  25841  itgss3  25850  itgsplit  25871  ellimc  25908  limcmo  25917  cnlimc  25923  limciun  25929  limcun  25930  eldv  25933  dvbsss  25937  dvreslem  25944  elcpn  25970  dvaddf  25979  dvmulf  25980  dvcof  25986  rolle  26028  dvlip2  26034  dvivthlem1  26047  lhop1  26053  lhop2  26054  ftc1cn  26084  fta1glem2  26208  plyco0  26231  elply  26234  ply1termlem  26242  eltayl  26401  tayl0  26403  taylplem1  26404  taylplem2  26405  dvtaylp  26412  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  abelth  26485  cxpcn3  26791  rlimcnp  27008  fsumharmonic  27055  dchrelbas  27280  pntrsumbnd2  27611  ostth2lem2  27678  nolesgn2ores  27717  nogesgn1ores  27719  nosupprefixmo  27745  noinfprefixmo  27746  nosupcbv  27747  nosupdm  27749  nosupfv  27751  nosupres  27752  nosupbnd1lem1  27753  nosupbnd1lem3  27755  nosupbnd1lem5  27757  nosupbnd2lem1  27760  noinfcbv  27762  noinfdm  27764  noinffv  27766  noinfres  27767  noinfbnd1lem1  27768  noinfbnd1lem3  27770  noinfbnd1lem5  27772  noinfbnd2lem1  27775  elmade  27906  elold  27908  ssltleft  27909  ssltright  27910  oldlim  27925  madebday  27938  newbday  27940  sltlpss  27945  cofcutr  27958  cofcutrtime  27961  lrrecval  27972  lrrecval2  27973  addsval  27995  precsexlem9  28239  precsexlem11  28241  sltonold  28283  noseqrdgfn  28312  istrkgb  28463  istrkgcb  28464  istrkge  28465  istrkgl  28466  istrkgld  28467  axtgsegcon  28472  axtg5seg  28473  axtgbtwnid  28474  axtgpasch  28475  axtgupdim2  28479  axtgeucl  28480  tgdim01  28515  iscgrg  28520  isismt  28542  tglnunirn  28556  tglngval  28559  tgellng  28561  legval  28592  legov  28593  legov2  28594  ishlg  28610  mirreu3  28662  mirval  28663  mirfv  28664  mircgr  28665  mirbtwn  28666  ismir  28667  mireq  28673  symquadlem  28697  israg  28705  perpln1  28718  perpln2  28719  isperp  28720  islnopp  28747  outpasch  28763  ishpg  28767  iscgra  28817  dfcgra2  28838  isinag  28846  isleag  28855  iseqlg  28875  f1otrgitv  28878  f1otrg  28879  f1otrge  28880  ttgval  28883  ttgvalOLD  28884  ttgelitv  28897  elee  28909  brbtwn  28914  brcgr  28915  axlowdimlem16  28972  ebtwntg  28997  elntg2  29000  upgrex  29109  edgupgr  29151  upgredg  29154  edglnl  29160  numedglnl  29161  uhgr2edg  29225  umgr2edg1  29228  usgredg2vlem1  29242  usgredg2vlem2  29243  ushgredgedg  29246  ushgredgedgloop  29248  uhgrspansubgrlem  29307  fusgrfisstep  29346  nbgrval  29353  nbgrel  29357  nbupgrel  29362  nbgr2vtx1edg  29367  nbuhgr2vtx1edgblem  29368  nbuhgr2vtx1edgb  29369  nbusgreledg  29370  usgrnbcnvfv  29382  uvtxval  29404  uvtxel  29405  uvtx01vtx  29414  uvtxusgrel  29420  nbcplgr  29451  cplgr3v  29452  cusgrexi  29460  structtocusgr  29463  vtxdgfval  29485  vtxdg0v  29491  vtxdeqd  29495  vtxdun  29499  1loopgrnb0  29520  1loopgrvd0  29522  1hevtxdg0  29523  1hevtxdg1  29524  1egrvtxdg1  29527  umgr2v2evtxel  29540  umgr2v2enb1  29544  umgr2v2evd2  29545  vtxdginducedm1lem4  29560  vtxdginducedm1  29561  finsumvtxdg2sstep  29567  ewlksfval  29619  isewlk  29620  wksfval  29627  iswlk  29628  uspgr2wlkeq  29664  wlkres  29688  dfpth2  29749  usgr2pthlem  29783  clwlkcompim  29800  uspgrn2crct  29828  wwlks  29855  iswwlksn  29858  wwlknvtx  29865  wlkiswwlks2  29895  wwlksm1edg  29901  wwlksnred  29912  wwlksnext  29913  wwlksnredwwlkn  29915  wwlksnredwwlkn0  29916  wwlksnwwlksnon  29935  wspn0  29944  usgr2wspthons3  29984  rusgrnumwwlkb0  29991  clwwlk  30002  clwwlkccatlem  30008  clwlkclwwlklem2a4  30016  clwlkclwwlk  30021  clwwisshclwwslem  30033  clwwlkinwwlk  30059  clwwlkel  30065  clwwlkf  30066  clwwlkext2edg  30075  wwlksext2clwwlk  30076  wwlksubclwwlk  30077  clwwnisshclwwsn  30078  eleclclwwlknlem2  30080  erclwwlknsym  30089  erclwwlkntr  30090  umgrhashecclwwlk  30097  clwwlkvbij  30132  eupth2lem3lem3  30249  eupth2lem3lem4  30250  eupth2lem3lem6  30252  eupth2lemb  30256  eucrct2eupth  30264  fusgreg2wsplem  30352  2clwwlklem  30362  2clwwlk2clwwlklem  30365  2clwwlkel  30368  2clwwlk2clwwlk  30369  extwwlkfabel  30372  clwwlknonclwlknonf1o  30381  dlwwlknondlwlknonf1olem1  30383  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  ex-res  30460  isssp  30743  sspn  30755  islno  30772  isblo  30801  nmlno0  30814  ishmo  30830  dipdir  30861  dipass  30864  ubthlem1  30889  ubthlem2  30890  htthlem  30936  htth  30937  ocel  31300  ocnel  31317  shsel  31333  shsel2  31341  shmodsi  31408  pjhtheu  31413  pjeq  31418  axpjpj  31439  pjoc2  31458  elspani  31562  h1de2ctlem  31574  elspansn  31585  elspansn2  31586  elnlfn  31947  eleigvec  31976  riesz3i  32081  cbviunf  32568  iuneq12daf  32569  iunrdx  32576  iunrnmptss  32578  cbvdisjf  32584  disjorf  32592  disjabrex  32595  disjabrexf  32596  iundisjf  32602  disjrdx  32604  brab2d  32619  2ndresdju  32659  abfmpunirn  32662  abfmpeld  32664  abfmpel  32665  fmptcof2  32667  acunirnmpt2  32670  acunirnmpt2f  32671  aciunf1lem  32672  funcnvmpt  32677  suppss3  32735  fpwrelmap  32744  xrofsup  32771  iundisjfi  32798  eliccioo  32913  s3f1  32931  ccatf1  32933  ccatws1f1o  32936  swrdrn3  32940  ismnt  32973  mgcoval  32976  chnccats1  33005  gsummpt2co  33051  gsumpart  33060  gsumhashmul  33064  xrge0tsmsbi  33066  gsumwrd2dccatlem  33069  gsumwrd2dccat  33070  cycpmco2  33153  cyc3co2  33160  inftmrel  33187  isinftm  33188  isslmd  33208  urpropd  33236  elrgspn  33250  erlval  33262  rlocval  33263  rloccring  33274  rloc1r  33276  domnpropd  33280  isdrng4  33298  fracfld  33310  resv1r  33368  ellspds  33396  ellpi  33401  lbslsp  33405  rhmimaidl  33460  isprmidl  33466  qsidomlem1  33480  qsidomlem2  33481  ismxidl  33490  crngmxidl  33497  drng0mxidl  33504  opprqus0g  33518  qsfld  33526  isrprm  33545  rsprprmprmidlb  33551  ply1mulrtss  33606  dimpropd  33659  lbslsat  33667  extdg1id  33716  fldextrspunlsplem  33723  fldextrspunlsp  33724  elirng  33736  ply1annidllem  33744  constrsuc  33779  constrconj  33786  smatrcl  33795  smatcl  33801  ist0cld  33832  txomap  33833  locfinreflem  33839  zarclsiin  33870  zart0  33878  rhmpreimacnlem  33883  metidval  33889  cnre2csqima  33910  ordtrest2NEW  33922  fmcncfil  33930  fsumcvg4  33949  ofcfval  34099  measvuni  34215  meascnbl  34220  faeval  34247  ismbfm  34252  elunirnmbfm  34253  imambfm  34264  elcarsg  34307  itgeq12dv  34328  issibf  34335  eulerpartlems  34362  eulerpartlemgc  34364  eulerpartlemgvv  34378  eulerpartlemgu  34379  eulerpart  34384  rrvmbfm  34444  elorvc  34462  elorrvc  34466  dstfrvunirn  34477  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemsima  34518  ballotlemrv  34522  fzssfzo  34554  signstfvn  34584  signstfvneq0  34587  signstres  34590  repr0  34626  reprinrn  34633  reprdifc  34642  hgt750lemg  34669  hgt750lemb  34671  istrkg2d  34681  axtgupdim2ALTV  34683  afsval  34686  brafs  34687  bnj945  34787  bnj1400  34849  bnj18eq1  34941  bnj916  34947  bnj1014  34975  bnj1015  34976  bnj1110  34996  bnj1417  35055  revpfxsfxrev  35121  cplgredgex  35126  pfxwlk  35129  revwlk  35130  subfacp1lem2b  35186  subfacp1lem4  35188  subfacp1lem5  35189  subfacp1lem6  35190  ptpconn  35238  cvmscbv  35263  iscvm  35264  cvmsi  35270  cvmsval  35271  cvmliftmolem1  35286  cvmlift2lem12  35319  cvmlift2lem13  35320  cvmlift3lem7  35330  snmlval  35336  satfv1  35368  satfvsucsuc  35370  satfrnmapom  35375  satf0op  35382  satf0n0  35383  sat1el2xp  35384  fmlafvel  35390  isfmlasuc  35393  fmlaomn0  35395  gonan0  35397  goaln0  35398  gonar  35400  goalr  35402  satffunlem1lem2  35408  satffunlem2lem2  35411  satfv0fvfmla0  35418  satef  35421  satefvfmla0  35423  sategoelfvb  35424  satfv1fvfmla1  35428  mrsubfval  35513  mrsubvrs  35527  mclsrcl  35566  mclsval  35568  mppsval  35577  mclsppslem  35588  opelco3  35775  wsuclem  35826  funtransport  36032  fvtransport  36033  brcolinear  36060  colineardim1  36062  funray  36141  fvray  36142  funline  36143  fvline  36145  lineelsb2  36149  fwddifval  36163  fwddifnval  36164  rankelg  36169  rankeq1o  36172  elhf2  36176  0hf  36178  rmoeqbidv  36214  disjeq12dv  36216  ixpeq12dv  36217  prodeq12sdv  36219  itgeq12sdv  36220  cbvralvw2  36227  cbvrexvw2  36228  cbvrmovw2  36229  cbvreuvw2  36230  cbvcsbvw2  36232  cbviunvw2  36233  cbviinvw2  36234  cbvmptvw2  36235  cbvdisjvw2  36236  cbvmpo1vw2  36244  cbvmpo2vw2  36245  cbvsbcdavw  36258  cbvcsbdavw  36260  cbvcsbdavw2  36261  cbviundavw  36263  cbviindavw  36264  cbvdisjdavw  36269  cbvrabdavw2  36286  cbviundavw2  36287  cbviindavw2  36288  cbvmptdavw2  36289  cbvdisjdavw2  36290  cbvriotadavw2  36291  cbvmpo1davw2  36293  cbvmpo2davw2  36294  cbvsumdavw2  36296  neibastop2lem  36361  neibastop3  36363  eltail  36375  bj-projeq  36993  bj-projval  36997  bj-restsn  37083  opelopabbv  37144  brabd0  37148  bj-eldiag  37177  bj-eldiag2  37178  mptsnunlem  37339  dissneqlem  37341  iooelexlt  37363  relowlssretop  37364  rdgellim  37377  exrecfnlem  37380  finxpeq1  37387  finxpreclem6  37397  pibp21  37416  curf  37605  uncf  37606  curunc  37609  unccur  37610  fin2so  37614  lindsadd  37620  lindsdom  37621  lindsenlbs  37622  matunitlindflem1  37623  matunitlindflem2  37624  matunitlindf  37625  ptrest  37626  ptrecube  37627  poimirlem2  37629  poimirlem8  37635  poimirlem17  37644  poimirlem18  37645  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem24  37651  poimirlem26  37653  poimirlem29  37656  heicant  37662  mblfinlem1  37664  mblfinlem2  37665  volsupnfl  37672  itg2addnclem  37678  itg2gt0cn  37682  indexdom  37741  incsequz  37755  istotbnd  37776  istotbnd3  37778  0totbnd  37780  sstotbnd  37782  sstotbnd3  37783  isbnd  37787  prdstotbnd  37801  cntotbnd  37803  isismty  37808  heibor1lem  37816  heiborlem2  37819  heiborlem3  37820  heibor  37828  isass  37853  exidcl  37883  exidreslem  37884  elghomlem2OLD  37893  rngoidmlem  37943  rngo1cl  37946  divrngcl  37964  isdrngo2  37965  isrngohom  37972  isrngoiso  37985  isriscg  37991  iscom2  38002  iscringd  38005  isidl  38021  ispridl  38041  ismaxidl  38047  ac6s6  38179  dmecd  38305  releldmqs  38659  releldmqscoss  38661  erimeq2  38679  eldisjlem19  38811  membpartlem19  38812  prter3  38883  islshp  38980  islsat  38992  lcvfbr  39021  islfl  39061  ellkr  39090  islshpkrN  39121  ldual1dim  39167  isopos  39181  cmtfvalN  39211  cvrfval  39269  isat  39287  islln  39508  islpln  39532  islvol  39575  isline  39741  ispointN  39744  ispsubsp  39747  elpmap  39760  elpmapat  39766  elpadd  39801  paddclN  39844  elpclN  39894  elpcliN  39895  pclfinN  39902  pclcmpatN  39903  ispsubclN  39939  iswatN  39996  islhp  39998  islaut  40085  ispautN  40101  isldil  40112  isltrn  40121  isdilN  40156  istrnN  40159  istendo  40762  dvhb1dimN  40988  erng1lem  40989  erngdvlem4-rN  41001  diaelval  41035  diaeldm  41038  dia1dimid  41065  cdlemm10N  41120  dibopelvalN  41145  dibopelval2  41147  dibelval3  41149  dibelval1st  41151  dibelval2nd  41154  dibeldmN  41160  dibvalrel  41165  dibglbN  41168  dicffval  41176  dicfval  41177  dicopelval  41179  dicelvalN  41180  dicelval3  41182  dicvalrelN  41187  dicelval1sta  41189  diclspsn  41196  dihopelvalbN  41240  dihopelvalcqat  41248  dihopelvalcpre  41250  dihvalrel  41281  dih1  41288  dihmeetlem4preN  41308  dihmeetlem13N  41321  dih1dimatlem  41331  dochnel2  41394  dihjatcclem4  41423  dvh2dim  41447  dvh3dim  41448  dvh4dimN  41449  dochfln0  41479  lpolsetN  41484  islpolN  41485  lcfrvalsnN  41543  lcfrlem21  41565  lcfrlem27  41571  lcfrlem37  41581  lcfr  41587  lcdlss  41621  mapdcv  41662  hdmap1fval  41798  hdmapffval  41828  hdmapfval  41829  hdmapval  41830  hgmapffval  41887  hgmapfval  41888  hdmapellkr  41916  hlhilhillem  41966  fzsplitnd  41983  isprimroot  42094  primrootsunit1  42098  primrootscoprmpow  42100  primrootscoprbij  42103  aks6d1c1p2  42110  aks6d1c1p3  42111  aks6d1c1p4  42112  aks6d1c1p5  42113  aks6d1c1p6  42115  aks6d1c1  42117  evl1gprodd  42118  sticksstones11  42157  sticksstones12a  42158  rhmqusspan  42186  grpods  42195  fzosumm1  42291  frlmfielbas  42510  frlmsnic  42550  psrmnd  42555  isnacs  42715  mrefg2  42718  elmzpcl  42737  mzpcompact2  42763  eldiophb  42768  elpell1qr  42858  elpell14qr  42860  elpell1234qr  42862  pw2f1ocnv  43049  pw2f1o2val2  43052  aomclem4  43069  aomclem6  43071  islssfg2  43083  imasgim  43112  lnr2i  43128  elmnc  43148  rngunsnply  43181  onexomgt  43253  onexlimgt  43255  onexoegt  43256  oaordnr  43309  omnord1  43318  oenord1  43329  cantnfresb  43337  tfsconcatun  43350  tfsconcat0i  43358  ofoaf  43368  naddcnff  43375  naddcnffo  43377  naddcnfcom  43379  naddcnfid1  43380  naddcnfid2  43381  naddcnfass  43382  naddwordnexlem4  43414  fiinfi  43586  sqrtcvallem1  43644  elintima  43666  eliunov2  43692  ov2ssiunov2  43713  brtrclfv2  43740  rfovcnvf1od  44017  rfovcnvfvd  44020  fsovrfovd  44022  fsovfvd  44023  fsovcnvlem  44026  ntrclsfv1  44068  ntrclselnel1  44070  ntrclsneine0lem  44077  ntrneifv1  44092  ntrneifv2  44093  ntrneiel  44094  gneispace2  44145  gneispacess2  44159  extoimad  44177  mnringelbased  44233  dvconstbi  44353  bccbc  44364  wfac8prim  45019  eliin2f  45109  iineq12dv  45111  rabbida2  45137  disjinfi  45197  unirnmap  45213  elmptima  45265  iuneqfzuzlem  45345  iooiinioc  45569  fsumiunss  45590  fsumsupp0  45593  lptre2pt  45655  icccncfext  45902  cncfiooicclem1  45908  dvnprodlem2  45962  stoweidlem27  46042  stoweidlem29  46044  stoweidlem31  46046  stoweidlem34  46049  stoweidlem48  46063  stoweidlem59  46074  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem2  46124  fourierdlem3  46125  fourierdlem25  46147  fourierdlem32  46154  fourierdlem33  46155  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem62  46183  fourierdlem70  46191  fourierdlem80  46201  fourierdlem92  46213  fourierdlem93  46214  fourierdlem101  46222  etransclem37  46286  sge0val  46381  sge0f1o  46397  sge0iunmptlemre  46430  sge0iunmpt  46433  iundjiun  46475  caragenel  46510  ovncvrrp  46579  ovnsubaddlem1  46585  ovnsubadd  46587  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hoidmvle  46615  ovncvr2  46626  hspdifhsp  46631  hoiqssbl  46640  hspmbllem2  46642  hspmbl  46644  opnvonmbllem1  46647  isvonmbl  46653  ovnovollem1  46671  issmflem  46742  smflimlem3  46788  smflimlem4  46789  smflim  46792  smfmullem2  46807  smflimmpt  46825  smfsuplem1  46826  smflimsuplem1  46835  smflimsuplem3  46837  smflimsuplem4  46838  smflimsuplem7  46841  smflimsup  46843  tworepnotupword  46901  fcores  47079  fcoresf1  47081  afvelrnb  47175  afvelrnb0  47176  afv2co2  47269  el1fzopredsuc  47337  iccpart  47403  iccpartgtprec  47407  iccpartiltu  47409  iccpartigtl  47410  iccpartltu  47412  iccpartgtl  47413  iccpartgt  47414  iccpartleu  47415  iccpartgel  47416  iccelpart  47420  iccpartiun  47421  icceuelpart  47423  fargshiftfv  47426  fargshiftfo  47429  sprel  47471  prprelb  47503  prprelprb  47504  fpprel  47715  sbgoldbo  47774  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem3  47794  bgoldbtbnd  47796  clnbgrval  47809  elclnbgrelnbgr  47812  clnbgrel  47815  clnbupgrel  47821  vopnbgrel  47840  isubgredg  47852  uspgrimprop  47873  grtriprop  47908  isgrtri  47910  grtriclwlk3  47912  stgredgel  47924  gpgvtxel  48005  gpgedgel  48007  opgpgvtx  48010  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  gpg3kgrtriex  48045  upwlksfval  48051  isupwlk  48052  intop  48119  isclintop  48123  assintop  48125  isassintop  48126  assintopcllaw  48128  uzlidlring  48151  elrngchomALTV  48185  rngccatidALTV  48188  rngcsectALTV  48191  rngcisoALTV  48193  rhmsubcALTVlem3  48199  rhmsubcALTVlem4  48200  funcringcsetcALTV2lem7  48212  funcringcsetcALTV2lem9  48214  elringchomALTV  48219  ringccatidALTV  48222  ringcsectALTV  48225  ringcisoALTV  48227  ringcbasbasALTV  48228  funcringcsetclem7ALTV  48235  funcringcsetclem9ALTV  48237  srhmsubcALTV  48241  cbvmpox2  48252  ply1sclrmsm  48300  dmatALTbasel  48319  lcoval  48329  lindslinindsimp1  48374  lindslinindsimp2  48380  lmod1  48409  elbigo  48472  elbigo2  48473  elbigolo1  48478  dig2nn0ld  48525  naryfvalel  48551  rrxlines  48654  rrxlinesc  48656  rrxlinec  48657  eenglngeehlnm  48660  elrrx2linest2  48666  rrxsphere  48669  itsclc0  48692  itsclc0b  48693  itsclinecirc0  48694  itsclinecirc0b  48695  itscnhlinecirc02p  48706  brab2dd  48741  f1omo  48792  lubeldm2d  48855  glbeldm2d  48856  catprs  48900  upfval  48933  upfval2  48934  upfval3  48935  isthinc  49069  isthincd2lem1  49075  thincmoALT  49078  thincmod  49079  isthincd  49085  thincpropd  49091  prsthinc  49111  termcterm  49145  termc2  49148  elsetrecslem  49218