Theorem eleq2d 2823

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eleq2d	⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Proof of Theorem eleq2d

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1d.1	. . . 4 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dfcleq 2730	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	sylib 218	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		anbi2 635	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1835	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 17	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		dfclel 2813	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		dfclel 2813	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

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

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

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

This theorem is referenced by:  eleq2  2826  eleq12d  2831  eleqtrd  2839  neleqtrd  2859  eqabrd  2878  raleqbidv  3312  rexeqbidv  3313  reueqbidv  3379  rabeqbidva  3406  elabd2  3613  sbcbid  3784  sbcbi2  3788  csbeq2d  3844  csbeq2dv  3845  cbvcsbw  3848  cbvcsb  3849  cbvcsbv  3850  csbie  3873  csbied  3874  csbie2g  3878  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  sbcel12  4352  sbcel1g  4357  sbcel2  4359  prel12g  4808  eliuni  4940  iuneqconst  4946  iuneq12df  4961  iuneq12d  4964  cbviun  4978  cbviin  4979  cbviung  4980  cbviing  4981  cbviunv  4982  cbviinv  4983  iinxsng  5031  iinxprg  5032  iunxsng  5033  iunxsngf  5035  cbvdisj  5063  cbvdisjv  5064  disjor  5068  disjiund  5077  mpteq12da  5169  mpteq12f  5171  mpteq12dva  5172  axpweq  5289  rabxfrd  5355  rbropapd  5511  opeliunxp  5692  opeliun2xp  5693  opeliunxp2  5788  iunxpf  5798  elimampt  6003  elrelimasn  6046  elimasni  6051  imadifssran  6110  xpdifid  6127  ressn  6244  funfni  6599  fnbr  6601  dffv3  6831  elfv2ex  6878  fvelrnb  6895  foelcdmi  6896  fvun1  6926  fvco2  6932  funcnvmpt  6944  elfvmptrab1w  6970  elfvmptrab1  6971  elfvmptrab  6972  elpreima  7005  dff3  7047  fmptco  7077  fnelfp  7124  fnelnfp  7126  tpres  7150  fnprb  7157  fntpb  7158  funfvima3  7185  eluniima  7199  dff13  7203  f1ounsn  7221  f1eqcocnv  7250  isoini  7287  riotaeqdv  7319  mpoeq123dva  7435  cbvmpox  7454  elimampo  7498  ovelrn  7537  elovmpod  7605  elovmpo  7606  elovmporab  7607  elovmporab1w  7608  elovmporab1  7609  elovmpt3rab1  7621  fiun  7890  f1iun  7891  zfrep6OLD  7902  fmpox  8014  el2mpocsbcl  8029  el2mpocl  8030  bropopvvv  8034  bropfvvvv  8036  xpord2indlem  8091  xpord3inddlem  8098  elsuppfng  8113  elsuppfn  8114  suppfnss  8133  opeliunxp2f  8154  mpoxopn0yelv  8157  mpoxopovel  8164  rntpos  8183  mpocurryd  8213  fpr2  8248  wfr2  8271  onoviun  8277  smoel  8294  smoiso  8296  smoel2  8297  smo11  8298  tfrlem9  8318  oalimcl  8489  oaass  8490  omordi  8495  omordlim  8506  omlimcl  8507  odi  8508  omeulem1  8511  omeulem2  8512  oen0  8516  oeordi  8517  oeordsuc  8524  oelimcl  8530  oeeulem  8531  oeeui  8532  nnmordi  8561  oaabs2  8579  omabs  8581  omsmolem  8587  ereldm  8691  iiner  8730  elmapg  8780  elpmg  8784  elixpsn  8879  ixpsnf1o  8880  boxriin  8882  omxpenlem  9010  pw2f1olem  9013  phplem2  9133  php3  9137  infn0  9206  elfi  9320  dffi3  9338  marypha2lem2  9343  ordiso2  9424  wemapsolem  9459  elharval  9470  inf3lemd  9542  inf3lem1  9543  inf3lem2  9544  inf3lem3  9545  cantnfs  9581  cantnfp1lem3  9595  cantnflem1b  9601  cantnflem1  9604  ttrclselem2  9641  trcl  9643  frr2  9678  r1sdom  9692  r1ordg  9696  r1pwss  9702  tz9.12lem3  9707  tz9.12  9708  r1elwf  9714  rankr1ai  9716  rankidb  9718  rankr1bg  9721  rankval2  9736  rankunb  9768  tcrank  9802  acni  9961  acni2  9962  acndom  9967  infpwfien  9978  alephnbtwn  9987  cardaleph  10005  cardinfima  10013  iunfictbso  10030  dfac3  10037  dfac5lem5  10043  dfac5  10045  dfac9  10053  dfac12r  10063  kmlem2  10068  kmlem12  10078  kmlem13  10079  kmlem14  10080  ackbij2lem3  10156  ackbij2  10158  cofsmo  10185  alephsing  10192  fin23lem30  10258  isf32lem9  10277  itunisuc  10335  axcc2lem  10352  axcc3  10354  domtriomlem  10358  axdc2lem  10364  axdc2  10365  axdc3lem2  10367  axdc3lem4  10369  axdc4lem  10371  ac6c4  10397  zorn2lem1  10412  ttukeylem6  10430  pwcfsdom  10500  axregndlem2  10520  axinfndlem1  10522  axacndlem4  10527  axacnd  10529  pwfseqlem1  10575  inar1  10692  inatsk  10695  gruurn  10715  grur1  10737  eltskm  10760  genpelv  10917  eluz1  12786  elixx1  13301  elixx3g  13305  elioo2  13333  elfz1  13460  elfz2  13462  elfzp1  13522  fzpr  13527  fzsuc2  13530  fzrev3  13538  elfzp12  13551  fzm1  13555  elfzo  13609  fz0add1fz1  13684  elfzo0l  13705  elfzom1b  13715  fzosplitsni  13728  elfzr  13730  elfzlmr  13731  zmodidfzo  13853  seqp1  13972  seqf1o  13999  bcval  14260  bcpasc  14277  hashf1lem1  14411  fundmge2nop0  14458  wrdmap  14502  elovmpowrd  14514  ccatfval  14529  elfzelfzccat  14536  ccatlid  14543  ccatass  14545  ccatrn  14546  ccatalpha  14550  swrdfv2  14618  ccatswrd  14625  swrdccat2  14626  pfxfv  14639  pfxeq  14652  ccatpfx  14657  swrdswrd  14661  swrdpfx  14663  pfxpfx  14664  cats1un  14677  swrdccatfn  14680  swrdccatin1  14681  pfxccatin12lem4  14682  pfxccatin12lem1  14684  swrdccatin2  14685  pfxccatin12lem2c  14686  pfxccatin12lem2  14687  swrdccat3blem  14695  swrdccatin1d  14699  swrdccatin2d  14700  pfxccatin12d  14701  revccat  14722  revrev  14723  repswpfx  14741  repswccat  14742  cshwidxmod  14759  2cshw  14769  cshwcshid  14783  cshwcsh2id  14784  cshimadifsn  14785  cshimadifsn0  14786  revco  14790  ccatco  14791  cshco  14792  swrdco  14793  ofccat  14925  shftfn  15029  shftval  15030  limsupgle  15433  ello12  15472  elo12  15483  isercolllem3  15623  sumeq1  15645  fsumsplit  15697  sumsplit  15724  fsum2dlem  15726  fsumcom2  15730  fsumparts  15763  explecnv  15824  pwdif  15827  fprodser  15908  fprodsplit  15925  fprod2dlem  15939  fprodcom2  15943  eftlub  16070  divalgmod  16369  bitsval  16387  bitsp1e  16395  bitsp1o  16396  sadfval  16415  sadcp1  16418  sadval  16419  sadcadd  16421  sadadd2  16423  saddisjlem  16427  sadadd  16430  sadass  16434  smufval  16440  smuval  16444  smuval2  16445  smupvallem  16446  smu01lem  16448  smueqlem  16453  smumul  16456  bezoutlem2  16503  bezoutlem4  16505  algfx  16543  eucalgcvga  16549  reumodprminv  16769  nnnn0modprm0  16771  unbenlem  16873  prmreclem5  16885  vdwapval  16938  vdwapun  16939  vdwnnlem1  16960  vdwnn  16963  ramval  16973  0ram  16985  ramub1lem2  16992  prmgaplem7  17022  prmlem0  17070  elrest  17384  prdsbasmpt  17427  prdsleval  17434  prdsbasmpt2  17439  pwselbasb  17445  imasaddfnlem  17486  imasvscafn  17495  divsfval  17505  ismre  17546  mreunirn  17557  mrisval  17590  ismri  17591  isacs  17611  catidd  17640  iscatd2  17641  ismon  17694  isepi  17701  sectffval  17711  sectfval  17712  dfiso2  17733  cicsym  17765  issubc  17796  catsubcat  17800  isfunc  17825  funcres  17857  funcpropd  17863  ffthiso  17892  isnat  17911  isnat2  17912  fuciso  17939  initoval  17954  termoval  17955  isinito  17957  istermo  17958  iszeroo  17959  isinitoi  17960  istermoi  17961  initoid  17962  termoid  17963  iszeroi  17970  2initoinv  17971  initoeu1  17972  initoeu2  17977  2termoinv  17978  termoeu1  17979  arwhoma  18006  elsetchom  18042  setcmon  18048  setcepi  18049  setciso  18052  catciso  18072  elestrchom  18088  estrcbasbas  18091  funcestrcsetclem7  18106  funcestrcsetclem8  18107  funcestrcsetclem9  18108  fthestrcsetc  18110  fullestrcsetc  18111  equivestrcsetc  18112  setc1strwun  18113  funcsetcestrclem7  18121  funcsetcestrclem8  18122  funcsetcestrclem9  18123  fthsetcestrc  18125  fullsetcestrc  18126  hofcl  18219  hofpropd  18227  yonedalem4c  18237  yonedainv  18241  yonffthlem  18242  lubeldm  18311  glbeldm  18324  joindef  18334  meetdef  18348  poslubdg  18372  acsficl2d  18512  acsmapd  18514  psref  18534  psss  18540  dirge  18563  chnccats1  18585  chnccat  18586  chnrev  18587  mgmpropd  18613  issstrmgm  18615  grpidval  18623  grpidpropd  18624  grpidd  18633  ismgmhm  18658  issubmgm  18664  issgrpd  18692  sgrppropd  18693  ismndd  18718  mndpropd  18721  imasmnd2  18736  imasmnd  18737  xpsmnd0  18740  ismhm  18747  issubm  18765  gsumsgrpccat  18802  elefmndbas2  18836  smndex1mndlem  18874  imasgrp2  19025  imasgrp  19026  issubg  19096  subginv  19103  isnsg  19124  eqg0el  19152  quselbas  19153  isghm  19184  isghmOLD  19185  resghm2b  19203  conjnmzb  19222  conjnsg  19223  ghmpropd  19225  isga  19260  elcntz  19291  elcntzsn  19294  cntzrcl  19296  resscntz  19302  symgextf1  19390  gsmsymgreqlem2  19400  f1otrspeq  19416  pmtrfrn  19427  pmtrdifellem3  19447  pmtrdifellem4  19448  psgnunilem1  19462  psgnunilem5  19463  psgnunilem2  19464  psgnunilem3  19465  psgneldm2  19473  psgnfitr  19486  psgnsn  19489  gexdvds  19553  gex1  19560  isslw  19577  sylow3lem2  19597  lsmelvalx  19609  pj1ghm  19672  efgtlen  19695  efgsfo  19708  efgredlemc  19714  frgp0  19729  frgpmhm  19734  qusabl  19834  frgpnabllem1  19842  imasabl  19845  cycsubmcmn  19858  0cyg  19862  cycsubgcyg  19870  gsumval3  19876  gsumcllem  19877  gsumzaddlem  19890  gsumzsplit  19896  gsummptfzcl  19938  eldprd  19975  dprdcntz2  20009  dprd2d2  20015  dmdprdsplit2lem  20016  dmdprdsplit2  20017  dprdsplit  20019  ablfac2  20060  isrngd  20148  rngpropd  20149  imasrng  20152  qusrng  20155  ringurd  20160  isringd  20266  imasring  20304  xpsring1d  20307  dvdsrval  20335  isunit  20347  dvdsrpropd  20390  isirred  20393  isrnghm  20415  isrngim  20419  c0ghm  20435  c0snghm  20438  isrhm  20452  isrim0  20456  islring  20511  issubrng  20518  opprsubrng  20530  issubrg  20542  opprsubrg  20564  resrhm2b  20573  rhmpropd  20580  rnghmresel  20591  elrngchom  20595  rnghmsubcsetclem1  20602  rnghmsubcsetclem2  20603  rngcid  20606  rngcsect  20607  rngciso  20609  funcrngcsetcALT  20612  zrinitorngc  20613  zrtermorngc  20614  rhmresel  20620  elringchom  20624  rhmsubcsetclem1  20631  rhmsubcsetclem2  20632  ringcid  20635  rhmsscrnghm  20636  rhmsubcrngclem1  20637  rhmsubcrngclem2  20638  ringcsect  20641  ringciso  20643  ringcbasbas  20644  zrtermoringc  20646  srhmsubc  20651  rhmsubclem3  20658  rhmsubclem4  20659  drngunit  20705  isdrngd  20736  isdrngdOLD  20738  issdrg  20759  sdrgunit  20767  isabv  20782  issrngd  20826  islmod  20853  lmodprop2d  20913  islss  20923  islssd  20924  lssats2  20989  ellspsn  20992  islmhm  21017  lmhmf1o  21036  lmhmima  21037  lmhmpreima  21038  reslmhm  21042  pwssplit3  21051  lmhmpropd  21063  islbs  21066  lspprel  21084  lspfixed  21121  lbsacsbs  21149  lbsextlem1  21151  lbsextlem2  21152  lbsextlem3  21153  lbsextlem4  21154  ixpsnbasval  21198  isridlrng  21212  rnglidlmmgm  21238  isridl  21245  quscrng  21276  rngqiprngimfolem  21283  rngqiprngimf1lem  21287  rngqiprngimfo  21294  islpidl  21318  lidldvgen  21327  irinitoringc  21472  pzriprnglem13  21486  pzriprnglem14  21487  zrhrhmb  21503  znf1o  21544  frgpcyg  21566  psgnevpmb  21580  isphld  21647  phlssphl  21652  elocv  21661  iscss  21676  isobs  21713  obs2ss  21722  dsmmfi  21731  dsmmelbas  21732  dsmmlss  21737  frlmelbas  21749  frlmlbs  21790  frlmup1  21791  ellspd  21795  islinds  21802  islindf2  21807  f1lindf  21815  islindf4  21831  assamulgscmlem2  21893  psrgrp  21948  mplsubglem  21990  mpllsslem  21991  mplmonmul  22027  subrgascl  22057  subrgasclcl  22058  mpfind  22106  ismhp  22119  gsumply1subr  22210  lply1binomsc  22289  matbas2d  22401  matecl  22403  matvscl  22409  mat1  22425  mat0dim0  22445  mat0dimid  22446  mat0dimscm  22447  mat1dimelbas  22449  dmatel  22471  scmatel  22483  scmateALT  22490  scmataddcl  22494  scmatsubcl  22495  smatvscl  22502  scmatghm  22511  mat1scmat  22517  mdetunilem7  22596  mdetunilem9  22598  smadiadetr  22653  cramerimplem2  22662  cramer0  22668  pmatcoe1fsupp  22679  cpmatpmat  22688  cpmatel  22689  cpmatacl  22694  cpmatinvcl  22695  mat2pmatghm  22708  mat2pmatmul  22709  decpmatmullem  22749  pmatcollpwlem  22758  pmatcollpw3fi1lem1  22764  pmatcollpwscmatlem1  22767  monmat2matmon  22802  chfacfscmul0  22836  chfacfscmulgsum  22838  chfacfpmmulgsum  22842  cayhamlem1  22844  cpmadugsumlemB  22852  cpmadugsumlemC  22853  cpmadugsumlemF  22854  cayhamlem2  22862  istopon  22890  eltg  22935  eltg2  22936  eltop  22952  eltop2  22953  eltop3  22954  pptbas  22986  iscld  23005  neiss2  23079  isnei  23081  neiptopnei  23110  neiptopreu  23111  lpfval  23116  lpval  23117  islp  23118  maxlp  23125  islpi  23127  neitr  23158  restlp  23161  ordtbas2  23169  ordtrest2  23182  lmfval  23210  cnfval  23211  iscn  23213  iscnp  23215  tgcn  23230  tgcnp  23231  lmbrf  23238  cnpresti  23266  ist1  23299  ist1-2  23325  cnt1  23328  haust1  23330  cmpfi  23386  cmpfii  23387  1stcfb  23423  2ndc1stc  23429  1stcrest  23431  2ndcdisj  23434  1stcelcls  23439  nllyi  23453  subislly  23459  islocfin  23495  lfinpfin  23502  locfindis  23508  locfincf  23509  comppfsc  23510  kgenval  23513  elkgen  23514  kgencn2  23535  txbas  23545  eltx  23546  ptval  23548  ptpjpre1  23549  ptopn2  23562  ptpjopn  23590  ptclsg  23593  xkoccn  23597  txdis  23610  txdis1cn  23613  ptrescn  23617  hausdiag  23623  hauseqlcld  23624  txhaus  23625  xkohaus  23631  elqtop  23675  qtopeu  23694  kqcldsat  23711  hmeofval  23736  ptuncnv  23785  ptunhmeo  23786  elmptrab  23805  fbdmn0  23812  elfg  23849  elfilss  23854  filunirn  23860  fixufil  23900  elfm  23925  rnelfmlem  23930  rnelfm  23931  fmfnfmlem4  23935  elflim2  23942  flimtopon  23948  elflim  23949  hausflim  23959  flimcls  23963  flfnei  23969  isflf  23971  hausflf  23975  cnpflf  23979  cnflf  23980  txflf  23984  isfcls  23987  fclstopon  23990  isfcls2  23991  fclssscls  23996  fclsnei  23997  fclsfnflim  24005  flimfnfcls  24006  isfcf  24012  fcfelbas  24014  cnpfcf  24019  cnfcf  24020  flfcntr  24021  alexsublem  24022  alexsubALTlem3  24027  cnextfun  24042  cnextfvval  24043  cnextf  24044  cnextcn  24045  tmdgsum2  24074  tgpconncomp  24091  ghmcnp  24093  qustgplem  24099  eltsms  24111  haustsms  24114  tsmsgsum  24117  tsmssubm  24121  tsmssplit  24130  isust  24182  ustbas  24205  elutop  24211  ustuqtoplem  24217  ustuqtop4  24222  ustuqtop  24224  utopsnneiplem  24225  utopsnneip  24226  utopsnnei  24227  isusp  24239  isucn  24255  ucncn  24262  iscfilu  24265  neipcfilu  24273  iscusp  24276  cnextucn  24280  ispsmet  24282  ismet  24301  isxmet  24302  elblps  24365  elbl  24366  elmopn  24420  prdsbl  24469  neibl  24479  met1stc  24499  metrest  24502  prdsxmslem2  24507  txmetcnp  24525  txmetcn  24526  metustsym  24533  cfilucfil2  24539  elbl4  24541  metuel  24542  psmetutop  24545  restmetu  24548  metucn  24549  tngngp  24632  isnmhm  24724  zcld  24792  metnrmlem1a  24837  elcncf  24869  cncfcnvcn  24905  cnheibor  24935  lebnumlem1  24941  ishtpy  24952  isphtpy  24961  om1elbas  25012  elpi1  25025  pi1xfr  25035  pi1coghm  25041  tcphcph  25217  lmmbrf  25242  iscfil  25245  iscau  25256  iscauf  25260  caucfil  25263  iscmet  25264  cmetcaulem  25268  iscmet3lem1  25271  iscmet3lem2  25272  iscmet3  25273  bcthlem1  25304  cmsss  25331  cmetcusp1  25333  cmetcusp  25334  cmscsscms  25353  rrxcph  25372  minveclem3b  25408  ovolfioo  25447  ovolficc  25448  ovolctb  25470  ovoliunnul  25487  ovolshftlem1  25489  sca2rab  25492  ovolscalem1  25493  ovolicc2lem1  25497  ovolicc2lem2  25498  ovolicc2lem4  25500  ovolicc2lem5  25501  iundisj  25528  iunmbl2  25537  uniioombllem3  25565  vitalilem2  25589  vitalilem3  25590  mbfss  25626  i1faddlem  25673  i1fmullem  25674  mbfi1fseqlem2  25696  mbfi1fseqlem4  25698  mbfi1fseq  25701  itg2splitlem  25728  itg2split  25729  itg2monolem1  25730  itg2gt0  25740  isibl  25745  iblss2  25786  itgss3  25795  itgsplit  25816  ellimc  25853  limcmo  25862  cnlimc  25868  limciun  25874  limcun  25875  eldv  25878  dvbsss  25882  dvreslem  25889  elcpn  25914  dvaddf  25922  dvmulf  25923  dvcof  25928  rolle  25970  dvlip2  25975  dvivthlem1  25988  lhop1  25994  lhop2  25995  ftc1cn  26023  fta1glem2  26147  plyco0  26170  elply  26173  ply1termlem  26181  eltayl  26339  tayl0  26341  taylplem1  26342  taylplem2  26343  dvtaylp  26350  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  abelth  26422  cxpcn3  26728  rlimcnp  26945  fsumharmonic  26992  dchrelbas  27216  pntrsumbnd2  27547  ostth2lem2  27614  nolesgn2ores  27653  nogesgn1ores  27655  nosupprefixmo  27681  noinfprefixmo  27682  nosupcbv  27683  nosupdm  27685  nosupfv  27687  nosupres  27688  nosupbnd1lem1  27689  nosupbnd1lem3  27691  nosupbnd1lem5  27693  nosupbnd2lem1  27696  noinfcbv  27698  noinfdm  27700  noinffv  27702  noinfres  27703  noinfbnd1lem1  27704  noinfbnd1lem3  27706  noinfbnd1lem5  27708  noinfbnd2lem1  27711  elmade  27866  elold  27868  sltsleft  27869  sltsright  27870  oldlim  27896  madebday  27909  newbday  27911  ltslpss  27917  bdayiun  27924  cofcutr  27933  cofcutrtime  27936  lrrecval  27948  lrrecval2  27949  addsval  27971  precsexlem9  28224  precsexlem11  28226  ltonold  28270  onnolt  28275  onlts  28276  noseqrdgfn  28315  istrkgb  28540  istrkgcb  28541  istrkge  28542  istrkgl  28543  istrkgld  28544  axtgsegcon  28549  axtg5seg  28550  axtgbtwnid  28551  axtgpasch  28552  axtgupdim2  28556  axtgeucl  28557  tgdim01  28592  iscgrg  28597  isismt  28619  tglnunirn  28633  tglngval  28636  tgellng  28638  legval  28669  legov  28670  legov2  28671  ishlg  28687  mirreu3  28739  mirval  28740  mirfv  28741  mircgr  28742  mirbtwn  28743  ismir  28744  mireq  28750  symquadlem  28774  israg  28782  perpln1  28795  perpln2  28796  isperp  28797  islnopp  28824  outpasch  28840  ishpg  28844  iscgra  28894  dfcgra2  28915  isinag  28923  isleag  28932  iseqlg  28952  f1otrgitv  28955  f1otrg  28956  f1otrge  28957  ttgval  28960  ttgelitv  28968  elee  28979  brbtwn  28985  brcgr  28986  axlowdimlem16  29043  ebtwntg  29068  elntg2  29071  upgrex  29178  edgupgr  29220  upgredg  29223  edglnl  29229  numedglnl  29230  uhgr2edg  29294  umgr2edg1  29297  usgredg2vlem1  29311  usgredg2vlem2  29312  ushgredgedg  29315  ushgredgedgloop  29317  uhgrspansubgrlem  29376  fusgrfisstep  29415  nbgrval  29422  nbgrel  29426  nbupgrel  29431  nbgr2vtx1edg  29436  nbuhgr2vtx1edgblem  29437  nbuhgr2vtx1edgb  29438  nbusgreledg  29439  usgrnbcnvfv  29451  uvtxval  29473  uvtxel  29474  uvtx01vtx  29483  uvtxusgrel  29489  nbcplgr  29520  cplgr3v  29521  cusgrexi  29529  structtocusgr  29532  vtxdgfval  29554  vtxdg0v  29560  vtxdeqd  29564  vtxdun  29568  1loopgrnb0  29589  1loopgrvd0  29591  1hevtxdg0  29592  1hevtxdg1  29593  1egrvtxdg1  29596  umgr2v2evtxel  29609  umgr2v2enb1  29613  umgr2v2evd2  29614  vtxdginducedm1lem4  29629  vtxdginducedm1  29630  finsumvtxdg2sstep  29636  ewlksfval  29688  isewlk  29689  wksfval  29696  iswlk  29697  uspgr2wlkeq  29732  wlkres  29755  dfpth2  29815  usgr2pthlem  29849  clwlkcompim  29866  uspgrn2crct  29894  wwlks  29921  iswwlksn  29924  wwlknvtx  29931  wlkiswwlks2  29961  wwlksm1edg  29967  wwlksnred  29978  wwlksnext  29979  wwlksnredwwlkn  29981  wwlksnredwwlkn0  29982  wwlksnwwlksnon  30001  wspn0  30010  usgr2wspthons3  30053  rusgrnumwwlkb0  30060  clwwlk  30071  clwwlkccatlem  30077  clwlkclwwlklem2a4  30085  clwlkclwwlk  30090  clwwisshclwwslem  30102  clwwlkinwwlk  30128  clwwlkel  30134  clwwlkf  30135  clwwlkext2edg  30144  wwlksext2clwwlk  30145  wwlksubclwwlk  30146  clwwnisshclwwsn  30147  eleclclwwlknlem2  30149  erclwwlknsym  30158  erclwwlkntr  30159  umgrhashecclwwlk  30166  clwwlkvbij  30201  eupth2lem3lem3  30318  eupth2lem3lem4  30319  eupth2lem3lem6  30321  eupth2lemb  30325  eucrct2eupth  30333  fusgreg2wsplem  30421  2clwwlklem  30431  2clwwlk2clwwlklem  30434  2clwwlkel  30437  2clwwlk2clwwlk  30438  extwwlkfabel  30441  clwwlknonclwlknonf1o  30450  dlwwlknondlwlknonf1olem1  30452  numclwwlk2lem1  30464  numclwlk2lem2f  30465  numclwlk2lem2f1o  30467  ex-res  30529  isssp  30813  sspn  30825  islno  30842  isblo  30871  nmlno0  30884  ishmo  30900  dipdir  30931  dipass  30934  ubthlem1  30959  ubthlem2  30960  htthlem  31006  htth  31007  ocel  31370  ocnel  31387  shsel  31403  shsel2  31411  shmodsi  31478  pjhtheu  31483  pjeq  31488  axpjpj  31509  pjoc2  31528  elspani  31632  h1de2ctlem  31644  elspansn  31655  elspansn2  31656  elnlfn  32017  eleigvec  32046  riesz3i  32151  cbviunf  32643  iuneq12daf  32644  iunrdx  32651  iunrnmptss  32653  cbvdisjf  32659  disjorf  32667  disjabrex  32670  disjabrexf  32671  iundisjf  32677  disjrdx  32679  brab2d  32696  fresunsn  32716  2ndresdju  32740  abfmpunirn  32743  abfmpeld  32745  abfmpel  32746  fmptcof2  32748  acunirnmpt2  32751  acunirnmpt2f  32752  aciunf1lem  32753  suppss3  32814  fpwrelmap  32824  xrofsup  32858  iundisjfi  32887  eliccioo  33008  s3f1  33025  ccatf1  33027  ccatws1f1o  33029  swrdrn3  33033  ismnt  33061  mgcoval  33064  gsummpt2co  33127  gsumpart  33142  gsumhashmul  33146  gsummulsubdishift1  33147  xrge0tsmsbi  33153  gsumwrd2dccatlem  33156  gsumwrd2dccat  33157  cycpmco2  33212  cyc3co2  33219  isfxp  33247  cntrval2  33250  inftmrel  33259  isinftm  33260  isslmd  33281  urpropd  33310  elrgspn  33325  erlval  33337  rlocval  33338  rloccring  33349  rloc1r  33351  domnprodeq0  33355  domnpropd  33356  isdrng4  33374  fracfld  33387  resv1r  33417  ellspds  33446  ellpi  33451  lbslsp  33455  rhmimaidl  33510  isprmidl  33516  qsidomlem1  33530  qsidomlem2  33531  ismxidl  33540  crngmxidl  33547  drng0mxidl  33554  opprqus0g  33568  qsfld  33576  isrprm  33595  rsprprmprmidlb  33601  ressply1evls1  33643  ply1mulrtss  33660  ply1coedeg  33667  psrmonmul  33712  dimpropd  33771  lbslsat  33779  extdg1id  33829  fldextrspunlsplem  33836  fldextrspunlsp  33837  elirng  33849  ply1annidllem  33864  constrsuc  33901  constrconj  33908  constrllcllem  33915  constrlccllem  33916  constrcccllem  33917  nn0constr  33924  smatrcl  33959  smatcl  33965  ist0cld  33996  txomap  33997  locfinreflem  34003  zarclsiin  34034  zart0  34042  rhmpreimacnlem  34047  metidval  34053  cnre2csqima  34074  ordtrest2NEW  34086  fmcncfil  34094  fsumcvg4  34113  ofcfval  34261  measvuni  34377  meascnbl  34382  faeval  34409  ismbfm  34414  elunirnmbfm  34415  imambfm  34425  elcarsg  34468  itgeq12dv  34489  issibf  34496  eulerpartlems  34523  eulerpartlemgc  34525  eulerpartlemgvv  34539  eulerpartlemgu  34540  eulerpart  34545  rrvmbfm  34605  elorvc  34623  elorrvc  34627  dstfrvunirn  34638  ballotlemfc0  34656  ballotlemfcc  34657  ballotlemsima  34679  ballotlemrv  34683  fzssfzo  34702  signstfvn  34732  signstfvneq0  34735  signstres  34738  repr0  34774  reprinrn  34781  reprdifc  34790  hgt750lemg  34817  hgt750lemb  34819  istrkg2d  34829  axtgupdim2ALTV  34831  afsval  34834  brafs  34835  bnj945  34935  bnj1400  34996  bnj18eq1  35088  bnj916  35094  bnj1014  35122  bnj1015  35123  bnj1110  35143  bnj1417  35202  rankval2b  35261  r1filimi  35265  r1ssel  35269  onvf1odlem3  35306  vonf1owev  35309  revpfxsfxrev  35317  cplgredgex  35322  pfxwlk  35325  revwlk  35326  subfacp1lem2b  35382  subfacp1lem4  35384  subfacp1lem5  35385  subfacp1lem6  35386  ptpconn  35434  cvmscbv  35459  iscvm  35460  cvmsi  35466  cvmsval  35467  cvmliftmolem1  35482  cvmlift2lem12  35515  cvmlift2lem13  35516  cvmlift3lem7  35526  snmlval  35532  satfv1  35564  satfvsucsuc  35566  satfrnmapom  35571  satf0op  35578  satf0n0  35579  sat1el2xp  35580  fmlafvel  35586  isfmlasuc  35589  fmlaomn0  35591  gonan0  35593  goaln0  35594  gonar  35596  goalr  35598  satffunlem1lem2  35604  satffunlem2lem2  35607  satfv0fvfmla0  35614  satef  35617  satefvfmla0  35619  sategoelfvb  35620  satfv1fvfmla1  35624  mrsubfval  35709  mrsubvrs  35723  mclsrcl  35762  mclsval  35764  mppsval  35773  mclsppslem  35784  opelco3  35976  wsuclem  36024  funtransport  36232  fvtransport  36233  brcolinear  36260  colineardim1  36262  funray  36341  fvray  36342  funline  36343  fvline  36345  lineelsb2  36349  fwddifval  36363  fwddifnval  36364  rankelg  36369  rankeq1o  36372  elhf2  36376  0hf  36378  rmoeqbidv  36414  disjeq12dv  36416  ixpeq12dv  36417  prodeq12sdv  36419  itgeq12sdv  36420  cbvralvw2  36427  cbvrexvw2  36428  cbvrmovw2  36429  cbvreuvw2  36430  cbvcsbvw2  36432  cbviunvw2  36433  cbviinvw2  36434  cbvmptvw2  36435  cbvdisjvw2  36436  cbvmpo1vw2  36444  cbvmpo2vw2  36445  cbvsbcdavw  36458  cbvcsbdavw  36460  cbvcsbdavw2  36461  cbviundavw  36463  cbviindavw  36464  cbvdisjdavw  36469  cbvrabdavw2  36486  cbviundavw2  36487  cbviindavw2  36488  cbvmptdavw2  36489  cbvdisjdavw2  36490  cbvriotadavw2  36491  cbvmpo1davw2  36493  cbvmpo2davw2  36494  cbvsumdavw2  36496  neibastop2lem  36561  neibastop3  36563  eltail  36575  ttctr  36694  dfttc2g  36707  mh-infprim2bi  36748  bj-projeq  37318  bj-projval  37322  bj-restsn  37413  opelopabbv  37476  brabd0  37480  bj-eldiag  37509  bj-eldiag2  37510  mptsnunlem  37671  dissneqlem  37673  iooelexlt  37695  relowlssretop  37696  rdgellim  37709  exrecfnlem  37712  finxpeq1  37719  finxpreclem6  37729  pibp21  37748  curf  37936  uncf  37937  curunc  37940  unccur  37941  fin2so  37945  lindsadd  37951  lindsdom  37952  lindsenlbs  37953  matunitlindflem1  37954  matunitlindflem2  37955  matunitlindf  37956  ptrest  37957  ptrecube  37958  poimirlem2  37960  poimirlem8  37966  poimirlem17  37975  poimirlem18  37976  poimirlem20  37978  poimirlem21  37979  poimirlem22  37980  poimirlem24  37982  poimirlem26  37984  poimirlem29  37987  heicant  37993  mblfinlem1  37995  mblfinlem2  37996  volsupnfl  38003  itg2addnclem  38009  itg2gt0cn  38013  indexdom  38072  incsequz  38086  istotbnd  38107  istotbnd3  38109  0totbnd  38111  sstotbnd  38113  sstotbnd3  38114  isbnd  38118  prdstotbnd  38132  cntotbnd  38134  isismty  38139  heibor1lem  38147  heiborlem2  38150  heiborlem3  38151  heibor  38159  isass  38184  exidcl  38214  exidreslem  38215  elghomlem2OLD  38224  rngoidmlem  38274  rngo1cl  38277  divrngcl  38295  isdrngo2  38296  isrngohom  38303  isrngoiso  38316  isriscg  38322  iscom2  38333  iscringd  38336  isidl  38352  ispridl  38372  ismaxidl  38378  ac6s6  38510  dmecd  38648  dfpre4  38818  releldmqs  39081  releldmqscoss  39083  erimeq2  39101  qmapeldisjsim  39198  eldisjlem19  39251  membpartlem19  39252  prter3  39345  islshp  39442  islsat  39454  lcvfbr  39483  islfl  39523  ellkr  39552  islshpkrN  39583  ldual1dim  39629  isopos  39643  cmtfvalN  39673  cvrfval  39731  isat  39749  islln  39969  islpln  39993  islvol  40036  isline  40202  ispointN  40205  ispsubsp  40208  elpmap  40221  elpmapat  40227  elpadd  40262  paddclN  40305  elpclN  40355  elpcliN  40356  pclfinN  40363  pclcmpatN  40364  ispsubclN  40400  iswatN  40457  islhp  40459  islaut  40546  ispautN  40562  isldil  40573  isltrn  40582  isdilN  40617  istrnN  40620  istendo  41223  dvhb1dimN  41449  erng1lem  41450  erngdvlem4-rN  41462  diaelval  41496  diaeldm  41499  dia1dimid  41526  cdlemm10N  41581  dibopelvalN  41606  dibopelval2  41608  dibelval3  41610  dibelval1st  41612  dibelval2nd  41615  dibeldmN  41621  dibvalrel  41626  dibglbN  41629  dicffval  41637  dicfval  41638  dicopelval  41640  dicelvalN  41641  dicelval3  41643  dicvalrelN  41648  dicelval1sta  41650  diclspsn  41657  dihopelvalbN  41701  dihopelvalcqat  41709  dihopelvalcpre  41711  dihvalrel  41742  dih1  41749  dihmeetlem4preN  41769  dihmeetlem13N  41782  dih1dimatlem  41792  dochnel2  41855  dihjatcclem4  41884  dvh2dim  41908  dvh3dim  41909  dvh4dimN  41910  dochfln0  41940  lpolsetN  41945  islpolN  41946  lcfrvalsnN  42004  lcfrlem21  42026  lcfrlem27  42032  lcfrlem37  42042  lcfr  42048  lcdlss  42082  mapdcv  42123  hdmap1fval  42259  hdmapffval  42289  hdmapfval  42290  hdmapval  42291  hgmapffval  42348  hgmapfval  42349  hdmapellkr  42377  hlhilhillem  42423  fzsplitnd  42438  isprimroot  42549  primrootsunit1  42553  primrootscoprmpow  42555  primrootscoprbij  42558  aks6d1c1p2  42565  aks6d1c1p3  42566  aks6d1c1p4  42567  aks6d1c1p5  42568  aks6d1c1p6  42570  aks6d1c1  42572  evl1gprodd  42573  sticksstones11  42612  sticksstones12a  42613  rhmqusspan  42641  grpods  42650  fzosumm1  42706  frlmfielbas  42962  frlmsnic  43002  psrmnd  43005  isnacs  43153  mrefg2  43156  elmzpcl  43175  mzpcompact2  43201  eldiophb  43206  elpell1qr  43296  elpell14qr  43298  elpell1234qr  43300  pw2f1ocnv  43486  pw2f1o2val2  43489  aomclem4  43506  aomclem6  43508  islssfg2  43520  imasgim  43549  lnr2i  43565  elmnc  43585  rngunsnply  43618  onexomgt  43690  onexlimgt  43692  onexoegt  43693  oaordnr  43745  omnord1  43754  oenord1  43765  cantnfresb  43773  tfsconcatun  43786  tfsconcat0i  43794  ofoaf  43804  naddcnff  43811  naddcnffo  43813  naddcnfcom  43815  naddcnfid1  43816  naddcnfid2  43817  naddcnfass  43818  naddwordnexlem4  43850  fiinfi  44021  sqrtcvallem1  44079  elintima  44101  eliunov2  44127  ov2ssiunov2  44148  brtrclfv2  44175  rfovcnvf1od  44452  rfovcnvfvd  44455  fsovrfovd  44457  fsovfvd  44458  fsovcnvlem  44461  ntrclsfv1  44503  ntrclselnel1  44505  ntrclsneine0lem  44512  ntrneifv1  44527  ntrneifv2  44528  ntrneiel  44529  gneispace2  44580  gneispacess2  44594  extoimad  44612  mnringelbased  44665  dvconstbi  44782  bccbc  44793  wfac8prim  45450  permaxrep  45454  permac8prim  45462  eliin2f  45555  iineq12dv  45557  rabbida2  45583  disjinfi  45643  unirnmap  45658  elmptima  45708  iuneqfzuzlem  45785  iooiinioc  46007  fsumiunss  46026  fsumsupp0  46029  lptre2pt  46089  icccncfext  46336  cncfiooicclem1  46342  dvnprodlem2  46396  stoweidlem27  46476  stoweidlem29  46478  stoweidlem31  46480  stoweidlem34  46483  stoweidlem48  46497  stoweidlem59  46508  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem2  46558  fourierdlem3  46559  fourierdlem25  46581  fourierdlem32  46588  fourierdlem33  46589  fourierdlem41  46597  fourierdlem48  46603  fourierdlem49  46604  fourierdlem62  46617  fourierdlem70  46625  fourierdlem80  46635  fourierdlem92  46647  fourierdlem93  46648  fourierdlem101  46656  etransclem37  46720  sge0val  46815  sge0f1o  46831  sge0iunmptlemre  46864  sge0iunmpt  46867  iundjiun  46909  caragenel  46944  ovncvrrp  47013  ovnsubaddlem1  47019  ovnsubadd  47021  hoidmvlelem2  47045  hoidmvlelem3  47046  hoidmvlelem4  47047  hoidmvle  47049  ovncvr2  47060  hspdifhsp  47065  hoiqssbl  47074  hspmbllem2  47076  hspmbl  47078  opnvonmbllem1  47081  isvonmbl  47087  ovnovollem1  47105  issmflem  47176  smflimlem3  47222  smflimlem4  47223  smflim  47226  smfmullem2  47241  smflimmpt  47259  smfsuplem1  47260  smflimsuplem1  47269  smflimsuplem3  47271  smflimsuplem4  47272  smflimsuplem7  47275  smflimsup  47277  chnsubseq  47329  fcores  47530  fcoresf1  47532  afvelrnb  47626  afvelrnb0  47627  afv2co2  47720  el1fzopredsuc  47789  muldvdsfacm1  47850  iccpart  47891  iccpartgtprec  47895  iccpartiltu  47897  iccpartigtl  47898  iccpartltu  47900  iccpartgtl  47901  iccpartgt  47902  iccpartleu  47903  iccpartgel  47904  iccelpart  47908  iccpartiun  47909  icceuelpart  47911  fargshiftfv  47914  fargshiftfo  47917  sprel  47959  prprelb  47991  prprelprb  47992  nprmdvdsfacm1lem4  48101  fpprel  48219  sbgoldbo  48278  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem3  48298  bgoldbtbnd  48300  clnbgrval  48313  elclnbgrelnbgr  48316  clnbgrel  48319  clnbupgrel  48325  vopnbgrel  48345  isubgredg  48357  upgrimwlklem3  48390  upgrimwlklem5  48392  upgrimpths  48400  grtriprop  48432  isgrtri  48434  grtriclwlk3  48436  stgredgel  48448  gpgvtxel  48538  gpgiedgdmel  48540  gpgedgel  48541  opgpgvtx  48546  gpg5nbgrvtx13starlem1  48562  gpg5nbgrvtx13starlem2  48563  gpg5nbgrvtx13starlem3  48564  gpg3kgrtriex  48580  grlimedgnedg  48622  upwlksfval  48626  isupwlk  48627  intop  48694  isclintop  48698  assintop  48700  isassintop  48701  assintopcllaw  48703  uzlidlring  48726  elrngchomALTV  48760  rngccatidALTV  48763  rngcsectALTV  48766  rngcisoALTV  48768  rhmsubcALTVlem3  48774  rhmsubcALTVlem4  48775  funcringcsetcALTV2lem7  48787  funcringcsetcALTV2lem9  48789  elringchomALTV  48794  ringccatidALTV  48797  ringcsectALTV  48800  ringcisoALTV  48802  ringcbasbasALTV  48803  funcringcsetclem7ALTV  48810  funcringcsetclem9ALTV  48812  srhmsubcALTV  48816  cbvmpox2  48827  ply1sclrmsm  48875  dmatALTbasel  48893  lcoval  48903  lindslinindsimp1  48948  lindslinindsimp2  48954  lmod1  48983  elbigo  49042  elbigo2  49043  elbigolo1  49048  dig2nn0ld  49095  naryfvalel  49121  rrxlines  49224  rrxlinesc  49226  rrxlinec  49227  eenglngeehlnm  49230  elrrx2linest2  49236  rrxsphere  49239  itsclc0  49262  itsclc0b  49263  itsclinecirc0  49264  itsclinecirc0b  49265  itscnhlinecirc02p  49276  brab2dd  49318  f1omo  49383  f1omoOLD  49384  lubeldm2d  49448  glbeldm2d  49449  catprs  49501  sectpropdlem  49526  nelsubc3lem  49560  initc  49581  imaid  49644  upfval  49666  upfval2  49667  upfval3  49668  uppropd  49671  oppcinito  49725  oppctermo  49726  oppczeroo  49727  initopropd  49733  termopropd  49734  isthinc  49909  isthincd2lem1  49915  thincmoALT  49919  thincmod  49920  isthincd  49926  thincpropd  49932  indcthing  49950  discthing  49951  prsthinc  49954  termcterm  50003  termc2  50008  isinito4  50037  2arwcatlem1  50085  setc1onsubc  50092  cnelsubclem  50093  ranval3  50121  lmdfval2  50145  cmdfval2  50146  termolmd  50160  elsetrecslem  50189