Theorem eleq2d 2814

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eleq2  2817  eleq12d  2822  eleqtrd  2830  neleqtrd  2850  eqabrd  2870  raleqbidv  3310  rexeqbidv  3311  reueqbidv  3385  rabeqbidva  3413  elabd2  3627  sbcbid  3799  csbeq2d  3859  csbeq2dv  3860  cbvcsbw  3863  cbvcsb  3864  cbvcsbv  3865  csbie  3888  csbied  3889  csbie2g  3893  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  sbcel12  4364  sbcel1g  4369  sbcel2  4371  prel12g  4818  eliuni  4950  iuneqconst  4956  iuneq12df  4971  iuneq12d  4974  cbviun  4988  cbviin  4989  cbviung  4990  cbviing  4991  cbviunv  4992  cbviinv  4993  iinxsng  5040  iinxprg  5041  iunxsng  5042  iunxsngf  5044  cbvdisj  5072  cbvdisjv  5073  disjor  5077  disjiund  5086  mpteq12da  5178  mpteq12f  5180  mpteq12dva  5181  axpweq  5293  rabxfrd  5359  rbropapd  5509  opeliunxp  5690  opeliun2xp  5691  opeliunxp2  5785  iunxpf  5795  elimampt  5998  elrelimasn  6041  elimasni  6046  imadifssran  6104  xpdifid  6121  ressn  6237  funfni  6592  fnbr  6594  dffv3  6822  elfv2ex  6870  fvelrnb  6887  foelcdmi  6888  fvun1  6918  fvco2  6924  elfvmptrab1w  6961  elfvmptrab1  6962  elfvmptrab  6963  elpreima  6996  dff3  7038  fmptco  7067  fnelfp  7115  fnelnfp  7117  tpres  7141  fnprb  7148  fntpb  7149  funfvima3  7176  eluniima  7190  elunirn2OLD  7193  dff13  7195  f1ounsn  7213  f1eqcocnv  7242  isoini  7279  riotaeqdv  7311  mpoeq123dva  7427  cbvmpox  7446  elimampo  7490  ovelrn  7529  elovmpod  7597  elovmpo  7598  elovmporab  7599  elovmporab1w  7600  elovmporab1  7601  elovmpt3rab1  7613  fiun  7885  f1iun  7886  zfrep6  7897  fmpox  8009  el2mpocsbcl  8025  el2mpocl  8026  bropopvvv  8030  bropfvvvv  8032  xpord2indlem  8087  xpord3inddlem  8094  elsuppfng  8109  elsuppfn  8110  suppfnss  8129  opeliunxp2f  8150  mpoxopn0yelv  8153  mpoxopovel  8160  rntpos  8179  mpocurryd  8209  fpr2  8244  wfr2  8267  onoviun  8273  smoel  8290  smoiso  8292  smoel2  8293  smo11  8294  tfrlem9  8314  oalimcl  8485  oaass  8486  omordi  8491  omordlim  8502  omlimcl  8503  odi  8504  omeulem1  8507  omeulem2  8508  oen0  8511  oeordi  8512  oeordsuc  8519  oelimcl  8525  oeeulem  8526  oeeui  8527  nnmordi  8556  oaabs2  8574  omabs  8576  omsmolem  8582  ereldm  8685  iiner  8723  elmapg  8773  elpmg  8777  elixpsn  8871  ixpsnf1o  8872  boxriin  8874  omxpenlem  9002  pw2f1olem  9005  phplem2  9129  php3  9133  infn0  9209  elfi  9322  dffi3  9340  marypha2lem2  9345  ordiso2  9426  wemapsolem  9461  elharval  9472  inf3lemd  9542  inf3lem1  9543  inf3lem2  9544  inf3lem3  9545  cantnfs  9581  cantnfp1lem3  9595  cantnflem1b  9601  cantnflem1  9604  ttrclselem2  9641  trcl  9643  frr2  9675  r1sdom  9689  r1ordg  9693  r1pwss  9699  tz9.12lem3  9704  tz9.12  9705  r1elwf  9711  rankr1ai  9713  rankidb  9715  rankr1bg  9718  rankval2  9733  rankunb  9765  tcrank  9799  acni  9958  acni2  9959  acndom  9964  infpwfien  9975  alephnbtwn  9984  cardaleph  10002  cardinfima  10010  iunfictbso  10027  dfac3  10034  dfac5lem5  10040  dfac5  10042  dfac9  10050  dfac12r  10060  kmlem2  10065  kmlem12  10075  kmlem13  10076  kmlem14  10077  ackbij2lem3  10153  ackbij2  10155  cofsmo  10182  alephsing  10189  fin23lem30  10255  isf32lem9  10274  itunisuc  10332  axcc2lem  10349  axcc3  10351  domtriomlem  10355  axdc2lem  10361  axdc2  10362  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  ac6c4  10394  zorn2lem1  10409  ttukeylem6  10427  pwcfsdom  10496  axregndlem2  10516  axinfndlem1  10518  axacndlem4  10523  axacnd  10525  pwfseqlem1  10571  inar1  10688  inatsk  10691  gruurn  10711  grur1  10733  eltskm  10756  genpelv  10913  eluz1  12757  eluzaddOLD  12788  eluzsubOLD  12789  elixx1  13275  elixx3g  13279  elioo2  13307  elfz1  13433  elfz2  13435  elfzp1  13495  fzpr  13500  fzsuc2  13503  fzrev3  13511  elfzp12  13524  fzm1  13528  elfzo  13582  fz0add1fz1  13656  elfzo0l  13677  elfzom1b  13687  fzosplitsni  13699  elfzr  13701  elfzlmr  13702  zmodidfzo  13822  seqp1  13941  seqf1o  13968  bcval  14229  bcpasc  14246  hashf1lem1  14380  fundmge2nop0  14427  wrdmap  14471  elovmpowrd  14483  ccatfval  14498  elfzelfzccat  14505  ccatlid  14511  ccatass  14513  ccatrn  14514  ccatalpha  14518  swrdfv2  14586  ccatswrd  14593  swrdccat2  14594  pfxfv  14607  pfxeq  14620  ccatpfx  14625  swrdswrd  14629  swrdpfx  14631  pfxpfx  14632  cats1un  14645  swrdccatfn  14648  swrdccatin1  14649  pfxccatin12lem4  14650  pfxccatin12lem1  14652  swrdccatin2  14653  pfxccatin12lem2c  14654  pfxccatin12lem2  14655  swrdccat3blem  14663  swrdccatin1d  14667  swrdccatin2d  14668  pfxccatin12d  14669  revccat  14690  revrev  14691  repswpfx  14709  repswccat  14710  cshwidxmod  14727  2cshw  14737  cshwcshid  14752  cshwcsh2id  14753  cshimadifsn  14754  cshimadifsn0  14755  revco  14759  ccatco  14760  cshco  14761  swrdco  14762  ofccat  14894  shftfn  14998  shftval  14999  limsupgle  15402  ello12  15441  elo12  15452  isercolllem3  15592  sumeq1  15614  fsumsplit  15666  sumsplit  15693  fsum2dlem  15695  fsumcom2  15699  fsumparts  15731  explecnv  15790  pwdif  15793  fprodser  15874  fprodsplit  15891  fprod2dlem  15905  fprodcom2  15909  eftlub  16036  divalgmod  16335  bitsval  16353  bitsp1e  16361  bitsp1o  16362  sadfval  16381  sadcp1  16384  sadval  16385  sadcadd  16387  sadadd2  16389  saddisjlem  16393  sadadd  16396  sadass  16400  smufval  16406  smuval  16410  smuval2  16411  smupvallem  16412  smu01lem  16414  smueqlem  16419  smumul  16422  bezoutlem2  16469  bezoutlem4  16471  algfx  16509  eucalgcvga  16515  reumodprminv  16734  nnnn0modprm0  16736  unbenlem  16838  prmreclem5  16850  vdwapval  16903  vdwapun  16904  vdwnnlem1  16925  vdwnn  16928  ramval  16938  0ram  16950  ramub1lem2  16957  prmgaplem7  16987  prmlem0  17035  elrest  17349  prdsbasmpt  17392  prdsleval  17399  prdsbasmpt2  17404  pwselbasb  17410  imasaddfnlem  17450  imasvscafn  17459  divsfval  17469  ismre  17510  mreunirn  17521  mrisval  17554  ismri  17555  isacs  17575  catidd  17604  iscatd2  17605  ismon  17658  isepi  17665  sectffval  17675  sectfval  17676  dfiso2  17697  cicsym  17729  issubc  17760  catsubcat  17764  isfunc  17789  funcres  17821  funcpropd  17827  ffthiso  17856  isnat  17875  isnat2  17876  fuciso  17903  initoval  17918  termoval  17919  isinito  17921  istermo  17922  iszeroo  17923  isinitoi  17924  istermoi  17925  initoid  17926  termoid  17927  iszeroi  17934  2initoinv  17935  initoeu1  17936  initoeu2  17941  2termoinv  17942  termoeu1  17943  arwhoma  17970  elsetchom  18006  setcmon  18012  setcepi  18013  setciso  18016  catciso  18036  elestrchom  18052  estrcbasbas  18055  funcestrcsetclem7  18070  funcestrcsetclem8  18071  funcestrcsetclem9  18072  fthestrcsetc  18074  fullestrcsetc  18075  equivestrcsetc  18076  setc1strwun  18077  funcsetcestrclem7  18085  funcsetcestrclem8  18086  funcsetcestrclem9  18087  fthsetcestrc  18089  fullsetcestrc  18090  hofcl  18183  hofpropd  18191  yonedalem4c  18201  yonedainv  18205  yonffthlem  18206  lubeldm  18275  glbeldm  18288  joindef  18298  meetdef  18312  poslubdg  18336  acsficl2d  18476  acsmapd  18478  psref  18498  psss  18504  dirge  18527  mgmpropd  18543  issstrmgm  18545  grpidval  18553  grpidpropd  18554  grpidd  18563  ismgmhm  18588  issubmgm  18594  issgrpd  18622  sgrppropd  18623  ismndd  18648  mndpropd  18651  imasmnd2  18666  imasmnd  18667  xpsmnd0  18670  ismhm  18677  issubm  18695  gsumsgrpccat  18732  elefmndbas2  18766  smndex1mndlem  18801  imasgrp2  18952  imasgrp  18953  issubg  19023  subginv  19030  isnsg  19052  eqg0el  19080  quselbas  19081  isghm  19112  isghmOLD  19113  resghm2b  19131  conjnmzb  19150  conjnsg  19151  ghmpropd  19153  isga  19188  elcntz  19219  elcntzsn  19222  cntzrcl  19224  resscntz  19230  symgextf1  19318  gsmsymgreqlem2  19328  f1otrspeq  19344  pmtrfrn  19355  pmtrdifellem3  19375  pmtrdifellem4  19376  psgnunilem1  19390  psgnunilem5  19391  psgnunilem2  19392  psgnunilem3  19393  psgneldm2  19401  psgnfitr  19414  psgnsn  19417  gexdvds  19481  gex1  19488  isslw  19505  sylow3lem2  19525  lsmelvalx  19537  pj1ghm  19600  efgtlen  19623  efgsfo  19636  efgredlemc  19642  frgp0  19657  frgpmhm  19662  qusabl  19762  frgpnabllem1  19770  imasabl  19773  cycsubmcmn  19786  0cyg  19790  cycsubgcyg  19798  gsumval3  19804  gsumcllem  19805  gsumzaddlem  19818  gsumzsplit  19824  gsummptfzcl  19866  eldprd  19903  dprdcntz2  19937  dprd2d2  19943  dmdprdsplit2lem  19944  dmdprdsplit2  19945  dprdsplit  19947  ablfac2  19988  isrngd  20076  rngpropd  20077  imasrng  20080  qusrng  20083  ringurd  20088  isringd  20194  imasring  20233  xpsring1d  20236  dvdsrval  20264  isunit  20276  dvdsrpropd  20319  isirred  20322  isrnghm  20344  isrngim  20348  c0ghm  20364  c0snghm  20367  isrhm  20381  isrim0OLD  20384  isrim0  20386  islring  20443  issubrng  20450  opprsubrng  20462  issubrg  20474  opprsubrg  20496  resrhm2b  20505  rhmpropd  20512  rnghmresel  20523  elrngchom  20527  rnghmsubcsetclem1  20534  rnghmsubcsetclem2  20535  rngcid  20538  rngcsect  20539  rngciso  20541  funcrngcsetcALT  20544  zrinitorngc  20545  zrtermorngc  20546  rhmresel  20552  elringchom  20556  rhmsubcsetclem1  20563  rhmsubcsetclem2  20564  ringcid  20567  rhmsscrnghm  20568  rhmsubcrngclem1  20569  rhmsubcrngclem2  20570  ringcsect  20573  ringciso  20575  ringcbasbas  20576  zrtermoringc  20578  srhmsubc  20583  rhmsubclem3  20590  rhmsubclem4  20591  drngunit  20637  isdrngd  20668  isdrngdOLD  20670  issdrg  20691  sdrgunit  20699  isabv  20714  issrngd  20758  islmod  20785  lmodprop2d  20845  islss  20855  islssd  20856  lssats2  20921  ellspsn  20924  islmhm  20949  lmhmf1o  20968  lmhmima  20969  lmhmpreima  20970  reslmhm  20974  pwssplit3  20983  lmhmpropd  20995  islbs  20998  lspprel  21016  lspfixed  21053  lbsacsbs  21081  lbsextlem1  21083  lbsextlem2  21084  lbsextlem3  21085  lbsextlem4  21086  ixpsnbasval  21130  isridlrng  21144  rnglidlmmgm  21170  isridl  21177  quscrng  21208  rngqiprngimfolem  21215  rngqiprngimf1lem  21219  rngqiprngimfo  21226  islpidl  21250  lidldvgen  21259  irinitoringc  21404  pzriprnglem13  21418  pzriprnglem14  21419  zrhrhmb  21435  znf1o  21476  frgpcyg  21498  psgnevpmb  21512  isphld  21579  phlssphl  21584  elocv  21593  iscss  21608  isobs  21645  obs2ss  21654  dsmmfi  21663  dsmmelbas  21664  dsmmlss  21669  frlmelbas  21681  frlmlbs  21722  frlmup1  21723  ellspd  21727  islinds  21734  islindf2  21739  f1lindf  21747  islindf4  21763  assamulgscmlem2  21825  psrgrp  21881  mplsubglem  21924  mpllsslem  21925  mplmonmul  21959  subrgascl  21989  subrgasclcl  21990  mpfind  22030  ismhp  22043  gsumply1subr  22134  lply1binomsc  22214  matbas2d  22326  matecl  22328  matvscl  22334  mat1  22350  mat0dim0  22370  mat0dimid  22371  mat0dimscm  22372  mat1dimelbas  22374  dmatel  22396  scmatel  22408  scmateALT  22415  scmataddcl  22419  scmatsubcl  22420  smatvscl  22427  scmatghm  22436  mat1scmat  22442  mdetunilem7  22521  mdetunilem9  22523  smadiadetr  22578  cramerimplem2  22587  cramer0  22593  pmatcoe1fsupp  22604  cpmatpmat  22613  cpmatel  22614  cpmatacl  22619  cpmatinvcl  22620  mat2pmatghm  22633  mat2pmatmul  22634  decpmatmullem  22674  pmatcollpwlem  22683  pmatcollpw3fi1lem1  22689  pmatcollpwscmatlem1  22692  monmat2matmon  22727  chfacfscmul0  22761  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  cayhamlem1  22769  cpmadugsumlemB  22777  cpmadugsumlemC  22778  cpmadugsumlemF  22779  cayhamlem2  22787  istopon  22815  eltg  22860  eltg2  22861  eltop  22877  eltop2  22878  eltop3  22879  pptbas  22911  iscld  22930  neiss2  23004  isnei  23006  neiptopnei  23035  neiptopreu  23036  lpfval  23041  lpval  23042  islp  23043  maxlp  23050  islpi  23052  neitr  23083  restlp  23086  ordtbas2  23094  ordtrest2  23107  lmfval  23135  cnfval  23136  iscn  23138  iscnp  23140  tgcn  23155  tgcnp  23156  lmbrf  23163  cnpresti  23191  ist1  23224  ist1-2  23250  cnt1  23253  haust1  23255  cmpfi  23311  cmpfii  23312  1stcfb  23348  2ndc1stc  23354  1stcrest  23356  2ndcdisj  23359  1stcelcls  23364  nllyi  23378  subislly  23384  islocfin  23420  lfinpfin  23427  locfindis  23433  locfincf  23434  comppfsc  23435  kgenval  23438  elkgen  23439  kgencn2  23460  txbas  23470  eltx  23471  ptval  23473  ptpjpre1  23474  ptopn2  23487  ptpjopn  23515  ptclsg  23518  xkoccn  23522  txdis  23535  txdis1cn  23538  ptrescn  23542  hausdiag  23548  hauseqlcld  23549  txhaus  23550  xkohaus  23556  elqtop  23600  qtopeu  23619  kqcldsat  23636  hmeofval  23661  ptuncnv  23710  ptunhmeo  23711  elmptrab  23730  fbdmn0  23737  elfg  23774  elfilss  23779  filunirn  23785  fixufil  23825  elfm  23850  rnelfmlem  23855  rnelfm  23856  fmfnfmlem4  23860  elflim2  23867  flimtopon  23873  elflim  23874  hausflim  23884  flimcls  23888  flfnei  23894  isflf  23896  hausflf  23900  cnpflf  23904  cnflf  23905  txflf  23909  isfcls  23912  fclstopon  23915  isfcls2  23916  fclssscls  23921  fclsnei  23922  fclsfnflim  23930  flimfnfcls  23931  isfcf  23937  fcfelbas  23939  cnpfcf  23944  cnfcf  23945  flfcntr  23946  alexsublem  23947  alexsubALTlem3  23952  cnextfun  23967  cnextfvval  23968  cnextf  23969  cnextcn  23970  tmdgsum2  23999  tgpconncomp  24016  ghmcnp  24018  qustgplem  24024  eltsms  24036  haustsms  24039  tsmsgsum  24042  tsmssubm  24046  tsmssplit  24055  isust  24107  ustbas  24131  elutop  24137  ustuqtoplem  24143  ustuqtop4  24148  ustuqtop  24150  utopsnneiplem  24151  utopsnneip  24152  utopsnnei  24153  isusp  24165  isucn  24181  ucncn  24188  iscfilu  24191  neipcfilu  24199  iscusp  24202  cnextucn  24206  ispsmet  24208  ismet  24227  isxmet  24228  elblps  24291  elbl  24292  elmopn  24346  prdsbl  24395  neibl  24405  met1stc  24425  metrest  24428  prdsxmslem2  24433  txmetcnp  24451  txmetcn  24452  metustsym  24459  cfilucfil2  24465  elbl4  24467  metuel  24468  psmetutop  24471  restmetu  24474  metucn  24475  tngngp  24558  isnmhm  24650  zcld  24718  metnrmlem1a  24763  elcncf  24798  cncfcnvcn  24835  cnheibor  24870  lebnumlem1  24876  ishtpy  24887  isphtpy  24896  om1elbas  24948  elpi1  24961  pi1xfr  24971  pi1coghm  24977  tcphcph  25153  lmmbrf  25178  iscfil  25181  iscau  25192  iscauf  25196  caucfil  25199  iscmet  25200  cmetcaulem  25204  iscmet3lem1  25207  iscmet3lem2  25208  iscmet3  25209  bcthlem1  25240  cmsss  25267  cmetcusp1  25269  cmetcusp  25270  cmscsscms  25289  rrxcph  25308  minveclem3b  25344  ovolfioo  25384  ovolficc  25385  ovolctb  25407  ovoliunnul  25424  ovolshftlem1  25426  sca2rab  25429  ovolscalem1  25430  ovolicc2lem1  25434  ovolicc2lem2  25435  ovolicc2lem4  25437  ovolicc2lem5  25438  iundisj  25465  iunmbl2  25474  uniioombllem3  25502  vitalilem2  25526  vitalilem3  25527  mbfss  25563  i1faddlem  25610  i1fmullem  25611  mbfi1fseqlem2  25633  mbfi1fseqlem4  25635  mbfi1fseq  25638  itg2splitlem  25665  itg2split  25666  itg2monolem1  25667  itg2gt0  25677  isibl  25682  iblss2  25723  itgss3  25732  itgsplit  25753  ellimc  25790  limcmo  25799  cnlimc  25805  limciun  25811  limcun  25812  eldv  25815  dvbsss  25819  dvreslem  25826  elcpn  25852  dvaddf  25861  dvmulf  25862  dvcof  25868  rolle  25910  dvlip2  25916  dvivthlem1  25929  lhop1  25935  lhop2  25936  ftc1cn  25966  fta1glem2  26090  plyco0  26113  elply  26116  ply1termlem  26124  eltayl  26283  tayl0  26285  taylplem1  26286  taylplem2  26287  dvtaylp  26294  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  abelth  26367  cxpcn3  26674  rlimcnp  26891  fsumharmonic  26938  dchrelbas  27163  pntrsumbnd2  27494  ostth2lem2  27561  nolesgn2ores  27600  nogesgn1ores  27602  nosupprefixmo  27628  noinfprefixmo  27629  nosupcbv  27630  nosupdm  27632  nosupfv  27634  nosupres  27635  nosupbnd1lem1  27636  nosupbnd1lem3  27638  nosupbnd1lem5  27640  nosupbnd2lem1  27643  noinfcbv  27645  noinfdm  27647  noinffv  27649  noinfres  27650  noinfbnd1lem1  27651  noinfbnd1lem3  27653  noinfbnd1lem5  27655  noinfbnd2lem1  27658  elmade  27799  elold  27801  ssltleft  27802  ssltright  27803  oldlim  27819  madebday  27832  newbday  27834  sltlpss  27840  bdayiun  27847  cofcutr  27855  cofcutrtime  27858  lrrecval  27869  lrrecval2  27870  addsval  27892  precsexlem9  28140  precsexlem11  28142  sltonold  28185  onnolt  28190  onslt  28191  noseqrdgfn  28223  istrkgb  28418  istrkgcb  28419  istrkge  28420  istrkgl  28421  istrkgld  28422  axtgsegcon  28427  axtg5seg  28428  axtgbtwnid  28429  axtgpasch  28430  axtgupdim2  28434  axtgeucl  28435  tgdim01  28470  iscgrg  28475  isismt  28497  tglnunirn  28511  tglngval  28514  tgellng  28516  legval  28547  legov  28548  legov2  28549  ishlg  28565  mirreu3  28617  mirval  28618  mirfv  28619  mircgr  28620  mirbtwn  28621  ismir  28622  mireq  28628  symquadlem  28652  israg  28660  perpln1  28673  perpln2  28674  isperp  28675  islnopp  28702  outpasch  28718  ishpg  28722  iscgra  28772  dfcgra2  28793  isinag  28801  isleag  28810  iseqlg  28830  f1otrgitv  28833  f1otrg  28834  f1otrge  28835  ttgval  28838  ttgelitv  28846  elee  28857  brbtwn  28862  brcgr  28863  axlowdimlem16  28920  ebtwntg  28945  elntg2  28948  upgrex  29055  edgupgr  29097  upgredg  29100  edglnl  29106  numedglnl  29107  uhgr2edg  29171  umgr2edg1  29174  usgredg2vlem1  29188  usgredg2vlem2  29189  ushgredgedg  29192  ushgredgedgloop  29194  uhgrspansubgrlem  29253  fusgrfisstep  29292  nbgrval  29299  nbgrel  29303  nbupgrel  29308  nbgr2vtx1edg  29313  nbuhgr2vtx1edgblem  29314  nbuhgr2vtx1edgb  29315  nbusgreledg  29316  usgrnbcnvfv  29328  uvtxval  29350  uvtxel  29351  uvtx01vtx  29360  uvtxusgrel  29366  nbcplgr  29397  cplgr3v  29398  cusgrexi  29406  structtocusgr  29409  vtxdgfval  29431  vtxdg0v  29437  vtxdeqd  29441  vtxdun  29445  1loopgrnb0  29466  1loopgrvd0  29468  1hevtxdg0  29469  1hevtxdg1  29470  1egrvtxdg1  29473  umgr2v2evtxel  29486  umgr2v2enb1  29490  umgr2v2evd2  29491  vtxdginducedm1lem4  29506  vtxdginducedm1  29507  finsumvtxdg2sstep  29513  ewlksfval  29565  isewlk  29566  wksfval  29573  iswlk  29574  uspgr2wlkeq  29609  wlkres  29632  dfpth2  29692  usgr2pthlem  29726  clwlkcompim  29743  uspgrn2crct  29771  wwlks  29798  iswwlksn  29801  wwlknvtx  29808  wlkiswwlks2  29838  wwlksm1edg  29844  wwlksnred  29855  wwlksnext  29856  wwlksnredwwlkn  29858  wwlksnredwwlkn0  29859  wwlksnwwlksnon  29878  wspn0  29887  usgr2wspthons3  29927  rusgrnumwwlkb0  29934  clwwlk  29945  clwwlkccatlem  29951  clwlkclwwlklem2a4  29959  clwlkclwwlk  29964  clwwisshclwwslem  29976  clwwlkinwwlk  30002  clwwlkel  30008  clwwlkf  30009  clwwlkext2edg  30018  wwlksext2clwwlk  30019  wwlksubclwwlk  30020  clwwnisshclwwsn  30021  eleclclwwlknlem2  30023  erclwwlknsym  30032  erclwwlkntr  30033  umgrhashecclwwlk  30040  clwwlkvbij  30075  eupth2lem3lem3  30192  eupth2lem3lem4  30193  eupth2lem3lem6  30195  eupth2lemb  30199  eucrct2eupth  30207  fusgreg2wsplem  30295  2clwwlklem  30305  2clwwlk2clwwlklem  30308  2clwwlkel  30311  2clwwlk2clwwlk  30312  extwwlkfabel  30315  clwwlknonclwlknonf1o  30324  dlwwlknondlwlknonf1olem1  30326  numclwwlk2lem1  30338  numclwlk2lem2f  30339  numclwlk2lem2f1o  30341  ex-res  30403  isssp  30686  sspn  30698  islno  30715  isblo  30744  nmlno0  30757  ishmo  30773  dipdir  30804  dipass  30807  ubthlem1  30832  ubthlem2  30833  htthlem  30879  htth  30880  ocel  31243  ocnel  31260  shsel  31276  shsel2  31284  shmodsi  31351  pjhtheu  31356  pjeq  31361  axpjpj  31382  pjoc2  31401  elspani  31505  h1de2ctlem  31517  elspansn  31528  elspansn2  31529  elnlfn  31890  eleigvec  31919  riesz3i  32024  cbviunf  32517  iuneq12daf  32518  iunrdx  32525  iunrnmptss  32527  cbvdisjf  32533  disjorf  32541  disjabrex  32544  disjabrexf  32545  iundisjf  32551  disjrdx  32553  brab2d  32568  2ndresdju  32606  abfmpunirn  32609  abfmpeld  32611  abfmpel  32612  fmptcof2  32614  acunirnmpt2  32617  acunirnmpt2f  32618  aciunf1lem  32619  funcnvmpt  32624  suppss3  32680  fpwrelmap  32689  xrofsup  32723  iundisjfi  32752  eliccioo  32884  s3f1  32901  ccatf1  32903  ccatws1f1o  32906  swrdrn3  32910  ismnt  32938  mgcoval  32941  chnccats1  32970  gsummpt2co  33014  gsumpart  33023  gsumhashmul  33027  xrge0tsmsbi  33029  gsumwrd2dccatlem  33032  gsumwrd2dccat  33033  cycpmco2  33088  cyc3co2  33095  isfxp  33123  cntrval2  33126  inftmrel  33135  isinftm  33136  isslmd  33157  urpropd  33185  elrgspn  33199  erlval  33211  rlocval  33212  rloccring  33223  rloc1r  33225  domnpropd  33229  isdrng4  33247  fracfld  33260  resv1r  33290  ellspds  33318  ellpi  33323  lbslsp  33327  rhmimaidl  33382  isprmidl  33388  qsidomlem1  33402  qsidomlem2  33403  ismxidl  33412  crngmxidl  33419  drng0mxidl  33426  opprqus0g  33440  qsfld  33448  isrprm  33467  rsprprmprmidlb  33473  ressply1evls1  33513  ply1mulrtss  33529  dimpropd  33583  lbslsat  33591  extdg1id  33640  fldextrspunlsplem  33647  fldextrspunlsp  33648  elirng  33660  ply1annidllem  33670  constrsuc  33707  constrconj  33714  constrllcllem  33721  constrlccllem  33722  constrcccllem  33723  nn0constr  33730  smatrcl  33765  smatcl  33771  ist0cld  33802  txomap  33803  locfinreflem  33809  zarclsiin  33840  zart0  33848  rhmpreimacnlem  33853  metidval  33859  cnre2csqima  33880  ordtrest2NEW  33892  fmcncfil  33900  fsumcvg4  33919  ofcfval  34067  measvuni  34183  meascnbl  34188  faeval  34215  ismbfm  34220  elunirnmbfm  34221  imambfm  34232  elcarsg  34275  itgeq12dv  34296  issibf  34303  eulerpartlems  34330  eulerpartlemgc  34332  eulerpartlemgvv  34346  eulerpartlemgu  34347  eulerpart  34352  rrvmbfm  34412  elorvc  34430  elorrvc  34434  dstfrvunirn  34445  ballotlemfc0  34463  ballotlemfcc  34464  ballotlemsima  34486  ballotlemrv  34490  fzssfzo  34509  signstfvn  34539  signstfvneq0  34542  signstres  34545  repr0  34581  reprinrn  34588  reprdifc  34597  hgt750lemg  34624  hgt750lemb  34626  istrkg2d  34636  axtgupdim2ALTV  34638  afsval  34641  brafs  34642  bnj945  34742  bnj1400  34804  bnj18eq1  34896  bnj916  34902  bnj1014  34930  bnj1015  34931  bnj1110  34951  bnj1417  35010  onvf1odlem3  35080  vonf1owev  35083  revpfxsfxrev  35091  cplgredgex  35096  pfxwlk  35099  revwlk  35100  subfacp1lem2b  35156  subfacp1lem4  35158  subfacp1lem5  35159  subfacp1lem6  35160  ptpconn  35208  cvmscbv  35233  iscvm  35234  cvmsi  35240  cvmsval  35241  cvmliftmolem1  35256  cvmlift2lem12  35289  cvmlift2lem13  35290  cvmlift3lem7  35300  snmlval  35306  satfv1  35338  satfvsucsuc  35340  satfrnmapom  35345  satf0op  35352  satf0n0  35353  sat1el2xp  35354  fmlafvel  35360  isfmlasuc  35363  fmlaomn0  35365  gonan0  35367  goaln0  35368  gonar  35370  goalr  35372  satffunlem1lem2  35378  satffunlem2lem2  35381  satfv0fvfmla0  35388  satef  35391  satefvfmla0  35393  sategoelfvb  35394  satfv1fvfmla1  35398  mrsubfval  35483  mrsubvrs  35497  mclsrcl  35536  mclsval  35538  mppsval  35547  mclsppslem  35558  opelco3  35750  wsuclem  35801  funtransport  36007  fvtransport  36008  brcolinear  36035  colineardim1  36037  funray  36116  fvray  36117  funline  36118  fvline  36120  lineelsb2  36124  fwddifval  36138  fwddifnval  36139  rankelg  36144  rankeq1o  36147  elhf2  36151  0hf  36153  rmoeqbidv  36189  disjeq12dv  36191  ixpeq12dv  36192  prodeq12sdv  36194  itgeq12sdv  36195  cbvralvw2  36202  cbvrexvw2  36203  cbvrmovw2  36204  cbvreuvw2  36205  cbvcsbvw2  36207  cbviunvw2  36208  cbviinvw2  36209  cbvmptvw2  36210  cbvdisjvw2  36211  cbvmpo1vw2  36219  cbvmpo2vw2  36220  cbvsbcdavw  36233  cbvcsbdavw  36235  cbvcsbdavw2  36236  cbviundavw  36238  cbviindavw  36239  cbvdisjdavw  36244  cbvrabdavw2  36261  cbviundavw2  36262  cbviindavw2  36263  cbvmptdavw2  36264  cbvdisjdavw2  36265  cbvriotadavw2  36266  cbvmpo1davw2  36268  cbvmpo2davw2  36269  cbvsumdavw2  36271  neibastop2lem  36336  neibastop3  36338  eltail  36350  bj-projeq  36968  bj-projval  36972  bj-restsn  37058  opelopabbv  37119  brabd0  37123  bj-eldiag  37152  bj-eldiag2  37153  mptsnunlem  37314  dissneqlem  37316  iooelexlt  37338  relowlssretop  37339  rdgellim  37352  exrecfnlem  37355  finxpeq1  37362  finxpreclem6  37372  pibp21  37391  curf  37580  uncf  37581  curunc  37584  unccur  37585  fin2so  37589  lindsadd  37595  lindsdom  37596  lindsenlbs  37597  matunitlindflem1  37598  matunitlindflem2  37599  matunitlindf  37600  ptrest  37601  ptrecube  37602  poimirlem2  37604  poimirlem8  37610  poimirlem17  37619  poimirlem18  37620  poimirlem20  37622  poimirlem21  37623  poimirlem22  37624  poimirlem24  37626  poimirlem26  37628  poimirlem29  37631  heicant  37637  mblfinlem1  37639  mblfinlem2  37640  volsupnfl  37647  itg2addnclem  37653  itg2gt0cn  37657  indexdom  37716  incsequz  37730  istotbnd  37751  istotbnd3  37753  0totbnd  37755  sstotbnd  37757  sstotbnd3  37758  isbnd  37762  prdstotbnd  37776  cntotbnd  37778  isismty  37783  heibor1lem  37791  heiborlem2  37794  heiborlem3  37795  heibor  37803  isass  37828  exidcl  37858  exidreslem  37859  elghomlem2OLD  37868  rngoidmlem  37918  rngo1cl  37921  divrngcl  37939  isdrngo2  37940  isrngohom  37947  isrngoiso  37960  isriscg  37966  iscom2  37977  iscringd  37980  isidl  37996  ispridl  38016  ismaxidl  38022  ac6s6  38154  dmecd  38280  releldmqs  38638  releldmqscoss  38640  erimeq2  38658  eldisjlem19  38790  membpartlem19  38791  prter3  38863  islshp  38960  islsat  38972  lcvfbr  39001  islfl  39041  ellkr  39070  islshpkrN  39101  ldual1dim  39147  isopos  39161  cmtfvalN  39191  cvrfval  39249  isat  39267  islln  39488  islpln  39512  islvol  39555  isline  39721  ispointN  39724  ispsubsp  39727  elpmap  39740  elpmapat  39746  elpadd  39781  paddclN  39824  elpclN  39874  elpcliN  39875  pclfinN  39882  pclcmpatN  39883  ispsubclN  39919  iswatN  39976  islhp  39978  islaut  40065  ispautN  40081  isldil  40092  isltrn  40101  isdilN  40136  istrnN  40139  istendo  40742  dvhb1dimN  40968  erng1lem  40969  erngdvlem4-rN  40981  diaelval  41015  diaeldm  41018  dia1dimid  41045  cdlemm10N  41100  dibopelvalN  41125  dibopelval2  41127  dibelval3  41129  dibelval1st  41131  dibelval2nd  41134  dibeldmN  41140  dibvalrel  41145  dibglbN  41148  dicffval  41156  dicfval  41157  dicopelval  41159  dicelvalN  41160  dicelval3  41162  dicvalrelN  41167  dicelval1sta  41169  diclspsn  41176  dihopelvalbN  41220  dihopelvalcqat  41228  dihopelvalcpre  41230  dihvalrel  41261  dih1  41268  dihmeetlem4preN  41288  dihmeetlem13N  41301  dih1dimatlem  41311  dochnel2  41374  dihjatcclem4  41403  dvh2dim  41427  dvh3dim  41428  dvh4dimN  41429  dochfln0  41459  lpolsetN  41464  islpolN  41465  lcfrvalsnN  41523  lcfrlem21  41545  lcfrlem27  41551  lcfrlem37  41561  lcfr  41567  lcdlss  41601  mapdcv  41642  hdmap1fval  41778  hdmapffval  41808  hdmapfval  41809  hdmapval  41810  hgmapffval  41867  hgmapfval  41868  hdmapellkr  41896  hlhilhillem  41942  fzsplitnd  41958  isprimroot  42069  primrootsunit1  42073  primrootscoprmpow  42075  primrootscoprbij  42078  aks6d1c1p2  42085  aks6d1c1p3  42086  aks6d1c1p4  42087  aks6d1c1p5  42088  aks6d1c1p6  42090  aks6d1c1  42092  evl1gprodd  42093  sticksstones11  42132  sticksstones12a  42133  rhmqusspan  42161  grpods  42170  fzosumm1  42226  frlmfielbas  42476  frlmsnic  42516  psrmnd  42521  isnacs  42680  mrefg2  42683  elmzpcl  42702  mzpcompact2  42728  eldiophb  42733  elpell1qr  42823  elpell14qr  42825  elpell1234qr  42827  pw2f1ocnv  43013  pw2f1o2val2  43016  aomclem4  43033  aomclem6  43035  islssfg2  43047  imasgim  43076  lnr2i  43092  elmnc  43112  rngunsnply  43145  onexomgt  43217  onexlimgt  43219  onexoegt  43220  oaordnr  43272  omnord1  43281  oenord1  43292  cantnfresb  43300  tfsconcatun  43313  tfsconcat0i  43321  ofoaf  43331  naddcnff  43338  naddcnffo  43340  naddcnfcom  43342  naddcnfid1  43343  naddcnfid2  43344  naddcnfass  43345  naddwordnexlem4  43377  fiinfi  43549  sqrtcvallem1  43607  elintima  43629  eliunov2  43655  ov2ssiunov2  43676  brtrclfv2  43703  rfovcnvf1od  43980  rfovcnvfvd  43983  fsovrfovd  43985  fsovfvd  43986  fsovcnvlem  43989  ntrclsfv1  44031  ntrclselnel1  44033  ntrclsneine0lem  44040  ntrneifv1  44055  ntrneifv2  44056  ntrneiel  44057  gneispace2  44108  gneispacess2  44122  extoimad  44140  mnringelbased  44193  dvconstbi  44310  bccbc  44321  wfac8prim  44979  permaxrep  44983  permac8prim  44991  eliin2f  45085  iineq12dv  45087  rabbida2  45113  disjinfi  45173  unirnmap  45189  elmptima  45239  iuneqfzuzlem  45317  iooiinioc  45541  fsumiunss  45560  fsumsupp0  45563  lptre2pt  45625  icccncfext  45872  cncfiooicclem1  45878  dvnprodlem2  45932  stoweidlem27  46012  stoweidlem29  46014  stoweidlem31  46016  stoweidlem34  46019  stoweidlem48  46033  stoweidlem59  46044  dirkercncflem2  46089  dirkercncflem4  46091  fourierdlem2  46094  fourierdlem3  46095  fourierdlem25  46117  fourierdlem32  46124  fourierdlem33  46125  fourierdlem41  46133  fourierdlem48  46139  fourierdlem49  46140  fourierdlem62  46153  fourierdlem70  46161  fourierdlem80  46171  fourierdlem92  46183  fourierdlem93  46184  fourierdlem101  46192  etransclem37  46256  sge0val  46351  sge0f1o  46367  sge0iunmptlemre  46400  sge0iunmpt  46403  iundjiun  46445  caragenel  46480  ovncvrrp  46549  ovnsubaddlem1  46555  ovnsubadd  46557  hoidmvlelem2  46581  hoidmvlelem3  46582  hoidmvlelem4  46583  hoidmvle  46585  ovncvr2  46596  hspdifhsp  46601  hoiqssbl  46610  hspmbllem2  46612  hspmbl  46614  opnvonmbllem1  46617  isvonmbl  46623  ovnovollem1  46641  issmflem  46712  smflimlem3  46758  smflimlem4  46759  smflim  46762  smfmullem2  46777  smflimmpt  46795  smfsuplem1  46796  smflimsuplem1  46805  smflimsuplem3  46807  smflimsuplem4  46808  smflimsuplem7  46811  smflimsup  46813  tworepnotupword  46871  fcores  47055  fcoresf1  47057  afvelrnb  47151  afvelrnb0  47152  afv2co2  47245  el1fzopredsuc  47313  iccpart  47404  iccpartgtprec  47408  iccpartiltu  47410  iccpartigtl  47411  iccpartltu  47413  iccpartgtl  47414  iccpartgt  47415  iccpartleu  47416  iccpartgel  47417  iccelpart  47421  iccpartiun  47422  icceuelpart  47424  fargshiftfv  47427  fargshiftfo  47430  sprel  47472  prprelb  47504  prprelprb  47505  fpprel  47716  sbgoldbo  47775  wtgoldbnnsum4prm  47790  bgoldbnnsum3prm  47792  bgoldbtbndlem3  47795  bgoldbtbnd  47797  clnbgrval  47810  elclnbgrelnbgr  47813  clnbgrel  47816  clnbupgrel  47822  vopnbgrel  47842  isubgredg  47854  upgrimwlklem3  47887  upgrimwlklem5  47889  upgrimpths  47897  grtriprop  47929  isgrtri  47931  grtriclwlk3  47933  stgredgel  47945  gpgvtxel  48035  gpgiedgdmel  48037  gpgedgel  48038  opgpgvtx  48043  gpg5nbgrvtx13starlem1  48059  gpg5nbgrvtx13starlem2  48060  gpg5nbgrvtx13starlem3  48061  gpg3kgrtriex  48077  grlimedgnedg  48119  upwlksfval  48123  isupwlk  48124  intop  48191  isclintop  48195  assintop  48197  isassintop  48198  assintopcllaw  48200  uzlidlring  48223  elrngchomALTV  48257  rngccatidALTV  48260  rngcsectALTV  48263  rngcisoALTV  48265  rhmsubcALTVlem3  48271  rhmsubcALTVlem4  48272  funcringcsetcALTV2lem7  48284  funcringcsetcALTV2lem9  48286  elringchomALTV  48291  ringccatidALTV  48294  ringcsectALTV  48297  ringcisoALTV  48299  ringcbasbasALTV  48300  funcringcsetclem7ALTV  48307  funcringcsetclem9ALTV  48309  srhmsubcALTV  48313  cbvmpox2  48324  ply1sclrmsm  48372  dmatALTbasel  48391  lcoval  48401  lindslinindsimp1  48446  lindslinindsimp2  48452  lmod1  48481  elbigo  48540  elbigo2  48541  elbigolo1  48546  dig2nn0ld  48593  naryfvalel  48619  rrxlines  48722  rrxlinesc  48724  rrxlinec  48725  eenglngeehlnm  48728  elrrx2linest2  48734  rrxsphere  48737  itsclc0  48760  itsclc0b  48761  itsclinecirc0  48762  itsclinecirc0b  48763  itscnhlinecirc02p  48774  brab2dd  48816  f1omo  48881  f1omoOLD  48882  lubeldm2d  48946  glbeldm2d  48947  catprs  49000  sectpropdlem  49025  nelsubc3lem  49059  initc  49080  imaid  49143  upfval  49165  upfval2  49166  upfval3  49167  uppropd  49170  oppcinito  49224  oppctermo  49225  oppczeroo  49226  initopropd  49232  termopropd  49233  isthinc  49408  isthincd2lem1  49414  thincmoALT  49418  thincmod  49419  isthincd  49425  thincpropd  49431  indcthing  49449  discthing  49450  prsthinc  49453  termcterm  49502  termc2  49507  isinito4  49536  2arwcatlem1  49584  setc1onsubc  49591  cnelsubclem  49592  ranval3  49620  lmdfval2  49644  cmdfval2  49645  termolmd  49659  elsetrecslem  49688