Theorem eleq2d 2813

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

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

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

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

This theorem is referenced by:  eleq2  2816  eleq12d  2821  eleqtrd  2829  neleqtrd  2849  eqabrd  2870  nfceqdfOLD  2893  drnfc1OLD  2917  drnfc2OLD  2919  raleqbidv  3336  rexeqbidv  3337  elabd2  3655  sbcbid  3830  csbeq2d  3894  cbvcsbw  3898  cbvcsb  3899  csbie  3924  csbied  3926  csbie2g  3931  cbvralcsf  3933  cbvreucsf  3935  cbvrabcsf  3936  sbcel12  4403  sbcel1g  4408  sbcel2  4410  prel12g  4859  eliuni  4996  iuneqconst  5001  iuneq12df  5016  cbviun  5032  cbviin  5033  cbviung  5034  cbviing  5035  iinxsng  5084  iinxprg  5085  iunxsng  5086  iunxsngf  5088  cbvdisj  5116  disjor  5121  disjiund  5131  mpteq12da  5226  mpteq12dfOLD  5228  mpteq12f  5229  mpteq12dva  5230  axpweq  5341  rabxfrd  5408  rbropapd  5557  opeliunxp  5736  opeliunxp2  5831  iunxpf  5841  elrelimasn  6077  elimasngOLD  6082  elimasni  6083  xpdifid  6160  ressn  6277  predbrg  6315  funfni  6648  fnbr  6650  dffv3  6880  elfv2ex  6930  fvelrnb  6945  foelcdmi  6946  fvun1  6975  fvco2  6981  elfvmptrab1w  7017  elfvmptrab1  7018  elfvmptrab  7019  elpreima  7052  dff3  7094  fmptco  7122  fnelfp  7168  fnelnfp  7170  tpres  7197  fnprb  7204  fntpb  7205  funfvima3  7232  eluniima  7244  elunirn2OLD  7247  dff13  7249  f1eqcocnv  7294  f1eqcocnvOLD  7295  isoini  7330  riotaeqdv  7361  mpoeq123dva  7478  cbvmpox  7497  ovelrn  7579  elovmpo  7647  elovmporab  7648  elovmporab1w  7649  elovmporab1  7650  elovmpt3rab1  7662  fiun  7925  f1iun  7926  zfrep6  7937  fmpox  8049  el2mpocsbcl  8068  el2mpocl  8069  bropopvvv  8073  bropfvvvv  8075  xpord2indlem  8130  xpord3inddlem  8137  elsuppfng  8152  elsuppfn  8153  suppfnss  8171  opeliunxp2f  8193  mpoxopn0yelv  8196  mpoxopovel  8203  rntpos  8222  mpocurryd  8252  fpr2  8287  wfrdmclOLD  8315  wfrlem12OLD  8318  wfr2  8334  onoviun  8341  smoel  8358  smoiso  8360  smoel2  8361  smo11  8362  tfrlem9  8383  oalimcl  8558  oaass  8559  omordi  8564  omordlim  8575  omlimcl  8576  odi  8577  omeulem1  8580  omeulem2  8581  oen0  8584  oeordi  8585  oeordsuc  8592  oelimcl  8598  oeeulem  8599  oeeui  8600  nnmordi  8629  oaabs2  8647  omabs  8649  omsmolem  8655  ereldm  8750  iiner  8782  elmapg  8832  elpmg  8836  elixpsn  8930  ixpsnf1o  8931  boxriin  8933  omxpenlem  9072  pw2f1olem  9075  phplem2  9207  php3  9211  phplem4OLD  9219  php3OLD  9223  infn0  9306  elfi  9407  dffi3  9425  marypha2lem2  9430  ordiso2  9509  wemapsolem  9544  elharval  9555  inf3lemd  9621  inf3lem1  9622  inf3lem2  9623  inf3lem3  9624  cantnfs  9660  cantnfp1lem3  9674  cantnflem1b  9680  cantnflem1  9683  ttrclselem2  9720  trcl  9722  frr2  9754  r1sdom  9768  r1ordg  9772  r1pwss  9778  tz9.12lem3  9783  tz9.12  9784  r1elwf  9790  rankr1ai  9792  rankidb  9794  rankr1bg  9797  rankval2  9812  rankunb  9844  tcrank  9878  acni  10039  acni2  10040  acndom  10045  infpwfien  10056  alephnbtwn  10065  cardaleph  10083  cardinfima  10091  iunfictbso  10108  dfac3  10115  dfac5lem5  10121  dfac5  10122  dfac9  10130  dfac12r  10140  kmlem2  10145  kmlem12  10155  kmlem13  10156  kmlem14  10157  ackbij2lem3  10235  ackbij2  10237  cofsmo  10263  alephsing  10270  fin23lem30  10336  isf32lem9  10355  itunisuc  10413  axcc2lem  10430  axcc3  10432  domtriomlem  10436  axdc2lem  10442  axdc2  10443  axdc3lem2  10445  axdc3lem4  10447  axdc4lem  10449  ac6c4  10475  zorn2lem1  10490  ttukeylem6  10508  pwcfsdom  10577  axregndlem2  10597  axinfndlem1  10599  axacndlem4  10604  axacnd  10606  pwfseqlem1  10652  inar1  10769  inatsk  10772  gruurn  10792  grur1  10814  eltskm  10837  genpelv  10994  eluz1  12827  eluzaddOLD  12858  eluzsubOLD  12859  elixx1  13336  elixx3g  13340  elioo2  13368  elfz1  13492  elfz2  13494  elfzp1  13554  fzpr  13559  fzsuc2  13562  fzrev3  13570  elfzp12  13583  fzm1  13584  elfzo  13637  fz0add1fz1  13705  elfzo0l  13725  elfzom1b  13734  fzosplitsni  13746  elfzr  13748  elfzlmr  13749  zmodidfzo  13868  seqp1  13984  seqf1o  14012  bcval  14267  bcpasc  14284  hashf1lem1  14419  hashf1lem1OLD  14420  fundmge2nop0  14457  wrdmap  14500  elovmpowrd  14512  ccatfval  14527  elfzelfzccat  14534  ccatlid  14540  ccatass  14542  ccatrn  14543  ccatalpha  14547  swrdfv2  14615  ccatswrd  14622  swrdccat2  14623  pfxfv  14636  pfxeq  14650  ccatpfx  14655  swrdswrd  14659  swrdpfx  14661  pfxpfx  14662  cats1un  14675  swrdccatfn  14678  swrdccatin1  14679  pfxccatin12lem4  14680  pfxccatin12lem1  14682  swrdccatin2  14683  pfxccatin12lem2c  14684  pfxccatin12lem2  14685  swrdccat3blem  14693  swrdccatin1d  14697  swrdccatin2d  14698  pfxccatin12d  14699  revccat  14720  revrev  14721  repswpfx  14739  repswccat  14740  cshwidxmod  14757  2cshw  14767  cshwcshid  14782  cshwcsh2id  14783  cshimadifsn  14784  cshimadifsn0  14785  revco  14789  ccatco  14790  cshco  14791  swrdco  14792  ofccat  14920  shftfn  15024  shftval  15025  limsupgle  15425  ello12  15464  elo12  15475  isercolllem3  15617  sumeq1  15639  fsumsplit  15691  sumsplit  15718  fsum2dlem  15720  fsumcom2  15724  fsumparts  15756  explecnv  15815  pwdif  15818  fprodser  15897  fprodsplit  15914  fprod2dlem  15928  fprodcom2  15932  eftlub  16057  divalgmod  16354  bitsval  16370  bitsp1e  16378  bitsp1o  16379  sadfval  16398  sadcp1  16401  sadval  16402  sadcadd  16404  sadadd2  16406  saddisjlem  16410  sadadd  16413  sadass  16417  smufval  16423  smuval  16427  smuval2  16428  smupvallem  16429  smu01lem  16431  smueqlem  16436  smumul  16439  bezoutlem2  16487  bezoutlem4  16489  algfx  16522  eucalgcvga  16528  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  17046  elrest  17380  prdsbasmpt  17423  prdsleval  17430  prdsbasmpt2  17435  pwselbasb  17441  imasaddfnlem  17481  imasvscafn  17490  divsfval  17500  ismre  17541  mreunirn  17552  mrisval  17581  ismri  17582  isacs  17602  catidd  17631  iscatd2  17632  ismon  17687  isepi  17694  sectffval  17704  sectfval  17705  dfiso2  17726  cicsym  17758  issubc  17792  catsubcat  17796  isfunc  17821  funcres  17853  funcpropd  17860  ffthiso  17889  isnat  17908  isnat2  17909  fuciso  17938  initoval  17953  termoval  17954  isinito  17956  istermo  17957  iszeroo  17958  isinitoi  17959  istermoi  17960  initoid  17961  termoid  17962  iszeroi  17969  2initoinv  17970  initoeu1  17971  initoeu2  17976  2termoinv  17977  termoeu1  17978  arwhoma  18005  elsetchom  18041  setcmon  18047  setcepi  18048  setciso  18051  catciso  18071  elestrchom  18089  estrcbasbas  18092  funcestrcsetclem7  18108  funcestrcsetclem8  18109  funcestrcsetclem9  18110  fthestrcsetc  18112  fullestrcsetc  18113  equivestrcsetc  18114  setc1strwun  18115  funcsetcestrclem7  18123  funcsetcestrclem8  18124  funcsetcestrclem9  18125  fthsetcestrc  18127  fullsetcestrc  18128  hofcl  18222  hofpropd  18230  yonedalem4c  18240  yonedainv  18244  yonffthlem  18245  lubeldm  18316  glbeldm  18329  joindef  18339  meetdef  18353  poslubdg  18377  acsficl2d  18515  acsmapd  18517  psref  18537  psss  18543  dirge  18566  mgmpropd  18582  issstrmgm  18584  grpidval  18592  grpidpropd  18593  grpidd  18602  ismgmhm  18627  issubmgm  18633  issgrpd  18661  sgrppropd  18662  ismndd  18687  mndpropd  18690  imasmnd2  18702  imasmnd  18703  xpsmnd0  18706  ismhm  18713  issubm  18726  gsumsgrpccat  18763  elefmndbas2  18797  smndex1mndlem  18832  imasgrp2  18981  imasgrp  18982  issubg  19051  subginv  19058  isnsg  19080  quselbas  19108  isghm  19139  resghm2b  19157  conjnmzb  19176  conjnsg  19177  ghmpropd  19179  isga  19205  elcntz  19236  elcntzsn  19239  cntzrcl  19241  resscntz  19247  symgextf1  19339  gsmsymgreqlem2  19349  f1otrspeq  19365  pmtrfrn  19376  pmtrdifellem3  19396  pmtrdifellem4  19397  psgnunilem1  19411  psgnunilem5  19412  psgnunilem2  19413  psgnunilem3  19414  psgneldm2  19422  psgnfitr  19435  psgnsn  19438  gexdvds  19502  gex1  19509  isslw  19526  sylow3lem2  19546  lsmelvalx  19558  pj1ghm  19621  efgtlen  19644  efgsfo  19657  efgredlemc  19663  frgp0  19678  frgpmhm  19683  qusabl  19783  frgpnabllem1  19791  imasabl  19794  cycsubmcmn  19807  0cyg  19811  cycsubgcyg  19819  gsumval3  19825  gsumcllem  19826  gsumzaddlem  19839  gsumzsplit  19845  gsummptfzcl  19887  eldprd  19924  dprdcntz2  19958  dprd2d2  19964  dmdprdsplit2lem  19965  dmdprdsplit2  19966  dprdsplit  19968  ablfac2  20009  isrngd  20076  rngpropd  20077  imasrng  20080  qusrng  20083  ringurd  20088  isringd  20188  imasring  20227  xpsring1d  20230  dvdsrval  20261  isunit  20273  dvdsrpropd  20316  isirred  20319  isrnghm  20341  isrngim  20345  c0ghm  20361  c0snghm  20364  isrhm  20378  isrim0OLD  20381  isrim0  20383  islring  20438  issubrng  20445  opprsubrng  20457  issubrg  20471  opprsubrg  20493  resrhm2b  20502  rhmpropd  20509  rnghmresel  20514  elrngchom  20518  rnghmsubcsetclem1  20525  rnghmsubcsetclem2  20526  rngcid  20529  rngcsect  20530  rngciso  20532  funcrngcsetcALT  20535  zrinitorngc  20536  zrtermorngc  20537  rhmresel  20543  elringchom  20547  rhmsubcsetclem1  20554  rhmsubcsetclem2  20555  ringcid  20558  rhmsscrnghm  20559  rhmsubcrngclem1  20560  rhmsubcrngclem2  20561  ringcsect  20564  ringciso  20566  ringcbasbas  20567  zrtermoringc  20569  srhmsubc  20574  rhmsubclem3  20581  rhmsubclem4  20582  drngunit  20590  isdrngd  20618  isdrngdOLD  20620  issdrg  20637  sdrgunit  20645  isabv  20660  issrngd  20702  islmod  20708  lmodprop2d  20768  islss  20779  islssd  20780  lssats2  20845  lspsnel  20848  islmhm  20873  lmhmf1o  20892  lmhmima  20893  lmhmpreima  20894  reslmhm  20898  pwssplit3  20907  lmhmpropd  20919  islbs  20922  lspprel  20940  lspfixed  20977  lbsacsbs  21005  lbsextlem1  21007  lbsextlem2  21008  lbsextlem3  21009  lbsextlem4  21010  ixpsnbasval  21062  isridlrng  21076  rnglidlmmgm  21101  isridl  21107  quscrng  21136  rngqiprngimfolem  21141  rngqiprngimf1lem  21145  rngqiprngimfo  21152  islpidl  21176  lidldvgen  21185  irinitoringc  21362  pzriprnglem13  21376  pzriprnglem14  21377  zrhrhmb  21393  znf1o  21442  frgpcyg  21464  psgnevpmb  21476  isphld  21543  phlssphl  21548  elocv  21557  iscss  21572  isobs  21611  obs2ss  21620  dsmmfi  21629  dsmmelbas  21630  dsmmlss  21635  frlmelbas  21647  frlmlbs  21688  frlmup1  21689  ellspd  21693  islinds  21700  islindf2  21705  f1lindf  21713  islindf4  21729  assamulgscmlem2  21790  psrgrp  21855  mplsubglem  21896  mpllsslem  21897  mplmonmul  21929  subrgascl  21965  subrgasclcl  21966  mpfind  22008  ismhp  22020  mhplss  22034  gsumply1subr  22103  lply1binomsc  22181  matbas2d  22276  matecl  22278  matvscl  22284  mat1  22300  mat0dim0  22320  mat0dimid  22321  mat0dimscm  22322  mat1dimelbas  22324  dmatel  22346  scmatel  22358  scmateALT  22365  scmataddcl  22369  scmatsubcl  22370  smatvscl  22377  scmatghm  22386  mat1scmat  22392  mdetunilem7  22471  mdetunilem9  22473  smadiadetr  22528  cramerimplem2  22537  cramer0  22543  pmatcoe1fsupp  22554  cpmatpmat  22563  cpmatel  22564  cpmatacl  22569  cpmatinvcl  22570  mat2pmatghm  22583  mat2pmatmul  22584  decpmatmullem  22624  pmatcollpwlem  22633  pmatcollpw3fi1lem1  22639  pmatcollpwscmatlem1  22642  monmat2matmon  22677  chfacfscmul0  22711  chfacfscmulgsum  22713  chfacfpmmulgsum  22717  cayhamlem1  22719  cpmadugsumlemB  22727  cpmadugsumlemC  22728  cpmadugsumlemF  22729  cayhamlem2  22737  istopon  22765  eltg  22811  eltg2  22812  eltop  22828  eltop2  22829  eltop3  22830  pptbas  22862  iscld  22882  neiss2  22956  isnei  22958  neiptopnei  22987  neiptopreu  22988  lpfval  22993  lpval  22994  islp  22995  maxlp  23002  islpi  23004  neitr  23035  restlp  23038  ordtbas2  23046  ordtrest2  23059  lmfval  23087  cnfval  23088  iscn  23090  iscnp  23092  tgcn  23107  tgcnp  23108  lmbrf  23115  cnpresti  23143  ist1  23176  ist1-2  23202  cnt1  23205  haust1  23207  cmpfi  23263  cmpfii  23264  1stcfb  23300  2ndc1stc  23306  1stcrest  23308  2ndcdisj  23311  1stcelcls  23316  nllyi  23330  subislly  23336  islocfin  23372  lfinpfin  23379  locfindis  23385  locfincf  23386  comppfsc  23387  kgenval  23390  elkgen  23391  kgencn2  23412  txbas  23422  eltx  23423  ptval  23425  ptpjpre1  23426  ptopn2  23439  ptpjopn  23467  ptclsg  23470  xkoccn  23474  txdis  23487  txdis1cn  23490  ptrescn  23494  hausdiag  23500  hauseqlcld  23501  txhaus  23502  xkohaus  23508  elqtop  23552  qtopeu  23571  kqcldsat  23588  hmeofval  23613  ptuncnv  23662  ptunhmeo  23663  elmptrab  23682  fbdmn0  23689  elfg  23726  elfilss  23731  filunirn  23737  fixufil  23777  elfm  23802  rnelfmlem  23807  rnelfm  23808  fmfnfmlem4  23812  elflim2  23819  flimtopon  23825  elflim  23826  hausflim  23836  flimcls  23840  flfnei  23846  isflf  23848  hausflf  23852  cnpflf  23856  cnflf  23857  txflf  23861  isfcls  23864  fclstopon  23867  isfcls2  23868  fclssscls  23873  fclsnei  23874  fclsfnflim  23882  flimfnfcls  23883  isfcf  23889  fcfelbas  23891  cnpfcf  23896  cnfcf  23897  flfcntr  23898  alexsublem  23899  alexsubALTlem3  23904  cnextfun  23919  cnextfvval  23920  cnextf  23921  cnextcn  23922  tmdgsum2  23951  tgpconncomp  23968  ghmcnp  23970  qustgplem  23976  eltsms  23988  haustsms  23991  tsmsgsum  23994  tsmssubm  23998  tsmssplit  24007  isust  24059  ustbas  24083  elutop  24089  ustuqtoplem  24095  ustuqtop4  24100  ustuqtop  24102  utopsnneiplem  24103  utopsnneip  24104  utopsnnei  24105  isusp  24117  isucn  24134  ucncn  24141  iscfilu  24144  neipcfilu  24152  iscusp  24155  cnextucn  24159  ispsmet  24161  ismet  24180  isxmet  24181  elblps  24244  elbl  24245  elmopn  24299  prdsbl  24351  neibl  24361  met1stc  24381  metrest  24384  prdsxmslem2  24389  txmetcnp  24407  txmetcn  24408  metustsym  24415  cfilucfil2  24421  elbl4  24423  metuel  24424  psmetutop  24427  restmetu  24430  metucn  24431  tngngp  24522  isnmhm  24614  zcld  24680  metnrmlem1a  24725  elcncf  24760  cncfcnvcn  24797  cnheibor  24832  lebnumlem1  24838  ishtpy  24849  isphtpy  24858  om1elbas  24910  elpi1  24923  pi1xfr  24933  pi1coghm  24939  tcphcph  25116  lmmbrf  25141  iscfil  25144  iscau  25155  iscauf  25159  caucfil  25162  iscmet  25163  cmetcaulem  25167  iscmet3lem1  25170  iscmet3lem2  25171  iscmet3  25172  bcthlem1  25203  cmsss  25230  cmetcusp1  25232  cmetcusp  25233  cmscsscms  25252  rrxcph  25271  minveclem3b  25307  ovolfioo  25347  ovolficc  25348  ovolctb  25370  ovoliunnul  25387  ovolshftlem1  25389  sca2rab  25392  ovolscalem1  25393  ovolicc2lem1  25397  ovolicc2lem2  25398  ovolicc2lem4  25400  ovolicc2lem5  25401  iundisj  25428  iunmbl2  25437  uniioombllem3  25465  vitalilem2  25489  vitalilem3  25490  mbfss  25526  i1faddlem  25573  i1fmullem  25574  mbfi1fseqlem2  25597  mbfi1fseqlem4  25599  mbfi1fseq  25602  itg2splitlem  25629  itg2split  25630  itg2monolem1  25631  itg2gt0  25641  isibl  25646  iblss2  25686  itgss3  25695  itgsplit  25716  ellimc  25753  limcmo  25762  cnlimc  25768  limciun  25774  limcun  25775  eldv  25778  dvbsss  25782  dvreslem  25789  elcpn  25815  dvaddf  25824  dvmulf  25825  dvcof  25831  rolle  25873  dvlip2  25879  dvivthlem1  25892  lhop1  25898  lhop2  25899  ftc1cn  25929  fta1glem2  26054  plyco0  26077  elply  26080  ply1termlem  26088  eltayl  26245  tayl0  26247  taylplem1  26248  taylplem2  26249  dvtaylp  26256  taylthlem1  26259  taylthlem2  26260  taylthlem2OLD  26261  abelth  26329  cxpcn3  26634  rlimcnp  26848  fsumharmonic  26895  dchrelbas  27120  pntrsumbnd2  27451  ostth2lem2  27518  nolesgn2ores  27556  nogesgn1ores  27558  nosupprefixmo  27584  noinfprefixmo  27585  nosupcbv  27586  nosupdm  27588  nosupfv  27590  nosupres  27591  nosupbnd1lem1  27592  nosupbnd1lem3  27594  nosupbnd1lem5  27596  nosupbnd2lem1  27599  noinfcbv  27601  noinfdm  27603  noinffv  27605  noinfres  27606  noinfbnd1lem1  27607  noinfbnd1lem3  27609  noinfbnd1lem5  27611  noinfbnd2lem1  27614  elmade  27745  elold  27747  ssltleft  27748  ssltright  27749  oldlim  27764  madebday  27777  newbday  27779  sltlpss  27784  cofcutr  27795  cofcutrtime  27798  lrrecval  27807  lrrecval2  27808  addsval  27830  precsexlem9  28064  precsexlem11  28066  sltonold  28104  noseqrdgfn  28130  istrkgb  28210  istrkgcb  28211  istrkge  28212  istrkgl  28213  istrkgld  28214  axtgsegcon  28219  axtg5seg  28220  axtgbtwnid  28221  axtgpasch  28222  axtgupdim2  28226  axtgeucl  28227  tgdim01  28262  iscgrg  28267  isismt  28289  tglnunirn  28303  tglngval  28306  tgellng  28308  legval  28339  legov  28340  legov2  28341  ishlg  28357  mirreu3  28409  mirval  28410  mirfv  28411  mircgr  28412  mirbtwn  28413  ismir  28414  mireq  28420  symquadlem  28444  israg  28452  perpln1  28465  perpln2  28466  isperp  28467  islnopp  28494  outpasch  28510  ishpg  28514  iscgra  28564  dfcgra2  28585  isinag  28593  isleag  28602  iseqlg  28622  f1otrgitv  28625  f1otrg  28626  f1otrge  28627  ttgval  28630  ttgvalOLD  28631  ttgelitv  28644  elee  28656  brbtwn  28661  brcgr  28662  axlowdimlem16  28719  ebtwntg  28744  elntg2  28747  upgrex  28856  edgupgr  28898  upgredg  28901  edglnl  28907  numedglnl  28908  uhgr2edg  28969  umgr2edg1  28972  usgredg2vlem1  28986  usgredg2vlem2  28987  ushgredgedg  28990  ushgredgedgloop  28992  uhgrspansubgrlem  29051  fusgrfisstep  29090  nbgrval  29097  nbgrel  29101  nbupgrel  29106  nbgr2vtx1edg  29111  nbuhgr2vtx1edgblem  29112  nbuhgr2vtx1edgb  29113  nbusgreledg  29114  usgrnbcnvfv  29126  uvtxval  29148  uvtxel  29149  uvtx01vtx  29158  uvtxusgrel  29164  nbcplgr  29195  cplgr3v  29196  cusgrexi  29204  structtocusgr  29207  vtxdgfval  29229  vtxdg0v  29235  vtxdeqd  29239  vtxdun  29243  1loopgrnb0  29264  1loopgrvd0  29266  1hevtxdg0  29267  1hevtxdg1  29268  1egrvtxdg1  29271  umgr2v2evtxel  29284  umgr2v2enb1  29288  umgr2v2evd2  29289  vtxdginducedm1lem4  29304  vtxdginducedm1  29305  finsumvtxdg2sstep  29311  ewlksfval  29363  isewlk  29364  wksfval  29371  iswlk  29372  uspgr2wlkeq  29408  wlkres  29432  usgr2pthlem  29525  clwlkcompim  29542  uspgrn2crct  29567  wwlks  29594  iswwlksn  29597  wwlknvtx  29604  wlkiswwlks2  29634  wwlksm1edg  29640  wwlksnred  29651  wwlksnext  29652  wwlksnredwwlkn  29654  wwlksnredwwlkn0  29655  wwlksnwwlksnon  29674  wspn0  29683  usgr2wspthons3  29723  rusgrnumwwlkb0  29730  clwwlk  29741  clwwlkccatlem  29747  clwlkclwwlklem2a4  29755  clwlkclwwlk  29760  clwwisshclwwslem  29772  clwwlkinwwlk  29798  clwwlkel  29804  clwwlkf  29805  clwwlkext2edg  29814  wwlksext2clwwlk  29815  wwlksubclwwlk  29816  clwwnisshclwwsn  29817  eleclclwwlknlem2  29819  erclwwlknsym  29828  erclwwlkntr  29829  umgrhashecclwwlk  29836  clwwlkvbij  29871  eupth2lem3lem3  29988  eupth2lem3lem4  29989  eupth2lem3lem6  29991  eupth2lemb  29995  eucrct2eupth  30003  fusgreg2wsplem  30091  2clwwlklem  30101  2clwwlk2clwwlklem  30104  2clwwlkel  30107  2clwwlk2clwwlk  30108  extwwlkfabel  30111  clwwlknonclwlknonf1o  30120  dlwwlknondlwlknonf1olem1  30122  numclwwlk2lem1  30134  numclwlk2lem2f  30135  numclwlk2lem2f1o  30137  ex-res  30199  isssp  30482  sspn  30494  islno  30511  isblo  30540  nmlno0  30553  ishmo  30569  dipdir  30600  dipass  30603  ubthlem1  30628  ubthlem2  30629  htthlem  30675  htth  30676  ocel  31039  ocnel  31056  shsel  31072  shsel2  31080  shmodsi  31147  pjhtheu  31152  pjeq  31157  axpjpj  31178  pjoc2  31197  elspani  31301  h1de2ctlem  31313  elspansn  31324  elspansn2  31325  elnlfn  31686  eleigvec  31715  riesz3i  31820  cbviunf  32292  iuneq12daf  32293  iunrdx  32300  iunrnmptss  32302  cbvdisjf  32307  disjorf  32315  disjabrex  32318  disjabrexf  32319  iundisjf  32325  disjrdx  32327  elimampt  32367  2ndresdju  32379  abfmpunirn  32382  abfmpeld  32384  abfmpel  32385  fmptcof2  32387  acunirnmpt2  32390  acunirnmpt2f  32391  aciunf1lem  32392  funcnvmpt  32397  suppss3  32454  fpwrelmap  32463  xrofsup  32485  iundisjfi  32512  eliccioo  32600  s3f1  32616  ccatf1  32618  swrdrn3  32622  ismnt  32656  mgcoval  32659  gsummpt2co  32704  gsumpart  32711  gsumhashmul  32712  xrge0tsmsbi  32714  cycpmco2  32796  cyc3co2  32803  inftmrel  32830  isinftm  32831  isslmd  32851  urpropd  32882  isdrng4  32898  resv1r  32959  eqg0el  32980  ellspds  32987  lbslsp  32999  rhmimaidl  33056  isprmidl  33062  qsidomlem1  33077  qsidomlem2  33078  ismxidl  33084  crngmxidl  33091  drng0mxidl  33098  opprqus0g  33110  qsfld  33118  isrprm  33140  dimpropd  33211  lbslsat  33219  extdg1id  33260  elirng  33269  ply1annidllem  33281  smatrcl  33306  smatcl  33312  ist0cld  33343  txomap  33344  locfinreflem  33350  zarclsiin  33381  zart0  33389  rhmpreimacnlem  33394  metidval  33400  cnre2csqima  33421  ordtrest2NEW  33433  fmcncfil  33441  fsumcvg4  33460  ofcfval  33626  measvuni  33742  meascnbl  33747  faeval  33774  ismbfm  33779  elunirnmbfm  33780  imambfm  33791  elcarsg  33834  itgeq12dv  33855  issibf  33862  eulerpartlems  33889  eulerpartlemgc  33891  eulerpartlemgvv  33905  eulerpartlemgu  33906  eulerpart  33911  rrvmbfm  33971  elorvc  33988  elorrvc  33992  dstfrvunirn  34003  ballotlemfc0  34021  ballotlemfcc  34022  ballotlemsima  34044  ballotlemrv  34048  fzssfzo  34080  signstfvn  34110  signstfvneq0  34113  signstres  34116  repr0  34152  reprinrn  34159  reprdifc  34168  hgt750lemg  34195  hgt750lemb  34197  istrkg2d  34207  axtgupdim2ALTV  34209  afsval  34212  brafs  34213  bnj945  34313  bnj1400  34375  bnj18eq1  34467  bnj916  34473  bnj1014  34501  bnj1015  34502  bnj1110  34522  bnj1417  34581  revpfxsfxrev  34634  cplgredgex  34639  pfxwlk  34642  revwlk  34643  subfacp1lem2b  34700  subfacp1lem4  34702  subfacp1lem5  34703  subfacp1lem6  34704  ptpconn  34752  cvmscbv  34777  iscvm  34778  cvmsi  34784  cvmsval  34785  cvmliftmolem1  34800  cvmlift2lem12  34833  cvmlift2lem13  34834  cvmlift3lem7  34844  snmlval  34850  satfv1  34882  satfvsucsuc  34884  satfrnmapom  34889  satf0op  34896  satf0n0  34897  sat1el2xp  34898  fmlafvel  34904  isfmlasuc  34907  fmlaomn0  34909  gonan0  34911  goaln0  34912  gonar  34914  goalr  34916  satffunlem1lem2  34922  satffunlem2lem2  34925  satfv0fvfmla0  34932  satef  34935  satefvfmla0  34937  sategoelfvb  34938  satfv1fvfmla1  34942  mrsubfval  35027  mrsubvrs  35041  mclsrcl  35080  mclsval  35082  mppsval  35091  mclsppslem  35102  opelco3  35279  wsuclem  35330  funtransport  35536  fvtransport  35537  brcolinear  35564  colineardim1  35566  funray  35645  fvray  35646  funline  35647  fvline  35649  lineelsb2  35653  fwddifval  35667  fwddifnval  35668  rankelg  35673  rankeq1o  35676  elhf2  35680  0hf  35682  neibastop2lem  35753  neibastop3  35755  eltail  35767  bj-projeq  36380  bj-projval  36384  bj-restsn  36470  opelopabbv  36531  brabd0  36535  bj-eldiag  36564  bj-eldiag2  36565  mptsnunlem  36726  dissneqlem  36728  iooelexlt  36750  relowlssretop  36751  rdgellim  36764  exrecfnlem  36767  finxpeq1  36774  finxpreclem6  36784  pibp21  36803  curf  36977  uncf  36978  curunc  36981  unccur  36982  fin2so  36986  lindsadd  36992  lindsdom  36993  lindsenlbs  36994  matunitlindflem1  36995  matunitlindflem2  36996  matunitlindf  36997  ptrest  36998  ptrecube  36999  poimirlem2  37001  poimirlem8  37007  poimirlem17  37016  poimirlem18  37017  poimirlem20  37019  poimirlem21  37020  poimirlem22  37021  poimirlem24  37023  poimirlem26  37025  poimirlem29  37028  heicant  37034  mblfinlem1  37036  mblfinlem2  37037  volsupnfl  37044  itg2addnclem  37050  itg2gt0cn  37054  indexdom  37113  incsequz  37127  istotbnd  37148  istotbnd3  37150  0totbnd  37152  sstotbnd  37154  sstotbnd3  37155  isbnd  37159  prdstotbnd  37173  cntotbnd  37175  isismty  37180  heibor1lem  37188  heiborlem2  37191  heiborlem3  37192  heibor  37200  isass  37225  exidcl  37255  exidreslem  37256  elghomlem2OLD  37265  rngoidmlem  37315  rngo1cl  37318  divrngcl  37336  isdrngo2  37337  isrngohom  37344  isrngoiso  37357  isriscg  37363  iscom2  37374  iscringd  37377  isidl  37393  ispridl  37413  ismaxidl  37419  ac6s6  37551  dmecd  37684  releldmqs  38039  releldmqscoss  38041  erimeq2  38059  eldisjlem19  38191  membpartlem19  38192  prter3  38263  islshp  38360  islsat  38372  lcvfbr  38401  islfl  38441  ellkr  38470  islshpkrN  38501  ldual1dim  38547  isopos  38561  cmtfvalN  38591  cvrfval  38649  isat  38667  islln  38888  islpln  38912  islvol  38955  isline  39121  ispointN  39124  ispsubsp  39127  elpmap  39140  elpmapat  39146  elpadd  39181  paddclN  39224  elpclN  39274  elpcliN  39275  pclfinN  39282  pclcmpatN  39283  ispsubclN  39319  iswatN  39376  islhp  39378  islaut  39465  ispautN  39481  isldil  39492  isltrn  39501  isdilN  39536  istrnN  39539  istendo  40142  dvhb1dimN  40368  erng1lem  40369  erngdvlem4-rN  40381  diaelval  40415  diaeldm  40418  dia1dimid  40445  cdlemm10N  40500  dibopelvalN  40525  dibopelval2  40527  dibelval3  40529  dibelval1st  40531  dibelval2nd  40534  dibeldmN  40540  dibvalrel  40545  dibglbN  40548  dicffval  40556  dicfval  40557  dicopelval  40559  dicelvalN  40560  dicelval3  40562  dicvalrelN  40567  dicelval1sta  40569  diclspsn  40576  dihopelvalbN  40620  dihopelvalcqat  40628  dihopelvalcpre  40630  dihvalrel  40661  dih1  40668  dihmeetlem4preN  40688  dihmeetlem13N  40701  dih1dimatlem  40711  dochnel2  40774  dihjatcclem4  40803  dvh2dim  40827  dvh3dim  40828  dvh4dimN  40829  dochfln0  40859  lpolsetN  40864  islpolN  40865  lcfrvalsnN  40923  lcfrlem21  40945  lcfrlem27  40951  lcfrlem37  40961  lcfr  40967  lcdlss  41001  mapdcv  41042  hdmap1fval  41178  hdmapffval  41208  hdmapfval  41209  hdmapval  41210  hgmapffval  41267  hgmapfval  41268  hdmapellkr  41296  hlhilhillem  41346  fzsplitnd  41362  isprimroot  41472  primrootsunit1  41475  primrootscoprmpow  41477  primrootscoprbij  41480  aks6d1c1p2  41484  aks6d1c1p3  41485  aks6d1c1p4  41486  aks6d1c1p5  41487  aks6d1c1p6  41489  aks6d1c1  41491  evl1gprodd  41492  sticksstones11  41514  sticksstones12a  41515  fzosumm1  41610  frlmfielbas  41616  frlmsnic  41648  isnacs  42001  mrefg2  42004  elmzpcl  42023  mzpcompact2  42049  eldiophb  42054  elpell1qr  42144  elpell14qr  42146  elpell1234qr  42148  pw2f1ocnv  42335  pw2f1o2val2  42338  aomclem4  42358  aomclem6  42360  islssfg2  42372  imasgim  42401  lnr2i  42417  elmnc  42437  rngunsnply  42474  onexomgt  42547  onexlimgt  42549  onexoegt  42550  oaordnr  42603  omnord1  42612  oenord1  42623  cantnfresb  42631  tfsconcatun  42644  tfsconcat0i  42652  ofoaf  42662  naddcnff  42669  naddcnffo  42671  naddcnfcom  42673  naddcnfid1  42674  naddcnfid2  42675  naddcnfass  42676  naddwordnexlem4  42709  fiinfi  42881  sqrtcvallem1  42939  elintima  42961  eliunov2  42987  ov2ssiunov2  43008  brtrclfv2  43035  rfovcnvf1od  43312  rfovcnvfvd  43315  fsovrfovd  43317  fsovfvd  43318  fsovcnvlem  43321  ntrclsfv1  43363  ntrclselnel1  43365  ntrclsneine0lem  43372  ntrneifv1  43387  ntrneifv2  43388  ntrneiel  43389  gneispace2  43440  gneispacess2  43454  extoimad  43473  mnringelbased  43530  dvconstbi  43650  bccbc  43661  eliin2f  44349  rabbida2  44377  disjinfi  44444  unirnmap  44460  elmptima  44515  iuneqfzuzlem  44597  iooiinioc  44822  fsumiunss  44844  fsumsupp0  44847  lptre2pt  44909  icccncfext  45156  cncfiooicclem1  45162  dvnprodlem2  45216  stoweidlem27  45296  stoweidlem29  45298  stoweidlem31  45300  stoweidlem34  45303  stoweidlem48  45317  stoweidlem59  45328  dirkercncflem2  45373  dirkercncflem4  45375  fourierdlem2  45378  fourierdlem3  45379  fourierdlem25  45401  fourierdlem32  45408  fourierdlem33  45409  fourierdlem41  45417  fourierdlem48  45423  fourierdlem49  45424  fourierdlem62  45437  fourierdlem70  45445  fourierdlem80  45455  fourierdlem92  45467  fourierdlem93  45468  fourierdlem101  45476  etransclem37  45540  sge0val  45635  sge0f1o  45651  sge0iunmptlemre  45684  sge0iunmpt  45687  iundjiun  45729  caragenel  45764  ovncvrrp  45833  ovnsubaddlem1  45839  ovnsubadd  45841  hoidmvlelem2  45865  hoidmvlelem3  45866  hoidmvlelem4  45867  hoidmvle  45869  ovncvr2  45880  hspdifhsp  45885  hoiqssbl  45894  hspmbllem2  45896  hspmbl  45898  opnvonmbllem1  45901  isvonmbl  45907  ovnovollem1  45925  issmflem  45996  smflimlem3  46042  smflimlem4  46043  smflim  46046  smfmullem2  46061  smflimmpt  46079  smfsuplem1  46080  smflimsuplem1  46089  smflimsuplem3  46091  smflimsuplem4  46092  smflimsuplem7  46095  smflimsup  46097  tworepnotupword  46153  fcores  46330  fcoresf1  46332  afvelrnb  46424  afvelrnb0  46425  afv2co2  46518  el1fzopredsuc  46586  iccpart  46637  iccpartgtprec  46641  iccpartiltu  46643  iccpartigtl  46644  iccpartltu  46646  iccpartgtl  46647  iccpartgt  46648  iccpartleu  46649  iccpartgel  46650  iccelpart  46654  iccpartiun  46655  icceuelpart  46657  fargshiftfv  46660  fargshiftfo  46663  sprel  46705  prprelb  46737  prprelprb  46738  fpprel  46949  sbgoldbo  47008  wtgoldbnnsum4prm  47023  bgoldbnnsum3prm  47025  bgoldbtbndlem3  47028  bgoldbtbnd  47030  upwlksfval  47066  isupwlk  47067  intop  47134  isclintop  47138  assintop  47140  isassintop  47141  assintopcllaw  47143  uzlidlring  47166  elrngchomALTV  47200  rngccatidALTV  47203  rngcsectALTV  47206  rngcisoALTV  47208  rhmsubcALTVlem3  47214  rhmsubcALTVlem4  47215  funcringcsetcALTV2lem7  47227  funcringcsetcALTV2lem9  47229  elringchomALTV  47234  ringccatidALTV  47237  ringcsectALTV  47240  ringcisoALTV  47242  ringcbasbasALTV  47243  funcringcsetclem7ALTV  47250  funcringcsetclem9ALTV  47252  srhmsubcALTV  47256  opeliun2xp  47265  cbvmpox2  47268  ply1sclrmsm  47320  dmatALTbasel  47339  lcoval  47349  lindslinindsimp1  47394  lindslinindsimp2  47400  lmod1  47429  elbigo  47493  elbigo2  47494  elbigolo1  47499  dig2nn0ld  47546  naryfvalel  47572  rrxlines  47675  rrxlinesc  47677  rrxlinec  47678  eenglngeehlnm  47681  elrrx2linest2  47687  rrxsphere  47690  itsclc0  47713  itsclc0b  47714  itsclinecirc0  47715  itsclinecirc0b  47716  itscnhlinecirc02p  47727  f1omo  47782  lubeldm2d  47846  glbeldm2d  47847  catprs  47886  isthinc  47896  isthincd2lem1  47902  thincmoALT  47905  thincmod  47906  isthincd  47912  prsthinc  47929  elsetrecslem  47999