Theorem eleq2d 2822

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eleq2  2825  eleq12d  2830  eleqtrd  2838  neleqtrd  2858  eqabrd  2877  raleqbidv  3316  rexeqbidv  3317  reueqbidv  3388  rabeqbidva  3415  elabd2  3624  sbcbid  3795  csbeq2d  3855  csbeq2dv  3856  cbvcsbw  3859  cbvcsb  3860  cbvcsbv  3861  csbie  3884  csbied  3885  csbie2g  3889  cbvralcsf  3891  cbvreucsf  3893  cbvrabcsf  3894  sbcel12  4363  sbcel1g  4368  sbcel2  4370  prel12g  4820  eliuni  4952  iuneqconst  4958  iuneq12df  4973  iuneq12d  4976  cbviun  4990  cbviin  4991  cbviung  4992  cbviing  4993  cbviunv  4994  cbviinv  4995  iinxsng  5043  iinxprg  5044  iunxsng  5045  iunxsngf  5047  cbvdisj  5075  cbvdisjv  5076  disjor  5080  disjiund  5089  mpteq12da  5181  mpteq12f  5183  mpteq12dva  5184  axpweq  5296  rabxfrd  5362  rbropapd  5510  opeliunxp  5691  opeliun2xp  5692  opeliunxp2  5787  iunxpf  5797  elimampt  6002  elrelimasn  6045  elimasni  6050  imadifssran  6109  xpdifid  6126  ressn  6243  funfni  6598  fnbr  6600  dffv3  6830  elfv2ex  6877  fvelrnb  6894  foelcdmi  6895  fvun1  6925  fvco2  6931  elfvmptrab1w  6968  elfvmptrab1  6969  elfvmptrab  6970  elpreima  7003  dff3  7045  fmptco  7074  fnelfp  7121  fnelnfp  7123  tpres  7147  fnprb  7154  fntpb  7155  funfvima3  7182  eluniima  7196  dff13  7200  f1ounsn  7218  f1eqcocnv  7247  isoini  7284  riotaeqdv  7316  mpoeq123dva  7432  cbvmpox  7451  elimampo  7495  ovelrn  7534  elovmpod  7602  elovmpo  7603  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  elovmpt3rab1  7618  fiun  7887  f1iun  7888  zfrep6  7899  fmpox  8011  el2mpocsbcl  8027  el2mpocl  8028  bropopvvv  8032  bropfvvvv  8034  xpord2indlem  8089  xpord3inddlem  8096  elsuppfng  8111  elsuppfn  8112  suppfnss  8131  opeliunxp2f  8152  mpoxopn0yelv  8155  mpoxopovel  8162  rntpos  8181  mpocurryd  8211  fpr2  8246  wfr2  8269  onoviun  8275  smoel  8292  smoiso  8294  smoel2  8295  smo11  8296  tfrlem9  8316  oalimcl  8487  oaass  8488  omordi  8493  omordlim  8504  omlimcl  8505  odi  8506  omeulem1  8509  omeulem2  8510  oen0  8514  oeordi  8515  oeordsuc  8522  oelimcl  8528  oeeulem  8529  oeeui  8530  nnmordi  8559  oaabs2  8577  omabs  8579  omsmolem  8585  ereldm  8688  iiner  8726  elmapg  8776  elpmg  8780  elixpsn  8875  ixpsnf1o  8876  boxriin  8878  omxpenlem  9006  pw2f1olem  9009  phplem2  9129  php3  9133  infn0  9202  elfi  9316  dffi3  9334  marypha2lem2  9339  ordiso2  9420  wemapsolem  9455  elharval  9466  inf3lemd  9536  inf3lem1  9537  inf3lem2  9538  inf3lem3  9539  cantnfs  9575  cantnfp1lem3  9589  cantnflem1b  9595  cantnflem1  9598  ttrclselem2  9635  trcl  9637  frr2  9672  r1sdom  9686  r1ordg  9690  r1pwss  9696  tz9.12lem3  9701  tz9.12  9702  r1elwf  9708  rankr1ai  9710  rankidb  9712  rankr1bg  9715  rankval2  9730  rankunb  9762  tcrank  9796  acni  9955  acni2  9956  acndom  9961  infpwfien  9972  alephnbtwn  9981  cardaleph  9999  cardinfima  10007  iunfictbso  10024  dfac3  10031  dfac5lem5  10037  dfac5  10039  dfac9  10047  dfac12r  10057  kmlem2  10062  kmlem12  10072  kmlem13  10073  kmlem14  10074  ackbij2lem3  10150  ackbij2  10152  cofsmo  10179  alephsing  10186  fin23lem30  10252  isf32lem9  10271  itunisuc  10329  axcc2lem  10346  axcc3  10348  domtriomlem  10352  axdc2lem  10358  axdc2  10359  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  ac6c4  10391  zorn2lem1  10406  ttukeylem6  10424  pwcfsdom  10494  axregndlem2  10514  axinfndlem1  10516  axacndlem4  10521  axacnd  10523  pwfseqlem1  10569  inar1  10686  inatsk  10689  gruurn  10709  grur1  10731  eltskm  10754  genpelv  10911  eluz1  12755  elixx1  13270  elixx3g  13274  elioo2  13302  elfz1  13428  elfz2  13430  elfzp1  13490  fzpr  13495  fzsuc2  13498  fzrev3  13506  elfzp12  13519  fzm1  13523  elfzo  13577  fz0add1fz1  13651  elfzo0l  13672  elfzom1b  13682  fzosplitsni  13695  elfzr  13697  elfzlmr  13698  zmodidfzo  13820  seqp1  13939  seqf1o  13966  bcval  14227  bcpasc  14244  hashf1lem1  14378  fundmge2nop0  14425  wrdmap  14469  elovmpowrd  14481  ccatfval  14496  elfzelfzccat  14503  ccatlid  14510  ccatass  14512  ccatrn  14513  ccatalpha  14517  swrdfv2  14585  ccatswrd  14592  swrdccat2  14593  pfxfv  14606  pfxeq  14619  ccatpfx  14624  swrdswrd  14628  swrdpfx  14630  pfxpfx  14631  cats1un  14644  swrdccatfn  14647  swrdccatin1  14648  pfxccatin12lem4  14649  pfxccatin12lem1  14651  swrdccatin2  14652  pfxccatin12lem2c  14653  pfxccatin12lem2  14654  swrdccat3blem  14662  swrdccatin1d  14666  swrdccatin2d  14667  pfxccatin12d  14668  revccat  14689  revrev  14690  repswpfx  14708  repswccat  14709  cshwidxmod  14726  2cshw  14736  cshwcshid  14750  cshwcsh2id  14751  cshimadifsn  14752  cshimadifsn0  14753  revco  14757  ccatco  14758  cshco  14759  swrdco  14760  ofccat  14892  shftfn  14996  shftval  14997  limsupgle  15400  ello12  15439  elo12  15450  isercolllem3  15590  sumeq1  15612  fsumsplit  15664  sumsplit  15691  fsum2dlem  15693  fsumcom2  15697  fsumparts  15729  explecnv  15788  pwdif  15791  fprodser  15872  fprodsplit  15889  fprod2dlem  15903  fprodcom2  15907  eftlub  16034  divalgmod  16333  bitsval  16351  bitsp1e  16359  bitsp1o  16360  sadfval  16379  sadcp1  16382  sadval  16383  sadcadd  16385  sadadd2  16387  saddisjlem  16391  sadadd  16394  sadass  16398  smufval  16404  smuval  16408  smuval2  16409  smupvallem  16410  smu01lem  16412  smueqlem  16417  smumul  16420  bezoutlem2  16467  bezoutlem4  16469  algfx  16507  eucalgcvga  16513  reumodprminv  16732  nnnn0modprm0  16734  unbenlem  16836  prmreclem5  16848  vdwapval  16901  vdwapun  16902  vdwnnlem1  16923  vdwnn  16926  ramval  16936  0ram  16948  ramub1lem2  16955  prmgaplem7  16985  prmlem0  17033  elrest  17347  prdsbasmpt  17390  prdsleval  17397  prdsbasmpt2  17402  pwselbasb  17408  imasaddfnlem  17449  imasvscafn  17458  divsfval  17468  ismre  17509  mreunirn  17520  mrisval  17553  ismri  17554  isacs  17574  catidd  17603  iscatd2  17604  ismon  17657  isepi  17664  sectffval  17674  sectfval  17675  dfiso2  17696  cicsym  17728  issubc  17759  catsubcat  17763  isfunc  17788  funcres  17820  funcpropd  17826  ffthiso  17855  isnat  17874  isnat2  17875  fuciso  17902  initoval  17917  termoval  17918  isinito  17920  istermo  17921  iszeroo  17922  isinitoi  17923  istermoi  17924  initoid  17925  termoid  17926  iszeroi  17933  2initoinv  17934  initoeu1  17935  initoeu2  17940  2termoinv  17941  termoeu1  17942  arwhoma  17969  elsetchom  18005  setcmon  18011  setcepi  18012  setciso  18015  catciso  18035  elestrchom  18051  estrcbasbas  18054  funcestrcsetclem7  18069  funcestrcsetclem8  18070  funcestrcsetclem9  18071  fthestrcsetc  18073  fullestrcsetc  18074  equivestrcsetc  18075  setc1strwun  18076  funcsetcestrclem7  18084  funcsetcestrclem8  18085  funcsetcestrclem9  18086  fthsetcestrc  18088  fullsetcestrc  18089  hofcl  18182  hofpropd  18190  yonedalem4c  18200  yonedainv  18204  yonffthlem  18205  lubeldm  18274  glbeldm  18287  joindef  18297  meetdef  18311  poslubdg  18335  acsficl2d  18475  acsmapd  18477  psref  18497  psss  18503  dirge  18526  chnccats1  18548  chnccat  18549  chnrev  18550  mgmpropd  18576  issstrmgm  18578  grpidval  18586  grpidpropd  18587  grpidd  18596  ismgmhm  18621  issubmgm  18627  issgrpd  18655  sgrppropd  18656  ismndd  18681  mndpropd  18684  imasmnd2  18699  imasmnd  18700  xpsmnd0  18703  ismhm  18710  issubm  18728  gsumsgrpccat  18765  elefmndbas2  18799  smndex1mndlem  18834  imasgrp2  18985  imasgrp  18986  issubg  19056  subginv  19063  isnsg  19084  eqg0el  19112  quselbas  19113  isghm  19144  isghmOLD  19145  resghm2b  19163  conjnmzb  19182  conjnsg  19183  ghmpropd  19185  isga  19220  elcntz  19251  elcntzsn  19254  cntzrcl  19256  resscntz  19262  symgextf1  19350  gsmsymgreqlem2  19360  f1otrspeq  19376  pmtrfrn  19387  pmtrdifellem3  19407  pmtrdifellem4  19408  psgnunilem1  19422  psgnunilem5  19423  psgnunilem2  19424  psgnunilem3  19425  psgneldm2  19433  psgnfitr  19446  psgnsn  19449  gexdvds  19513  gex1  19520  isslw  19537  sylow3lem2  19557  lsmelvalx  19569  pj1ghm  19632  efgtlen  19655  efgsfo  19668  efgredlemc  19674  frgp0  19689  frgpmhm  19694  qusabl  19794  frgpnabllem1  19802  imasabl  19805  cycsubmcmn  19818  0cyg  19822  cycsubgcyg  19830  gsumval3  19836  gsumcllem  19837  gsumzaddlem  19850  gsumzsplit  19856  gsummptfzcl  19898  eldprd  19935  dprdcntz2  19969  dprd2d2  19975  dmdprdsplit2lem  19976  dmdprdsplit2  19977  dprdsplit  19979  ablfac2  20020  isrngd  20108  rngpropd  20109  imasrng  20112  qusrng  20115  ringurd  20120  isringd  20226  imasring  20266  xpsring1d  20269  dvdsrval  20297  isunit  20309  dvdsrpropd  20352  isirred  20355  isrnghm  20377  isrngim  20381  c0ghm  20397  c0snghm  20400  isrhm  20414  isrim0  20418  islring  20473  issubrng  20480  opprsubrng  20492  issubrg  20504  opprsubrg  20526  resrhm2b  20535  rhmpropd  20542  rnghmresel  20553  elrngchom  20557  rnghmsubcsetclem1  20564  rnghmsubcsetclem2  20565  rngcid  20568  rngcsect  20569  rngciso  20571  funcrngcsetcALT  20574  zrinitorngc  20575  zrtermorngc  20576  rhmresel  20582  elringchom  20586  rhmsubcsetclem1  20593  rhmsubcsetclem2  20594  ringcid  20597  rhmsscrnghm  20598  rhmsubcrngclem1  20599  rhmsubcrngclem2  20600  ringcsect  20603  ringciso  20605  ringcbasbas  20606  zrtermoringc  20608  srhmsubc  20613  rhmsubclem3  20620  rhmsubclem4  20621  drngunit  20667  isdrngd  20698  isdrngdOLD  20700  issdrg  20721  sdrgunit  20729  isabv  20744  issrngd  20788  islmod  20815  lmodprop2d  20875  islss  20885  islssd  20886  lssats2  20951  ellspsn  20954  islmhm  20979  lmhmf1o  20998  lmhmima  20999  lmhmpreima  21000  reslmhm  21004  pwssplit3  21013  lmhmpropd  21025  islbs  21028  lspprel  21046  lspfixed  21083  lbsacsbs  21111  lbsextlem1  21113  lbsextlem2  21114  lbsextlem3  21115  lbsextlem4  21116  ixpsnbasval  21160  isridlrng  21174  rnglidlmmgm  21200  isridl  21207  quscrng  21238  rngqiprngimfolem  21245  rngqiprngimf1lem  21249  rngqiprngimfo  21256  islpidl  21280  lidldvgen  21289  irinitoringc  21434  pzriprnglem13  21448  pzriprnglem14  21449  zrhrhmb  21465  znf1o  21506  frgpcyg  21528  psgnevpmb  21542  isphld  21609  phlssphl  21614  elocv  21623  iscss  21638  isobs  21675  obs2ss  21684  dsmmfi  21693  dsmmelbas  21694  dsmmlss  21699  frlmelbas  21711  frlmlbs  21752  frlmup1  21753  ellspd  21757  islinds  21764  islindf2  21769  f1lindf  21777  islindf4  21793  assamulgscmlem2  21856  psrgrp  21912  mplsubglem  21954  mpllsslem  21955  mplmonmul  21991  subrgascl  22021  subrgasclcl  22022  mpfind  22070  ismhp  22083  gsumply1subr  22174  lply1binomsc  22255  matbas2d  22367  matecl  22369  matvscl  22375  mat1  22391  mat0dim0  22411  mat0dimid  22412  mat0dimscm  22413  mat1dimelbas  22415  dmatel  22437  scmatel  22449  scmateALT  22456  scmataddcl  22460  scmatsubcl  22461  smatvscl  22468  scmatghm  22477  mat1scmat  22483  mdetunilem7  22562  mdetunilem9  22564  smadiadetr  22619  cramerimplem2  22628  cramer0  22634  pmatcoe1fsupp  22645  cpmatpmat  22654  cpmatel  22655  cpmatacl  22660  cpmatinvcl  22661  mat2pmatghm  22674  mat2pmatmul  22675  decpmatmullem  22715  pmatcollpwlem  22724  pmatcollpw3fi1lem1  22730  pmatcollpwscmatlem1  22733  monmat2matmon  22768  chfacfscmul0  22802  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  cayhamlem1  22810  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  cayhamlem2  22828  istopon  22856  eltg  22901  eltg2  22902  eltop  22918  eltop2  22919  eltop3  22920  pptbas  22952  iscld  22971  neiss2  23045  isnei  23047  neiptopnei  23076  neiptopreu  23077  lpfval  23082  lpval  23083  islp  23084  maxlp  23091  islpi  23093  neitr  23124  restlp  23127  ordtbas2  23135  ordtrest2  23148  lmfval  23176  cnfval  23177  iscn  23179  iscnp  23181  tgcn  23196  tgcnp  23197  lmbrf  23204  cnpresti  23232  ist1  23265  ist1-2  23291  cnt1  23294  haust1  23296  cmpfi  23352  cmpfii  23353  1stcfb  23389  2ndc1stc  23395  1stcrest  23397  2ndcdisj  23400  1stcelcls  23405  nllyi  23419  subislly  23425  islocfin  23461  lfinpfin  23468  locfindis  23474  locfincf  23475  comppfsc  23476  kgenval  23479  elkgen  23480  kgencn2  23501  txbas  23511  eltx  23512  ptval  23514  ptpjpre1  23515  ptopn2  23528  ptpjopn  23556  ptclsg  23559  xkoccn  23563  txdis  23576  txdis1cn  23579  ptrescn  23583  hausdiag  23589  hauseqlcld  23590  txhaus  23591  xkohaus  23597  elqtop  23641  qtopeu  23660  kqcldsat  23677  hmeofval  23702  ptuncnv  23751  ptunhmeo  23752  elmptrab  23771  fbdmn0  23778  elfg  23815  elfilss  23820  filunirn  23826  fixufil  23866  elfm  23891  rnelfmlem  23896  rnelfm  23897  fmfnfmlem4  23901  elflim2  23908  flimtopon  23914  elflim  23915  hausflim  23925  flimcls  23929  flfnei  23935  isflf  23937  hausflf  23941  cnpflf  23945  cnflf  23946  txflf  23950  isfcls  23953  fclstopon  23956  isfcls2  23957  fclssscls  23962  fclsnei  23963  fclsfnflim  23971  flimfnfcls  23972  isfcf  23978  fcfelbas  23980  cnpfcf  23985  cnfcf  23986  flfcntr  23987  alexsublem  23988  alexsubALTlem3  23993  cnextfun  24008  cnextfvval  24009  cnextf  24010  cnextcn  24011  tmdgsum2  24040  tgpconncomp  24057  ghmcnp  24059  qustgplem  24065  eltsms  24077  haustsms  24080  tsmsgsum  24083  tsmssubm  24087  tsmssplit  24096  isust  24148  ustbas  24171  elutop  24177  ustuqtoplem  24183  ustuqtop4  24188  ustuqtop  24190  utopsnneiplem  24191  utopsnneip  24192  utopsnnei  24193  isusp  24205  isucn  24221  ucncn  24228  iscfilu  24231  neipcfilu  24239  iscusp  24242  cnextucn  24246  ispsmet  24248  ismet  24267  isxmet  24268  elblps  24331  elbl  24332  elmopn  24386  prdsbl  24435  neibl  24445  met1stc  24465  metrest  24468  prdsxmslem2  24473  txmetcnp  24491  txmetcn  24492  metustsym  24499  cfilucfil2  24505  elbl4  24507  metuel  24508  psmetutop  24511  restmetu  24514  metucn  24515  tngngp  24598  isnmhm  24690  zcld  24758  metnrmlem1a  24803  elcncf  24838  cncfcnvcn  24875  cnheibor  24910  lebnumlem1  24916  ishtpy  24927  isphtpy  24936  om1elbas  24988  elpi1  25001  pi1xfr  25011  pi1coghm  25017  tcphcph  25193  lmmbrf  25218  iscfil  25221  iscau  25232  iscauf  25236  caucfil  25239  iscmet  25240  cmetcaulem  25244  iscmet3lem1  25247  iscmet3lem2  25248  iscmet3  25249  bcthlem1  25280  cmsss  25307  cmetcusp1  25309  cmetcusp  25310  cmscsscms  25329  rrxcph  25348  minveclem3b  25384  ovolfioo  25424  ovolficc  25425  ovolctb  25447  ovoliunnul  25464  ovolshftlem1  25466  sca2rab  25469  ovolscalem1  25470  ovolicc2lem1  25474  ovolicc2lem2  25475  ovolicc2lem4  25477  ovolicc2lem5  25478  iundisj  25505  iunmbl2  25514  uniioombllem3  25542  vitalilem2  25566  vitalilem3  25567  mbfss  25603  i1faddlem  25650  i1fmullem  25651  mbfi1fseqlem2  25673  mbfi1fseqlem4  25675  mbfi1fseq  25678  itg2splitlem  25705  itg2split  25706  itg2monolem1  25707  itg2gt0  25717  isibl  25722  iblss2  25763  itgss3  25772  itgsplit  25793  ellimc  25830  limcmo  25839  cnlimc  25845  limciun  25851  limcun  25852  eldv  25855  dvbsss  25859  dvreslem  25866  elcpn  25892  dvaddf  25901  dvmulf  25902  dvcof  25908  rolle  25950  dvlip2  25956  dvivthlem1  25969  lhop1  25975  lhop2  25976  ftc1cn  26006  fta1glem2  26130  plyco0  26153  elply  26156  ply1termlem  26164  eltayl  26323  tayl0  26325  taylplem1  26326  taylplem2  26327  dvtaylp  26334  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  abelth  26407  cxpcn3  26714  rlimcnp  26931  fsumharmonic  26978  dchrelbas  27203  pntrsumbnd2  27534  ostth2lem2  27601  nolesgn2ores  27640  nogesgn1ores  27642  nosupprefixmo  27668  noinfprefixmo  27669  nosupcbv  27670  nosupdm  27672  nosupfv  27674  nosupres  27675  nosupbnd1lem1  27676  nosupbnd1lem3  27678  nosupbnd1lem5  27680  nosupbnd2lem1  27683  noinfcbv  27685  noinfdm  27687  noinffv  27689  noinfres  27690  noinfbnd1lem1  27691  noinfbnd1lem3  27693  noinfbnd1lem5  27695  noinfbnd2lem1  27698  elmade  27853  elold  27855  sltsleft  27856  sltsright  27857  oldlim  27883  madebday  27896  newbday  27898  ltslpss  27904  bdayiun  27911  cofcutr  27920  cofcutrtime  27923  lrrecval  27935  lrrecval2  27936  addsval  27958  precsexlem9  28211  precsexlem11  28213  ltonold  28257  onnolt  28262  onlts  28263  noseqrdgfn  28302  istrkgb  28527  istrkgcb  28528  istrkge  28529  istrkgl  28530  istrkgld  28531  axtgsegcon  28536  axtg5seg  28537  axtgbtwnid  28538  axtgpasch  28539  axtgupdim2  28543  axtgeucl  28544  tgdim01  28579  iscgrg  28584  isismt  28606  tglnunirn  28620  tglngval  28623  tgellng  28625  legval  28656  legov  28657  legov2  28658  ishlg  28674  mirreu3  28726  mirval  28727  mirfv  28728  mircgr  28729  mirbtwn  28730  ismir  28731  mireq  28737  symquadlem  28761  israg  28769  perpln1  28782  perpln2  28783  isperp  28784  islnopp  28811  outpasch  28827  ishpg  28831  iscgra  28881  dfcgra2  28902  isinag  28910  isleag  28919  iseqlg  28939  f1otrgitv  28942  f1otrg  28943  f1otrge  28944  ttgval  28947  ttgelitv  28955  elee  28966  brbtwn  28972  brcgr  28973  axlowdimlem16  29030  ebtwntg  29055  elntg2  29058  upgrex  29165  edgupgr  29207  upgredg  29210  edglnl  29216  numedglnl  29217  uhgr2edg  29281  umgr2edg1  29284  usgredg2vlem1  29298  usgredg2vlem2  29299  ushgredgedg  29302  ushgredgedgloop  29304  uhgrspansubgrlem  29363  fusgrfisstep  29402  nbgrval  29409  nbgrel  29413  nbupgrel  29418  nbgr2vtx1edg  29423  nbuhgr2vtx1edgblem  29424  nbuhgr2vtx1edgb  29425  nbusgreledg  29426  usgrnbcnvfv  29438  uvtxval  29460  uvtxel  29461  uvtx01vtx  29470  uvtxusgrel  29476  nbcplgr  29507  cplgr3v  29508  cusgrexi  29516  structtocusgr  29519  vtxdgfval  29541  vtxdg0v  29547  vtxdeqd  29551  vtxdun  29555  1loopgrnb0  29576  1loopgrvd0  29578  1hevtxdg0  29579  1hevtxdg1  29580  1egrvtxdg1  29583  umgr2v2evtxel  29596  umgr2v2enb1  29600  umgr2v2evd2  29601  vtxdginducedm1lem4  29616  vtxdginducedm1  29617  finsumvtxdg2sstep  29623  ewlksfval  29675  isewlk  29676  wksfval  29683  iswlk  29684  uspgr2wlkeq  29719  wlkres  29742  dfpth2  29802  usgr2pthlem  29836  clwlkcompim  29853  uspgrn2crct  29881  wwlks  29908  iswwlksn  29911  wwlknvtx  29918  wlkiswwlks2  29948  wwlksm1edg  29954  wwlksnred  29965  wwlksnext  29966  wwlksnredwwlkn  29968  wwlksnredwwlkn0  29969  wwlksnwwlksnon  29988  wspn0  29997  usgr2wspthons3  30040  rusgrnumwwlkb0  30047  clwwlk  30058  clwwlkccatlem  30064  clwlkclwwlklem2a4  30072  clwlkclwwlk  30077  clwwisshclwwslem  30089  clwwlkinwwlk  30115  clwwlkel  30121  clwwlkf  30122  clwwlkext2edg  30131  wwlksext2clwwlk  30132  wwlksubclwwlk  30133  clwwnisshclwwsn  30134  eleclclwwlknlem2  30136  erclwwlknsym  30145  erclwwlkntr  30146  umgrhashecclwwlk  30153  clwwlkvbij  30188  eupth2lem3lem3  30305  eupth2lem3lem4  30306  eupth2lem3lem6  30308  eupth2lemb  30312  eucrct2eupth  30320  fusgreg2wsplem  30408  2clwwlklem  30418  2clwwlk2clwwlklem  30421  2clwwlkel  30424  2clwwlk2clwwlk  30425  extwwlkfabel  30428  clwwlknonclwlknonf1o  30437  dlwwlknondlwlknonf1olem1  30439  numclwwlk2lem1  30451  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  ex-res  30516  isssp  30799  sspn  30811  islno  30828  isblo  30857  nmlno0  30870  ishmo  30886  dipdir  30917  dipass  30920  ubthlem1  30945  ubthlem2  30946  htthlem  30992  htth  30993  ocel  31356  ocnel  31373  shsel  31389  shsel2  31397  shmodsi  31464  pjhtheu  31469  pjeq  31474  axpjpj  31495  pjoc2  31514  elspani  31618  h1de2ctlem  31630  elspansn  31641  elspansn2  31642  elnlfn  32003  eleigvec  32032  riesz3i  32137  cbviunf  32630  iuneq12daf  32631  iunrdx  32638  iunrnmptss  32640  cbvdisjf  32646  disjorf  32654  disjabrex  32657  disjabrexf  32658  iundisjf  32664  disjrdx  32666  brab2d  32683  fresunsn  32703  2ndresdju  32727  abfmpunirn  32730  abfmpeld  32732  abfmpel  32733  fmptcof2  32735  acunirnmpt2  32738  acunirnmpt2f  32739  aciunf1lem  32740  funcnvmpt  32745  suppss3  32802  fpwrelmap  32812  xrofsup  32847  iundisjfi  32876  eliccioo  33012  s3f1  33029  ccatf1  33031  ccatws1f1o  33033  swrdrn3  33037  ismnt  33065  mgcoval  33068  gsummpt2co  33131  gsumpart  33146  gsumhashmul  33150  gsummulsubdishift1  33151  xrge0tsmsbi  33156  gsumwrd2dccatlem  33159  gsumwrd2dccat  33160  cycpmco2  33215  cyc3co2  33222  isfxp  33250  cntrval2  33253  inftmrel  33262  isinftm  33263  isslmd  33284  urpropd  33313  elrgspn  33328  erlval  33340  rlocval  33341  rloccring  33352  rloc1r  33354  domnprodeq0  33358  domnpropd  33359  isdrng4  33377  fracfld  33390  resv1r  33420  ellspds  33449  ellpi  33454  lbslsp  33458  rhmimaidl  33513  isprmidl  33519  qsidomlem1  33533  qsidomlem2  33534  ismxidl  33543  crngmxidl  33550  drng0mxidl  33557  opprqus0g  33571  qsfld  33579  isrprm  33598  rsprprmprmidlb  33604  ressply1evls1  33646  ply1mulrtss  33663  ply1coedeg  33670  dimpropd  33765  lbslsat  33773  extdg1id  33823  fldextrspunlsplem  33830  fldextrspunlsp  33831  elirng  33843  ply1annidllem  33858  constrsuc  33895  constrconj  33902  constrllcllem  33909  constrlccllem  33910  constrcccllem  33911  nn0constr  33918  smatrcl  33953  smatcl  33959  ist0cld  33990  txomap  33991  locfinreflem  33997  zarclsiin  34028  zart0  34036  rhmpreimacnlem  34041  metidval  34047  cnre2csqima  34068  ordtrest2NEW  34080  fmcncfil  34088  fsumcvg4  34107  ofcfval  34255  measvuni  34371  meascnbl  34376  faeval  34403  ismbfm  34408  elunirnmbfm  34409  imambfm  34419  elcarsg  34462  itgeq12dv  34483  issibf  34490  eulerpartlems  34517  eulerpartlemgc  34519  eulerpartlemgvv  34533  eulerpartlemgu  34534  eulerpart  34539  rrvmbfm  34599  elorvc  34617  elorrvc  34621  dstfrvunirn  34632  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemsima  34673  ballotlemrv  34677  fzssfzo  34696  signstfvn  34726  signstfvneq0  34729  signstres  34732  repr0  34768  reprinrn  34775  reprdifc  34784  hgt750lemg  34811  hgt750lemb  34813  istrkg2d  34823  axtgupdim2ALTV  34825  afsval  34828  brafs  34829  bnj945  34929  bnj1400  34991  bnj18eq1  35083  bnj916  35089  bnj1014  35117  bnj1015  35118  bnj1110  35138  bnj1417  35197  rankval2b  35255  r1filimi  35259  r1ssel  35263  onvf1odlem3  35299  vonf1owev  35302  revpfxsfxrev  35310  cplgredgex  35315  pfxwlk  35318  revwlk  35319  subfacp1lem2b  35375  subfacp1lem4  35377  subfacp1lem5  35378  subfacp1lem6  35379  ptpconn  35427  cvmscbv  35452  iscvm  35453  cvmsi  35459  cvmsval  35460  cvmliftmolem1  35475  cvmlift2lem12  35508  cvmlift2lem13  35509  cvmlift3lem7  35519  snmlval  35525  satfv1  35557  satfvsucsuc  35559  satfrnmapom  35564  satf0op  35571  satf0n0  35572  sat1el2xp  35573  fmlafvel  35579  isfmlasuc  35582  fmlaomn0  35584  gonan0  35586  goaln0  35587  gonar  35589  goalr  35591  satffunlem1lem2  35597  satffunlem2lem2  35600  satfv0fvfmla0  35607  satef  35610  satefvfmla0  35612  sategoelfvb  35613  satfv1fvfmla1  35617  mrsubfval  35702  mrsubvrs  35716  mclsrcl  35755  mclsval  35757  mppsval  35766  mclsppslem  35777  opelco3  35969  wsuclem  36017  funtransport  36225  fvtransport  36226  brcolinear  36253  colineardim1  36255  funray  36334  fvray  36335  funline  36336  fvline  36338  lineelsb2  36342  fwddifval  36356  fwddifnval  36357  rankelg  36362  rankeq1o  36365  elhf2  36369  0hf  36371  rmoeqbidv  36407  disjeq12dv  36409  ixpeq12dv  36410  prodeq12sdv  36412  itgeq12sdv  36413  cbvralvw2  36420  cbvrexvw2  36421  cbvrmovw2  36422  cbvreuvw2  36423  cbvcsbvw2  36425  cbviunvw2  36426  cbviinvw2  36427  cbvmptvw2  36428  cbvdisjvw2  36429  cbvmpo1vw2  36437  cbvmpo2vw2  36438  cbvsbcdavw  36451  cbvcsbdavw  36453  cbvcsbdavw2  36454  cbviundavw  36456  cbviindavw  36457  cbvdisjdavw  36462  cbvrabdavw2  36479  cbviundavw2  36480  cbviindavw2  36481  cbvmptdavw2  36482  cbvdisjdavw2  36483  cbvriotadavw2  36484  cbvmpo1davw2  36486  cbvmpo2davw2  36487  cbvsumdavw2  36489  neibastop2lem  36554  neibastop3  36556  eltail  36568  bj-projeq  37193  bj-projval  37197  bj-restsn  37287  opelopabbv  37348  brabd0  37352  bj-eldiag  37381  bj-eldiag2  37382  mptsnunlem  37543  dissneqlem  37545  iooelexlt  37567  relowlssretop  37568  rdgellim  37581  exrecfnlem  37584  finxpeq1  37591  finxpreclem6  37601  pibp21  37620  curf  37799  uncf  37800  curunc  37803  unccur  37804  fin2so  37808  lindsadd  37814  lindsdom  37815  lindsenlbs  37816  matunitlindflem1  37817  matunitlindflem2  37818  matunitlindf  37819  ptrest  37820  ptrecube  37821  poimirlem2  37823  poimirlem8  37829  poimirlem17  37838  poimirlem18  37839  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem24  37845  poimirlem26  37847  poimirlem29  37850  heicant  37856  mblfinlem1  37858  mblfinlem2  37859  volsupnfl  37866  itg2addnclem  37872  itg2gt0cn  37876  indexdom  37935  incsequz  37949  istotbnd  37970  istotbnd3  37972  0totbnd  37974  sstotbnd  37976  sstotbnd3  37977  isbnd  37981  prdstotbnd  37995  cntotbnd  37997  isismty  38002  heibor1lem  38010  heiborlem2  38013  heiborlem3  38014  heibor  38022  isass  38047  exidcl  38077  exidreslem  38078  elghomlem2OLD  38087  rngoidmlem  38137  rngo1cl  38140  divrngcl  38158  isdrngo2  38159  isrngohom  38166  isrngoiso  38179  isriscg  38185  iscom2  38196  iscringd  38199  isidl  38215  ispridl  38235  ismaxidl  38241  ac6s6  38373  dmecd  38503  dfpre4  38654  releldmqs  38917  releldmqscoss  38919  erimeq2  38937  eldisjlem19  39069  membpartlem19  39070  prter3  39142  islshp  39239  islsat  39251  lcvfbr  39280  islfl  39320  ellkr  39349  islshpkrN  39380  ldual1dim  39426  isopos  39440  cmtfvalN  39470  cvrfval  39528  isat  39546  islln  39766  islpln  39790  islvol  39833  isline  39999  ispointN  40002  ispsubsp  40005  elpmap  40018  elpmapat  40024  elpadd  40059  paddclN  40102  elpclN  40152  elpcliN  40153  pclfinN  40160  pclcmpatN  40161  ispsubclN  40197  iswatN  40254  islhp  40256  islaut  40343  ispautN  40359  isldil  40370  isltrn  40379  isdilN  40414  istrnN  40417  istendo  41020  dvhb1dimN  41246  erng1lem  41247  erngdvlem4-rN  41259  diaelval  41293  diaeldm  41296  dia1dimid  41323  cdlemm10N  41378  dibopelvalN  41403  dibopelval2  41405  dibelval3  41407  dibelval1st  41409  dibelval2nd  41412  dibeldmN  41418  dibvalrel  41423  dibglbN  41426  dicffval  41434  dicfval  41435  dicopelval  41437  dicelvalN  41438  dicelval3  41440  dicvalrelN  41445  dicelval1sta  41447  diclspsn  41454  dihopelvalbN  41498  dihopelvalcqat  41506  dihopelvalcpre  41508  dihvalrel  41539  dih1  41546  dihmeetlem4preN  41566  dihmeetlem13N  41579  dih1dimatlem  41589  dochnel2  41652  dihjatcclem4  41681  dvh2dim  41705  dvh3dim  41706  dvh4dimN  41707  dochfln0  41737  lpolsetN  41742  islpolN  41743  lcfrvalsnN  41801  lcfrlem21  41823  lcfrlem27  41829  lcfrlem37  41839  lcfr  41845  lcdlss  41879  mapdcv  41920  hdmap1fval  42056  hdmapffval  42086  hdmapfval  42087  hdmapval  42088  hgmapffval  42145  hgmapfval  42146  hdmapellkr  42174  hlhilhillem  42220  fzsplitnd  42236  isprimroot  42347  primrootsunit1  42351  primrootscoprmpow  42353  primrootscoprbij  42356  aks6d1c1p2  42363  aks6d1c1p3  42364  aks6d1c1p4  42365  aks6d1c1p5  42366  aks6d1c1p6  42368  aks6d1c1  42370  evl1gprodd  42371  sticksstones11  42410  sticksstones12a  42411  rhmqusspan  42439  grpods  42448  fzosumm1  42505  frlmfielbas  42755  frlmsnic  42795  psrmnd  42798  isnacs  42946  mrefg2  42949  elmzpcl  42968  mzpcompact2  42994  eldiophb  42999  elpell1qr  43089  elpell14qr  43091  elpell1234qr  43093  pw2f1ocnv  43279  pw2f1o2val2  43282  aomclem4  43299  aomclem6  43301  islssfg2  43313  imasgim  43342  lnr2i  43358  elmnc  43378  rngunsnply  43411  onexomgt  43483  onexlimgt  43485  onexoegt  43486  oaordnr  43538  omnord1  43547  oenord1  43558  cantnfresb  43566  tfsconcatun  43579  tfsconcat0i  43587  ofoaf  43597  naddcnff  43604  naddcnffo  43606  naddcnfcom  43608  naddcnfid1  43609  naddcnfid2  43610  naddcnfass  43611  naddwordnexlem4  43643  fiinfi  43814  sqrtcvallem1  43872  elintima  43894  eliunov2  43920  ov2ssiunov2  43941  brtrclfv2  43968  rfovcnvf1od  44245  rfovcnvfvd  44248  fsovrfovd  44250  fsovfvd  44251  fsovcnvlem  44254  ntrclsfv1  44296  ntrclselnel1  44298  ntrclsneine0lem  44305  ntrneifv1  44320  ntrneifv2  44321  ntrneiel  44322  gneispace2  44373  gneispacess2  44387  extoimad  44405  mnringelbased  44458  dvconstbi  44575  bccbc  44586  wfac8prim  45243  permaxrep  45247  permac8prim  45255  eliin2f  45348  iineq12dv  45350  rabbida2  45376  disjinfi  45436  unirnmap  45452  elmptima  45502  iuneqfzuzlem  45579  iooiinioc  45802  fsumiunss  45821  fsumsupp0  45824  lptre2pt  45884  icccncfext  46131  cncfiooicclem1  46137  dvnprodlem2  46191  stoweidlem27  46271  stoweidlem29  46273  stoweidlem31  46275  stoweidlem34  46278  stoweidlem48  46292  stoweidlem59  46303  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem2  46353  fourierdlem3  46354  fourierdlem25  46376  fourierdlem32  46383  fourierdlem33  46384  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem62  46412  fourierdlem70  46420  fourierdlem80  46430  fourierdlem92  46442  fourierdlem93  46443  fourierdlem101  46451  etransclem37  46515  sge0val  46610  sge0f1o  46626  sge0iunmptlemre  46659  sge0iunmpt  46662  iundjiun  46704  caragenel  46739  ovncvrrp  46808  ovnsubaddlem1  46814  ovnsubadd  46816  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  hoidmvle  46844  ovncvr2  46855  hspdifhsp  46860  hoiqssbl  46869  hspmbllem2  46871  hspmbl  46873  opnvonmbllem1  46876  isvonmbl  46882  ovnovollem1  46900  issmflem  46971  smflimlem3  47017  smflimlem4  47018  smflim  47021  smfmullem2  47036  smflimmpt  47054  smfsuplem1  47055  smflimsuplem1  47064  smflimsuplem3  47066  smflimsuplem4  47067  smflimsuplem7  47070  smflimsup  47072  chnsubseq  47124  fcores  47313  fcoresf1  47315  afvelrnb  47409  afvelrnb0  47410  afv2co2  47503  el1fzopredsuc  47571  iccpart  47662  iccpartgtprec  47666  iccpartiltu  47668  iccpartigtl  47669  iccpartltu  47671  iccpartgtl  47672  iccpartgt  47673  iccpartleu  47674  iccpartgel  47675  iccelpart  47679  iccpartiun  47680  icceuelpart  47682  fargshiftfv  47685  fargshiftfo  47688  sprel  47730  prprelb  47762  prprelprb  47763  fpprel  47974  sbgoldbo  48033  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  bgoldbtbndlem3  48053  bgoldbtbnd  48055  clnbgrval  48068  elclnbgrelnbgr  48071  clnbgrel  48074  clnbupgrel  48080  vopnbgrel  48100  isubgredg  48112  upgrimwlklem3  48145  upgrimwlklem5  48147  upgrimpths  48155  grtriprop  48187  isgrtri  48189  grtriclwlk3  48191  stgredgel  48203  gpgvtxel  48293  gpgiedgdmel  48295  gpgedgel  48296  opgpgvtx  48301  gpg5nbgrvtx13starlem1  48317  gpg5nbgrvtx13starlem2  48318  gpg5nbgrvtx13starlem3  48319  gpg3kgrtriex  48335  grlimedgnedg  48377  upwlksfval  48381  isupwlk  48382  intop  48449  isclintop  48453  assintop  48455  isassintop  48456  assintopcllaw  48458  uzlidlring  48481  elrngchomALTV  48515  rngccatidALTV  48518  rngcsectALTV  48521  rngcisoALTV  48523  rhmsubcALTVlem3  48529  rhmsubcALTVlem4  48530  funcringcsetcALTV2lem7  48542  funcringcsetcALTV2lem9  48544  elringchomALTV  48549  ringccatidALTV  48552  ringcsectALTV  48555  ringcisoALTV  48557  ringcbasbasALTV  48558  funcringcsetclem7ALTV  48565  funcringcsetclem9ALTV  48567  srhmsubcALTV  48571  cbvmpox2  48582  ply1sclrmsm  48630  dmatALTbasel  48648  lcoval  48658  lindslinindsimp1  48703  lindslinindsimp2  48709  lmod1  48738  elbigo  48797  elbigo2  48798  elbigolo1  48803  dig2nn0ld  48850  naryfvalel  48876  rrxlines  48979  rrxlinesc  48981  rrxlinec  48982  eenglngeehlnm  48985  elrrx2linest2  48991  rrxsphere  48994  itsclc0  49017  itsclc0b  49018  itsclinecirc0  49019  itsclinecirc0b  49020  itscnhlinecirc02p  49031  brab2dd  49073  f1omo  49138  f1omoOLD  49139  lubeldm2d  49203  glbeldm2d  49204  catprs  49256  sectpropdlem  49281  nelsubc3lem  49315  initc  49336  imaid  49399  upfval  49421  upfval2  49422  upfval3  49423  uppropd  49426  oppcinito  49480  oppctermo  49481  oppczeroo  49482  initopropd  49488  termopropd  49489  isthinc  49664  isthincd2lem1  49670  thincmoALT  49674  thincmod  49675  isthincd  49681  thincpropd  49687  indcthing  49705  discthing  49706  prsthinc  49709  termcterm  49758  termc2  49763  isinito4  49792  2arwcatlem1  49840  setc1onsubc  49847  cnelsubclem  49848  ranval3  49876  lmdfval2  49900  cmdfval2  49901  termolmd  49915  elsetrecslem  49944