Theorem eleq2d 2848

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 2755	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	sylib 220	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		anbi2 643	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1853	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 17	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		dfclel 2838	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		dfclel 2838	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4g 316	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1558   = wceq 1560  ∃wex 1799   ∈ wcel 2142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837

This theorem is referenced by:  eleq2  2851  eleq12d  2856  eleqtrd  2864  neleqtrd  2884  eqabrd  2903  raleqbidv  3336  rexeqbidv  3337  reueqbidv  3403  rabeqbidva  3430  elabd2  3629  sbcbid  3798  sbcbi2  3802  csbeq2d  3858  csbeq2dv  3859  cbvcsbw  3862  cbvcsb  3863  cbvcsbv  3864  csbie  3887  csbied  3888  csbie2g  3892  cbvralcsf  3894  cbvreucsf  3896  cbvrabcsf  3897  sbcel12  4365  sbcel1g  4370  sbcel2  4372  prel12g  4822  eliuni  4955  iuneqconst  4961  iuneq12df  4976  iuneq12d  4979  cbviun  4992  cbviin  4993  cbviung  4994  cbviing  4995  cbviunv  4996  cbviinv  4997  iinxsng  5045  iinxprg  5046  iunxsng  5047  iunxsngf  5049  cbvdisj  5077  cbvdisjv  5078  disjor  5082  disjiund  5091  mpteq12da  5183  mpteq12f  5185  mpteq12dva  5186  axpweq  5307  rabxfrd  5374  brab2d  5508  rbropapd  5533  opeliunxp  5714  opeliun2xp  5715  opeliunxp2  5810  iunxpf  5820  elimampt  6032  elrelimasn  6075  elimasni  6080  imadifssran  6136  xpdifid  6153  xpdifcnvepel  6154  ressn  6272  funfni  6627  fnbr  6629  dffv3  6863  elfv2ex  6910  fvelrnb  6927  foelcdmi  6928  fvun1  6958  fvco2  6964  funcnvmpt  6977  elfvmptrab1w  7003  elfvmptrab1  7004  elfvmptrab  7005  elpreima  7039  dff3  7081  fmptco  7111  fnelfp  7159  fnelnfp  7161  tpres  7185  fnprb  7192  fntpb  7193  funfvima3  7220  eluniima  7234  dff13  7238  f1ounsn  7256  f1eqcocnv  7285  isoini  7322  riotaeqdv  7354  mpoeq123dva  7470  cbvmpox  7489  elimampo  7533  ovelrn  7572  elovmpod  7640  elovmpo  7641  elovmporab  7642  elovmporab1w  7643  elovmporab1  7644  elovmpt3rab1  7656  fiun  7924  f1iun  7925  zfrep6OLD  7936  fmpox  8048  el2mpocsbcl  8064  el2mpocl  8065  bropopvvv  8069  bropfvvvv  8071  xpord2indlem  8127  xpord3inddlem  8134  elsuppfng  8149  elsuppfn  8150  suppfnss  8169  opeliunxp2f  8190  mpoxopn0yelv  8193  mpoxopovel  8200  rntpos  8219  mpocurryd  8249  fpr2  8285  wfr2  8308  onoviun  8314  smoel  8331  smoiso  8333  smoel2  8334  smo11  8335  tfrlem9  8356  oalimcl  8529  oaass  8530  omordi  8535  omordlim  8546  omlimcl  8547  odi  8548  omeulem1  8551  omeulem2  8552  oen0  8556  oeordi  8557  oeordsuc  8564  oelimcl  8570  oeeulem  8571  oeeui  8572  nnmordi  8601  oaabs2  8619  omabs  8621  omsmolem  8627  ereldm  8732  iiner  8771  elmapg  8820  elpmg  8824  elixpsn  8919  ixpsnf1o  8920  boxriin  8922  omxpenlem  9050  pw2f1olem  9053  phplem2  9173  php3  9177  infn0  9246  elfi  9359  dffi3  9377  marypha2lem2  9382  ordiso2  9463  wemapsolem  9498  elharval  9509  inf3lemd  9582  inf3lem1  9583  inf3lem2  9584  inf3lem3  9585  cantnfs  9621  cantnfp1lem3  9635  cantnflem1b  9641  cantnflem1  9644  ttrclselem2  9681  trcl  9683  frr2  9718  r1sdom  9732  r1ordg  9736  r1pwss  9742  tz9.12lem3  9747  tz9.12  9748  r1elwf  9754  rankr1ai  9756  rankidb  9758  rankr1bg  9761  rankval2  9776  rankunb  9808  tcrank  9842  acni  10001  acni2  10002  acndom  10007  infpwfien  10018  alephnbtwn  10027  cardaleph  10045  cardinfima  10053  iunfictbso  10070  dfac3  10077  dfac5lem5  10083  dfac5  10085  dfac9  10093  dfac12r  10103  kmlem2  10108  kmlem12  10118  kmlem13  10119  kmlem14  10120  ackbij2lem3  10196  ackbij2  10198  cofsmo  10226  alephsing  10233  fin23lem30  10299  isf32lem9  10318  itunisuc  10376  axcc2lem  10393  axcc3  10395  domtriomlem  10399  axdc2lem  10405  axdc2  10406  axdc3lem2  10408  axdc3lem4  10410  axdc4lem  10412  ac6c4  10438  zorn2lem1  10453  ttukeylem6  10471  pwcfsdom  10541  axregndlem2  10561  axinfndlem1  10563  axacndlem4  10568  axacnd  10570  pwfseqlem1  10616  inar1  10733  inatsk  10736  gruurn  10756  grur1  10778  eltskm  10801  genpelv  10958  eluz1  12843  elixx1  13358  elixx3g  13362  elioo2  13390  elfz1  13517  elfz2  13519  elfzp1  13579  fzpr  13584  fzsuc2  13587  fzrev3  13595  elfzp12  13608  fzm1  13612  elfzo  13666  fz0add1fz1  13741  elfzo0l  13762  elfzom1b  13772  fzosplitsni  13785  elfzr  13787  elfzlmr  13788  zmodidfzo  13910  seqp1  14029  seqf1o  14056  bcval  14317  bcpasc  14334  hashf1lem1  14468  fundmge2nop0  14515  wrdmap  14559  elovmpowrd  14571  ccatfval  14586  elfzelfzccat  14593  ccatlid  14600  ccatass  14602  ccatrn  14603  ccatalpha  14607  swrdfv2  14675  ccatswrd  14682  swrdccat2  14683  pfxfv  14696  pfxeq  14709  ccatpfx  14714  swrdswrd  14718  swrdpfx  14720  pfxpfx  14721  cats1un  14734  swrdccatfn  14737  swrdccatin1  14738  pfxccatin12lem4  14739  pfxccatin12lem1  14741  swrdccatin2  14742  pfxccatin12lem2c  14743  pfxccatin12lem2  14744  swrdccat3blem  14752  swrdccatin1d  14756  swrdccatin2d  14757  pfxccatin12d  14758  revccat  14779  revrev  14780  repswpfx  14798  repswccat  14799  cshwidxmod  14816  2cshw  14826  cshwcshid  14840  cshwcsh2id  14841  cshimadifsn  14842  cshimadifsn0  14843  revco  14847  ccatco  14848  cshco  14849  swrdco  14850  ofccat  14982  shftfn  15086  shftval  15087  limsupgle  15504  ello12  15543  elo12  15554  isercolllem3  15694  sumeq1  15716  fsumsplit  15768  sumsplit  15795  fsum2dlem  15797  fsumcom2  15801  fsumparts  15834  explecnv  15895  pwdif  15898  fprodser  15979  fprodsplit  15996  fprod2dlem  16010  fprodcom2  16014  eftlub  16141  divalgmod  16440  bitsval  16458  bitsp1e  16466  bitsp1o  16467  sadfval  16486  sadcp1  16489  sadval  16490  sadcadd  16492  sadadd2  16494  saddisjlem  16498  sadadd  16501  sadass  16505  smufval  16511  smuval  16515  smuval2  16516  smupvallem  16517  smu01lem  16519  smueqlem  16524  smumul  16527  bezoutlem2  16574  bezoutlem4  16576  algfx  16614  eucalgcvga  16620  reumodprminv  16840  nnnn0modprm0  16842  unbenlem  16944  prmreclem5  16956  vdwapval  17009  vdwapun  17010  vdwnnlem1  17031  vdwnn  17034  ramval  17044  0ram  17056  ramub1lem2  17063  prmgaplem7  17093  prmlem0  17141  elrest  17456  prdsbasmpt  17499  prdsleval  17506  prdsbasmpt2  17511  pwselbasb  17517  imasaddfnlem  17558  imasvscafn  17567  divsfval  17577  ismre  17618  mreunirn  17629  mrisval  17662  ismri  17663  isacs  17683  catidd  17712  iscatd2  17713  ismon  17766  isepi  17773  sectffval  17783  sectfval  17784  dfiso2  17805  cicsym  17837  issubc  17868  catsubcat  17872  isfunc  17897  funcres  17929  funcpropd  17935  ffthiso  17964  isnat  17983  isnat2  17984  fuciso  18011  initoval  18026  termoval  18027  isinito  18029  istermo  18030  iszeroo  18031  isinitoi  18032  istermoi  18033  initoid  18034  termoid  18035  iszeroi  18042  2initoinv  18043  initoeu1  18044  initoeu2  18049  2termoinv  18050  termoeu1  18051  arwhoma  18078  elsetchom  18114  setcmon  18120  setcepi  18121  setciso  18124  catciso  18144  elestrchom  18160  estrcbasbas  18163  funcestrcsetclem7  18178  funcestrcsetclem8  18179  funcestrcsetclem9  18180  fthestrcsetc  18182  fullestrcsetc  18183  equivestrcsetc  18184  setc1strwun  18185  funcsetcestrclem7  18193  funcsetcestrclem8  18194  funcsetcestrclem9  18195  fthsetcestrc  18197  fullsetcestrc  18198  hofcl  18291  hofpropd  18299  yonedalem4c  18309  yonedainv  18313  yonffthlem  18314  lubeldm  18383  glbeldm  18396  joindef  18406  meetdef  18420  poslubdg  18444  acsficl2d  18584  acsmapd  18586  psref  18606  psss  18612  dirge  18635  chnccats1  18657  chnccat  18658  chnrev  18659  mgmpropd  18685  issstrmgm  18687  grpidval  18695  grpidpropd  18696  grpidd  18705  ismgmhm  18730  issubmgm  18736  issgrpd  18764  sgrppropd  18765  ismndd  18790  mndpropd  18793  imasmnd2  18808  imasmnd  18809  xpsmnd0  18812  ismhm  18819  issubm  18837  gsumsgrpccat  18874  elefmndbas2  18908  smndex1mndlem  18946  imasgrp2  19097  imasgrp  19098  issubg  19168  subginv  19175  isnsg  19196  eqg0el  19224  quselbas  19225  isghm  19256  resghm2b  19274  conjnmzb  19293  conjnsg  19294  ghmpropd  19296  isga  19331  elcntz  19362  elcntzsn  19365  cntzrcl  19367  resscntz  19373  symgextf1  19461  gsmsymgreqlem2  19471  f1otrspeq  19487  pmtrfrn  19498  pmtrdifellem3  19518  pmtrdifellem4  19519  psgnunilem1  19533  psgnunilem5  19534  psgnunilem2  19535  psgnunilem3  19536  psgneldm2  19544  psgnfitr  19557  psgnsn  19560  gexdvds  19624  gex1  19631  isslw  19648  sylow3lem2  19668  lsmelvalx  19680  pj1ghm  19743  efgtlen  19766  efgsfo  19779  efgredlemc  19785  frgp0  19800  frgpmhm  19805  qusabl  19905  frgpnabllem1  19913  imasabl  19916  cycsubmcmn  19929  0cyg  19933  cycsubgcyg  19941  gsumval3  19947  gsumcllem  19948  gsumzaddlem  19961  gsumzsplit  19967  gsummptfzcl  20009  eldprd  20046  dprdcntz2  20080  dprd2d2  20086  dmdprdsplit2lem  20087  dmdprdsplit2  20088  dprdsplit  20090  ablfac2  20131  isrngd  20219  rngpropd  20220  imasrng  20223  qusrng  20226  ringurd  20235  isringd  20341  imasring  20379  xpsring1d  20382  dvdsrval  20410  isunit  20422  dvdsrpropd  20465  isirred  20468  isrnghm  20490  isrngim  20494  c0ghm  20510  c0snghm  20513  isrhm  20527  isrim0  20531  islring  20590  issubrng  20597  opprsubrng  20609  issubrg  20621  opprsubrg  20643  resrhm2b  20652  rhmpropd  20659  rnghmresel  20670  elrngchom  20674  rnghmsubcsetclem1  20681  rnghmsubcsetclem2  20682  rngcid  20685  rngcsect  20686  rngciso  20688  funcrngcsetcALT  20691  zrinitorngc  20692  zrtermorngc  20693  rhmresel  20699  elringchom  20703  rhmsubcsetclem1  20710  rhmsubcsetclem2  20711  ringcid  20714  rhmsscrnghm  20715  rhmsubcrngclem1  20716  rhmsubcrngclem2  20717  ringcsect  20720  ringciso  20722  ringcbasbas  20723  zrtermoringc  20725  srhmsubc  20730  rhmsubclem3  20737  rhmsubclem4  20738  drngunit  20784  isdrngd  20815  isdrngdOLD  20817  issdrg  20837  sdrgunit  20845  isabv  20860  issrngd  20904  islmod  20931  lmodprop2d  20991  islss  21001  islssd  21002  lssats2  21067  ellspsn  21070  islmhm  21094  lmhmf1o  21113  lmhmima  21114  lmhmpreima  21115  reslmhm  21119  pwssplit3  21128  lmhmpropd  21140  islbs  21143  lspprel  21161  lspfixed  21198  lbsacsbs  21226  lbsextlem1  21228  lbsextlem2  21229  lbsextlem3  21230  lbsextlem4  21231  ixpsnbasval  21275  isridlrng  21289  rnglidlmmgm  21315  isridl  21322  quscrng  21353  rngqiprngimfolem  21360  rngqiprngimf1lem  21364  rngqiprngimfo  21371  islpidl  21395  lidldvgen  21404  irinitoringc  21531  pzriprnglem13  21545  pzriprnglem14  21546  zrhrhmb  21562  znf1o  21603  frgpcyg  21625  psgnevpmb  21639  isphld  21706  phlssphl  21711  elocv  21720  iscss  21735  isobs  21772  obs2ss  21781  dsmmfi  21790  dsmmelbas  21791  dsmmlss  21796  frlmelbas  21808  frlmlbs  21849  frlmup1  21850  ellspd  21854  islinds  21861  islindf2  21866  f1lindf  21874  islindf4  21890  assamulgscmlem2  21952  psrgrp  22008  mplsubglem  22050  mpllsslem  22051  mplmonmul  22089  subrgascl  22119  subrgasclcl  22120  mpfind  22168  ismhp  22205  gsumply1subr  22295  lply1binomsc  22374  matbas2d  22483  matecl  22485  matvscl  22491  mat1  22507  mat0dim0  22527  mat0dimid  22528  mat0dimscm  22529  mat1dimelbas  22531  dmatel  22553  scmatel  22565  scmateALT  22572  scmataddcl  22576  scmatsubcl  22577  smatvscl  22584  scmatghm  22593  mat1scmat  22599  mdetunilem7  22678  mdetunilem9  22680  smadiadetr  22735  cramerimplem2  22744  cramer0  22750  pmatcoe1fsupp  22761  cpmatpmat  22770  cpmatel  22771  cpmatacl  22776  cpmatinvcl  22777  mat2pmatghm  22790  mat2pmatmul  22791  decpmatmullem  22831  pmatcollpwlem  22840  pmatcollpw3fi1lem1  22846  pmatcollpwscmatlem1  22849  monmat2matmon  22884  chfacfscmul0  22918  chfacfscmulgsum  22920  chfacfpmmulgsum  22924  cayhamlem1  22926  cpmadugsumlemB  22934  cpmadugsumlemC  22935  cpmadugsumlemF  22936  cayhamlem2  22944  istopon  22972  eltg  23017  eltg2  23018  eltop  23034  eltop2  23035  eltop3  23036  pptbas  23068  iscld  23087  neiss2  23161  isnei  23163  neiptopnei  23192  neiptopreu  23193  lpfval  23198  lpval  23199  islp  23200  maxlp  23207  islpi  23209  neitr  23240  restlp  23243  ordtbas2  23251  ordtrest2  23264  lmfval  23292  cnfval  23293  iscn  23295  iscnp  23297  tgcn  23312  tgcnp  23313  lmbrf  23320  cnpresti  23348  ist1  23381  ist1-2  23407  cnt1  23410  haust1  23412  cmpfi  23468  cmpfii  23469  1stcfb  23505  2ndc1stc  23511  1stcrest  23513  2ndcdisj  23516  1stcelcls  23521  nllyi  23535  subislly  23541  islocfin  23577  lfinpfin  23584  locfindis  23590  locfincf  23591  comppfsc  23592  kgenval  23595  elkgen  23596  kgencn2  23617  txbas  23627  eltx  23628  ptval  23630  ptpjpre1  23631  ptopn2  23644  ptpjopn  23672  ptclsg  23675  xkoccn  23679  txdis  23692  txdis1cn  23695  ptrescn  23699  hausdiag  23705  hauseqlcld  23706  txhaus  23707  xkohaus  23713  elqtop  23757  qtopeu  23776  kqcldsat  23793  hmeofval  23818  ptuncnv  23867  ptunhmeo  23868  elmptrab  23887  fbdmn0  23894  elfg  23931  elfilss  23936  filunirn  23942  fixufil  23982  elfm  24007  rnelfmlem  24012  rnelfm  24013  fmfnfmlem4  24017  elflim2  24024  flimtopon  24030  elflim  24031  hausflim  24041  flimcls  24045  flfnei  24051  isflf  24053  hausflf  24057  cnpflf  24061  cnflf  24062  txflf  24066  isfcls  24069  fclstopon  24072  isfcls2  24073  fclssscls  24078  fclsnei  24079  fclsfnflim  24087  flimfnfcls  24088  isfcf  24094  fcfelbas  24096  cnpfcf  24101  cnfcf  24102  flfcntr  24103  alexsublem  24104  alexsubALTlem3  24109  cnextfun  24124  cnextfvval  24125  cnextf  24126  cnextcn  24127  tmdgsum2  24156  tgpconncomp  24173  ghmcnp  24175  qustgplem  24181  eltsms  24193  haustsms  24196  tsmsgsum  24199  tsmssubm  24203  tsmssplit  24212  isust  24264  ustbas  24287  elutop  24293  ustuqtoplem  24299  ustuqtop4  24304  ustuqtop  24306  utopsnneiplem  24307  utopsnneip  24308  utopsnnei  24309  isusp  24321  isucn  24337  ucncn  24344  iscfilu  24347  neipcfilu  24355  iscusp  24358  cnextucn  24362  ispsmet  24364  ismet  24383  isxmet  24384  elblps  24447  elbl  24448  elmopn  24502  prdsbl  24551  neibl  24561  met1stc  24581  metrest  24584  prdsxmslem2  24589  txmetcnp  24607  txmetcn  24608  metustsym  24615  cfilucfil2  24621  elbl4  24623  metuel  24624  psmetutop  24627  restmetu  24630  metucn  24631  tngngp  24714  isnmhm  24806  zcld  24874  metnrmlem1a  24919  elcncf  24951  cncfcnvcn  24987  cnheibor  25017  lebnumlem1  25023  ishtpy  25034  isphtpy  25043  om1elbas  25094  elpi1  25107  pi1xfr  25117  pi1coghm  25123  tcphcph  25299  lmmbrf  25324  iscfil  25327  iscau  25338  iscauf  25342  caucfil  25345  iscmet  25346  cmetcaulem  25350  iscmet3lem1  25353  iscmet3lem2  25354  iscmet3  25355  bcthlem1  25386  cmsss  25413  cmetcusp1  25415  cmetcusp  25416  cmscsscms  25435  rrxcph  25454  minveclem3b  25490  ovolfioo  25529  ovolficc  25530  ovolctb  25552  ovoliunnul  25569  ovolshftlem1  25571  sca2rab  25574  ovolscalem1  25575  ovolicc2lem1  25579  ovolicc2lem2  25580  ovolicc2lem4  25582  ovolicc2lem5  25583  iundisj  25610  iunmbl2  25619  uniioombllem3  25647  vitalilem2  25671  vitalilem3  25672  mbfss  25708  i1faddlem  25755  i1fmullem  25756  mbfi1fseqlem2  25778  mbfi1fseqlem4  25780  mbfi1fseq  25783  itg2splitlem  25810  itg2split  25811  itg2monolem1  25812  itg2gt0  25822  isibl  25827  iblss2  25868  itgss3  25877  itgsplit  25898  ellimc  25935  limcmo  25944  cnlimc  25950  limciun  25956  limcun  25957  eldv  25960  dvbsss  25964  dvreslem  25971  elcpn  25996  dvaddf  26004  dvmulf  26005  dvcof  26010  rolle  26052  dvlip2  26057  dvivthlem1  26070  lhop1  26076  lhop2  26077  ftc1cn  26105  fta1glem2  26229  plyco0  26252  elply  26255  ply1termlem  26263  eltayl  26423  tayl0  26425  taylplem1  26426  taylplem2  26427  dvtaylp  26433  taylthlem1  26436  taylthlem2  26437  abelth  26504  cxpcn3  26813  rlimcnp  27030  fsumharmonic  27076  dchrelbas  27300  pntrsumbnd2  27631  ostth2lem2  27698  nolesgn2ores  27736  nogesgn1ores  27738  nosupprefixmo  27764  noinfprefixmo  27765  nosupcbv  27766  nosupdm  27768  nosupfv  27770  nosupres  27771  nosupbnd1lem1  27772  nosupbnd1lem3  27774  nosupbnd1lem5  27776  nosupbnd2lem1  27779  noinfcbv  27781  noinfdm  27783  noinffv  27785  noinfres  27786  noinfbnd1lem1  27787  noinfbnd1lem3  27789  noinfbnd1lem5  27791  noinfbnd2lem1  27794  elmade  27950  elold  27952  sltsleft  27953  sltsright  27954  oldlim  27980  madebday  27993  newbday  27995  ltslpss  28001  bdayiun  28008  cofcutr  28017  cofcutrtime  28020  lrrecval  28032  lrrecval2  28033  addsval  28055  precsexlem9  28308  precsexlem11  28310  ltonold  28354  onnolt  28359  onlts  28360  noseqrdgfn  28399  istrkgb  28624  istrkgcb  28625  istrkge  28626  istrkgl  28627  istrkgld  28628  axtgsegcon  28633  axtg5seg  28634  axtgbtwnid  28635  axtgpasch  28636  axtgupdim2  28640  axtgeucl  28641  tgdim01  28676  iscgrg  28681  isismt  28703  tglnunirn  28717  tglngval  28720  tgellng  28722  legval  28753  legov  28754  legov2  28755  ishlg  28771  mirreu3  28827  mirval  28828  mirfv  28829  mircgr  28830  mirbtwn  28831  ismir  28832  mireq  28838  symquadlem  28862  israg  28870  perpln1  28883  perpln2  28884  isperp  28885  islnopp  28912  outpasch  28928  ishpg  28932  tgplnfn  28982  plngval  28984  isplng  28985  elplng  28987  elplngid  28989  lnincplng  28991  plngcplem  28992  plngcp  28993  plngrot  28997  iscgra  29003  dfcgra2  29024  isinag  29032  isleag  29041  iseqlg  29061  brprlng  29065  f1otrgitv  29070  f1otrg  29071  f1otrge  29072  ttgval  29075  ttgelitv  29083  elee  29094  brbtwn  29100  brcgr  29101  axlowdimlem16  29158  ebtwntg  29183  elntg2  29186  upgrex  29293  edgupgr  29335  upgredg  29338  edglnl  29344  numedglnl  29345  uhgr2edg  29409  umgr2edg1  29412  usgredg2vlem1  29426  usgredg2vlem2  29427  ushgredgedg  29430  ushgredgedgloop  29432  uhgrspansubgrlem  29491  fusgrfisstep  29530  nbgrval  29537  nbgrel  29541  nbupgrel  29546  nbgr2vtx1edg  29551  nbuhgr2vtx1edgblem  29552  nbuhgr2vtx1edgb  29553  nbusgreledg  29554  usgrnbcnvfv  29566  uvtxval  29588  uvtxel  29589  uvtx01vtx  29598  uvtxusgrel  29604  nbcplgr  29635  cplgr3v  29636  cusgrexi  29644  structtocusgr  29647  vtxdgfval  29668  vtxdg0v  29674  vtxdeqd  29678  vtxdun  29682  1loopgrnb0  29703  1loopgrvd0  29705  1hevtxdg0  29706  1hevtxdg1  29707  1egrvtxdg1  29710  umgr2v2evtxel  29723  umgr2v2enb1  29727  umgr2v2evd2  29728  vtxdginducedm1lem4  29743  vtxdginducedm1  29744  finsumvtxdg2sstep  29750  ewlksfval  29802  isewlk  29803  wksfval  29810  iswlk  29811  uspgr2wlkeq  29846  wlkres  29869  dfpth2  29929  usgr2pthlem  29963  clwlkcompim  29980  uspgrn2crct  30008  wwlks  30035  iswwlksn  30038  wwlknvtx  30045  wlkiswwlks2  30075  wwlksm1edg  30081  wwlksnred  30092  wwlksnext  30093  wwlksnredwwlkn  30095  wwlksnredwwlkn0  30096  wwlksnwwlksnon  30115  wspn0  30124  usgr2wspthons3  30167  rusgrnumwwlkb0  30174  clwwlk  30185  clwwlkccatlem  30191  clwlkclwwlklem2a4  30199  clwlkclwwlk  30204  clwwisshclwwslem  30216  clwwlkinwwlk  30242  clwwlkel  30248  clwwlkf  30249  clwwlkext2edg  30258  wwlksext2clwwlk  30259  wwlksubclwwlk  30260  clwwnisshclwwsn  30261  eleclclwwlknlem2  30263  erclwwlknsym  30272  erclwwlkntr  30273  umgrhashecclwwlk  30280  clwwlkvbij  30315  eupth2lem3lem3  30432  eupth2lem3lem4  30433  eupth2lem3lem6  30435  eupth2lemb  30439  eucrct2eupth  30447  fusgreg2wsplem  30535  2clwwlklem  30545  2clwwlk2clwwlklem  30548  2clwwlkel  30551  2clwwlk2clwwlk  30552  extwwlkfabel  30555  clwwlknonclwlknonf1o  30564  dlwwlknondlwlknonf1olem1  30566  numclwwlk2lem1  30578  numclwlk2lem2f  30579  numclwlk2lem2f1o  30581  ex-res  30643  isssp  30927  sspn  30939  islno  30956  isblo  30985  nmlno0  30998  ishmo  31014  dipdir  31045  dipass  31048  ubthlem1  31073  ubthlem2  31074  htthlem  31120  htth  31121  ocel  31484  ocnel  31501  shsel  31517  shsel2  31525  shmodsi  31592  pjhtheu  31597  pjeq  31602  axpjpj  31623  pjoc2  31642  elspani  31746  h1de2ctlem  31758  elspansn  31769  elspansn2  31770  elnlfn  32131  eleigvec  32160  riesz3i  32265  cbviunf  32755  iuneq12daf  32756  iunrdx  32763  iunrnmptss  32765  cbvdisjf  32771  disjorf  32779  disjabrex  32782  disjabrexf  32783  iundisjf  32789  disjrdx  32791  fresunsn  32827  2ndresdju  32851  abfmpunirn  32854  abfmpeld  32856  abfmpel  32857  fmptcof2  32859  acunirnmpt2  32862  acunirnmpt2f  32863  aciunf1lem  32864  suppss3  32925  fpwrelmap  32935  xrofsup  32969  iundisjfi  32998  eliccioo  33108  s3f1  33125  ccatf1  33127  ccatws1f1o  33129  swrdrn3  33133  ismnt  33161  mgcoval  33164  gsummpt2co  33228  gsumpart  33243  gsumhashmul  33247  gsummulsubdishift1  33248  xrge0tsmsbi  33254  gsumwrd2dccatlem  33257  gsumwrd2dccat  33258  cycpmco2  33313  cyc3co2  33320  isfxp  33348  cntrval2  33351  inftmrel  33360  isinftm  33361  isslmd  33382  urpropd  33411  elrgspn  33427  erlval  33439  rlocval  33440  rloccring  33452  rloc1r  33454  rlocisunit  33457  domnprodeq0  33460  domnpropd  33461  isdrng4  33482  fracfld  33495  resv1r  33525  ellspds  33554  ellpi  33559  lbslsp  33563  rhmimaidl  33618  isprmidl  33624  qsidomlem1  33639  qsidomlem2  33640  ismxidl  33650  crngmxidl  33657  drng0mxidl  33664  opprqus0g  33678  qsfld  33686  isrprm  33713  rsprprmprmidlb  33719  ressply1evls1  33761  ply1mulrtss  33778  ply1coedeg  33785  psrmonmul  33847  dimpropd  33906  lbslsat  33913  extdg1id  33963  fldextrspunlsplem  33970  fldextrspunlsp  33971  elirng  33983  ply1annidllem  33998  constrsuc  34035  constrconj  34042  constrllcllem  34049  constrlccllem  34050  constrcccllem  34051  nn0constr  34058  smatrcl  34093  smatcl  34099  ist0cld  34130  txomap  34131  locfinreflem  34137  zarclsiin  34168  zart0  34176  rhmpreimacnlem  34181  metidval  34187  cnre2csqima  34208  ordtrest2NEW  34220  fmcncfil  34228  fsumcvg4  34247  ofcfval  34395  measvuni  34511  meascnbl  34516  faeval  34543  ismbfm  34548  elunirnmbfm  34549  imambfm  34559  elcarsg  34602  itgeq12dv  34623  issibf  34630  eulerpartlems  34657  eulerpartlemgc  34659  eulerpartlemgvv  34673  eulerpartlemgu  34674  eulerpart  34679  rrvmbfm  34739  elorvc  34757  elorrvc  34761  dstfrvunirn  34772  ballotlemfc0  34790  ballotlemfcc  34791  ballotlemsima  34813  ballotlemrv  34817  fzssfzo  34836  signstfvn  34863  signstfvneq0  34866  signstres  34869  repr0  34905  reprinrn  34912  reprdifc  34921  hgt750lemg  34948  hgt750lemb  34950  istrkg2d  34960  axtgupdim2ALTV  34962  afsval  34968  brafs  34969  bnj945  35069  bnj1400  35130  bnj18eq1  35222  bnj916  35228  bnj1014  35256  bnj1015  35257  bnj1110  35277  bnj1417  35336  rankval2b  35395  r1filimi  35399  r1ssel  35403  onvf1odlem3  35448  vonf1wev  35451  vonf1owevOLD  35453  vonf1osev  35455  revpfxsfxrev  35466  cplgredgex  35471  pfxwlk  35474  revwlk  35475  subfacp1lem2b  35531  subfacp1lem4  35533  subfacp1lem5  35534  subfacp1lem6  35535  ptpconn  35583  cvmscbv  35608  iscvm  35609  cvmsi  35615  cvmsval  35616  cvmliftmolem1  35631  cvmlift2lem12  35664  cvmlift2lem13  35665  cvmlift3lem7  35675  snmlval  35681  satfv1  35713  satfvsucsuc  35715  satfrnmapom  35720  satf0op  35727  satf0n0  35728  sat1el2xp  35729  fmlafvel  35735  isfmlasuc  35738  fmlaomn0  35740  gonan0  35742  goaln0  35743  gonar  35745  goalr  35747  satffunlem1lem2  35753  satffunlem2lem2  35756  satfv0fvfmla0  35763  satef  35766  satefvfmla0  35768  sategoelfvb  35769  satfv1fvfmla1  35773  mrsubfval  35858  mrsubvrs  35872  mclsrcl  35911  mclsval  35913  mppsval  35922  mclsppslem  35933  opelco3  36125  wsuclem  36173  funtransport  36381  fvtransport  36382  brcolinear  36409  colineardim1  36411  funray  36490  fvray  36491  funline  36492  fvline  36494  lineelsb2  36498  fwddifval  36512  fwddifnval  36513  rankelg  36518  rankeq1o  36521  elhf2  36525  0hf  36527  nmulprop  36540  nmulr0  36545  rmoeqbidv  36573  disjeq12dv  36575  ixpeq12dv  36576  prodeq12sdv  36578  itgeq12sdv  36579  cbvralvw2  36586  cbvrexvw2  36587  cbvrmovw2  36588  cbvreuvw2  36589  cbvcsbvw2  36591  cbviunvw2  36592  cbviinvw2  36593  cbvmptvw2  36594  cbvdisjvw2  36595  cbvmpo1vw2  36603  cbvmpo2vw2  36604  cbvsbcdavw  36617  cbvcsbdavw  36619  cbvcsbdavw2  36620  cbviundavw  36622  cbviindavw  36623  cbvdisjdavw  36628  cbvrabdavw2  36645  cbviundavw2  36646  cbviindavw2  36647  cbvmptdavw2  36648  cbvdisjdavw2  36649  cbvriotadavw2  36650  cbvmpo1davw2  36652  cbvmpo2davw2  36653  cbvsumdavw2  36655  neibastop2lem  36720  neibastop3  36722  eltail  36734  ttctr  36853  dfttc2g  36866  mh-infprim2bi  36907  bj-projeq  37477  bj-projval  37481  bj-restsn  37572  opelopabbv  37635  brabd0  37639  bj-eldiag  37668  bj-eldiag2  37669  mptsnunlem  37832  dissneqlem  37834  iooelexlt  37856  relowlssretop  37857  rdgellim  37870  exrecfnlem  37873  finxpeq1  37880  finxpreclem6  37890  pibp21  37909  curf  38097  uncf  38098  curunc  38101  unccur  38102  fin2so  38106  lindsadd  38112  lindsdom  38113  lindsenlbs  38114  matunitlindflem1  38115  matunitlindflem2  38116  matunitlindf  38117  ptrest  38118  ptrecube  38119  poimirlem2  38121  poimirlem8  38127  poimirlem17  38136  poimirlem18  38137  poimirlem20  38139  poimirlem21  38140  poimirlem22  38141  poimirlem24  38143  poimirlem26  38145  poimirlem29  38148  heicant  38154  mblfinlem1  38156  mblfinlem2  38157  volsupnfl  38164  itg2addnclem  38170  itg2gt0cn  38174  indexdom  38233  incsequz  38247  istotbnd  38268  istotbnd3  38270  0totbnd  38272  sstotbnd  38274  sstotbnd3  38275  isbnd  38279  prdstotbnd  38293  cntotbnd  38295  isismty  38300  heibor1lem  38308  heiborlem2  38311  heiborlem3  38312  heibor  38320  isass  38345  exidcl  38375  exidreslem  38376  elghomlem2OLD  38385  rngoidmlem  38435  rngo1cl  38438  divrngcl  38456  isdrngo2  38457  isrngohom  38464  isrngoiso  38477  isriscg  38483  iscom2  38494  iscringd  38497  isidl  38513  ispridl  38533  ismaxidl  38539  ac6s6  38671  dmecd  38809  dfpre4  38979  releldmqs  39242  releldmqscoss  39244  erimeq2  39262  qmapeldisjsim  39359  eldisjlem19  39412  membpartlem19  39413  prter3  39506  islshp  39603  islsat  39615  lcvfbr  39644  islfl  39684  ellkr  39713  islshpkrN  39744  ldual1dim  39790  isopos  39804  cmtfvalN  39834  cvrfval  39892  isat  39910  islln  40130  islpln  40154  islvol  40197  isline  40363  ispointN  40366  ispsubsp  40369  elpmap  40382  elpmapat  40388  elpadd  40423  paddclN  40466  elpclN  40516  elpcliN  40517  pclfinN  40524  pclcmpatN  40525  ispsubclN  40561  iswatN  40618  islhp  40620  islaut  40707  ispautN  40723  isldil  40734  isltrn  40743  isdilN  40778  istrnN  40781  istendo  41384  dvhb1dimN  41610  erng1lem  41611  erngdvlem4-rN  41623  diaelval  41657  diaeldm  41660  dia1dimid  41687  cdlemm10N  41742  dibopelvalN  41767  dibopelval2  41769  dibelval3  41771  dibelval1st  41773  dibelval2nd  41776  dibeldmN  41782  dibvalrel  41787  dibglbN  41790  dicffval  41798  dicfval  41799  dicopelval  41801  dicelvalN  41802  dicelval3  41804  dicvalrelN  41809  dicelval1sta  41811  diclspsn  41818  dihopelvalbN  41862  dihopelvalcqat  41870  dihopelvalcpre  41872  dihvalrel  41903  dih1  41910  dihmeetlem4preN  41930  dihmeetlem13N  41943  dih1dimatlem  41953  dochnel2  42016  dihjatcclem4  42045  dvh2dim  42069  dvh3dim  42070  dvh4dimN  42071  dochfln0  42101  lpolsetN  42106  islpolN  42107  lcfrvalsnN  42165  lcfrlem21  42187  lcfrlem27  42193  lcfrlem37  42203  lcfr  42209  lcdlss  42243  mapdcv  42284  hdmap1fval  42420  hdmapffval  42450  hdmapfval  42451  hdmapval  42452  hgmapffval  42509  hgmapfval  42510  hdmapellkr  42538  hlhilhillem  42584  fzsplitnd  42599  isprimroot  42710  primrootsunit1  42714  primrootscoprmpow  42716  primrootscoprbij  42719  aks6d1c1p2  42726  aks6d1c1p3  42727  aks6d1c1p4  42728  aks6d1c1p5  42729  aks6d1c1p6  42731  aks6d1c1  42733  evl1gprodd  42734  sticksstones11  42773  sticksstones12a  42774  rhmqusspan  42802  grpods  42811  fzosumm1  42866  frlmfielbas  43122  frlmsnic  43158  psrmnd  43161  isnacs  43285  mrefg2  43288  elmzpcl  43307  mzpcompact2  43333  eldiophb  43338  elpell1qr  43424  elpell14qr  43426  elpell1234qr  43428  pw2f1ocnv  43614  pw2f1o2val2  43617  aomclem4  43634  aomclem6  43636  islssfg2  43648  imasgim  43677  lnr2i  43693  elmnc  43713  rngunsnply  43746  onexomgt  43818  onexlimgt  43820  onexoegt  43821  oaordnr  43873  omnord1  43882  oenord1  43893  cantnfresb  43901  tfsconcatun  43914  tfsconcat0i  43922  ofoaf  43932  naddcnff  43939  naddcnffo  43941  naddcnfcom  43943  naddcnfid1  43944  naddcnfid2  43945  naddcnfass  43946  naddwordnexlem4  43978  fiinfi  44149  sqrtcvallem1  44207  elintima  44229  eliunov2  44255  ov2ssiunov2  44276  brtrclfv2  44303  rfovcnvf1od  44580  rfovcnvfvd  44583  fsovrfovd  44585  fsovfvd  44586  fsovcnvlem  44589  ntrclsfv1  44631  ntrclselnel1  44633  ntrclsneine0lem  44640  ntrneifv1  44655  ntrneifv2  44656  ntrneiel  44657  gneispace2  44708  gneispacess2  44722  extoimad  44740  mnringelbased  44793  dvconstbi  44910  bccbc  44921  wfac8prim  45578  permaxrep  45582  permac8prim  45590  eliin2f  45682  iineq12dv  45684  rabbida2  45710  disjinfi  45770  unirnmap  45784  elmptima  45833  iuneqfzuzlem  45910  iooiinioc  46132  fsumiunss  46151  fsumsupp0  46154  lptre2pt  46214  icccncfext  46461  cncfiooicclem1  46467  dvnprodlem2  46521  stoweidlem27  46601  stoweidlem29  46603  stoweidlem31  46605  stoweidlem34  46608  stoweidlem48  46622  stoweidlem59  46633  dirkercncflem2  46678  dirkercncflem4  46680  fourierdlem2  46683  fourierdlem3  46684  fourierdlem25  46706  fourierdlem32  46713  fourierdlem33  46714  fourierdlem41  46722  fourierdlem48  46728  fourierdlem49  46729  fourierdlem62  46742  fourierdlem70  46750  fourierdlem80  46760  fourierdlem92  46772  fourierdlem93  46773  fourierdlem101  46781  etransclem37  46845  sge0val  46940  sge0f1o  46956  sge0iunmptlemre  46989  sge0iunmpt  46992  iundjiun  47034  caragenel  47069  ovncvrrp  47138  ovnsubaddlem1  47144  ovnsubadd  47146  hoidmvlelem2  47170  hoidmvlelem3  47171  hoidmvlelem4  47172  hoidmvle  47174  ovncvr2  47185  hspdifhsp  47190  hoiqssbl  47199  hspmbllem2  47201  hspmbl  47203  opnvonmbllem1  47206  isvonmbl  47212  ovnovollem1  47230  issmflem  47301  smflimlem3  47347  smflimlem4  47348  smflim  47351  smfmullem2  47366  smflimmpt  47384  smfsuplem1  47385  smflimsuplem1  47394  smflimsuplem3  47396  smflimsuplem4  47397  smflimsuplem7  47400  smflimsup  47402  chnsubseq  47456  fcores  47661  fcoresf1  47663  afvelrnb  47757  afvelrnb0  47758  afv2co2  47851  el1fzopredsuc  47920  muldvdsfacm1  47981  iccpart  48022  iccpartgtprec  48026  iccpartiltu  48028  iccpartigtl  48029  iccpartltu  48031  iccpartgtl  48032  iccpartgt  48033  iccpartleu  48034  iccpartgel  48035  iccelpart  48039  iccpartiun  48040  icceuelpart  48042  fargshiftfv  48045  fargshiftfo  48048  sprel  48090  prprelb  48122  prprelprb  48123  nprmdvdsfacm1lem4  48232  fpprel  48350  sbgoldbo  48409  wtgoldbnnsum4prm  48424  bgoldbnnsum3prm  48426  bgoldbtbndlem3  48429  bgoldbtbnd  48431  clnbgrval  48444  elclnbgrelnbgr  48447  clnbgrel  48450  clnbupgrel  48456  vopnbgrel  48476  isubgredg  48488  upgrimwlklem3  48521  upgrimwlklem5  48523  upgrimpths  48531  grtriprop  48563  isgrtri  48565  grtriclwlk3  48567  stgredgel  48579  gpgvtxel  48669  gpgiedgdmel  48671  gpgedgel  48672  opgpgvtx  48677  gpg5nbgrvtx13starlem1  48693  gpg5nbgrvtx13starlem2  48694  gpg5nbgrvtx13starlem3  48695  gpg3kgrtriex  48711  grlimedgnedg  48753  upwlksfval  48757  isupwlk  48758  intop  48825  isclintop  48829  assintop  48831  isassintop  48832  assintopcllaw  48834  uzlidlring  48857  elrngchomALTV  48891  rngccatidALTV  48894  rngcsectALTV  48897  rngcisoALTV  48899  rhmsubcALTVlem3  48905  rhmsubcALTVlem4  48906  funcringcsetcALTV2lem7  48918  funcringcsetcALTV2lem9  48920  elringchomALTV  48925  ringccatidALTV  48928  ringcsectALTV  48931  ringcisoALTV  48933  ringcbasbasALTV  48934  funcringcsetclem7ALTV  48941  funcringcsetclem9ALTV  48943  srhmsubcALTV  48947  cbvmpox2  48958  ply1sclrmsm  49006  dmatALTbasel  49024  lcoval  49034  lindslinindsimp1  49079  lindslinindsimp2  49085  lmod1  49114  elbigo  49173  elbigo2  49174  elbigolo1  49179  dig2nn0ld  49226  naryfvalel  49252  rrxlines  49355  rrxlinesc  49357  rrxlinec  49358  eenglngeehlnm  49361  elrrx2linest2  49367  rrxsphere  49370  itsclc0  49393  itsclc0b  49394  itsclinecirc0  49395  itsclinecirc0b  49396  itscnhlinecirc02p  49407  brab2dd  49449  f1omo  49514  f1omoOLD  49515  lubeldm2d  49579  glbeldm2d  49580  catprs  49632  sectpropdlem  49657  nelsubc3lem  49691  initc  49712  imaid  49775  upfval  49797  upfval2  49798  upfval3  49799  uppropd  49802  oppcinito  49856  oppctermo  49857  oppczeroo  49858  initopropd  49864  termopropd  49865  isthinc  50040  isthincd2lem1  50046  thincmoALT  50050  thincmod  50051  isthincd  50057  thincpropd  50063  indcthing  50081  discthing  50082  prsthinc  50085  termcterm  50134  termc2  50139  isinito4  50168  2arwcatlem1  50216  setc1onsubc  50223  cnelsubclem  50224  ranval3  50252  lmdfval2  50276  cmdfval2  50277  termolmd  50291  elsetrecslem  50320