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 635	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1835	. . 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 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114

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

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

This theorem is referenced by:  eleq2  2825  eleq12d  2830  eleqtrd  2838  neleqtrd  2858  eqabrd  2877  raleqbidv  3311  rexeqbidv  3312  reueqbidv  3378  rabeqbidva  3405  elabd2  3612  sbcbid  3783  sbcbi2  3787  csbeq2d  3843  csbeq2dv  3844  cbvcsbw  3847  cbvcsb  3848  cbvcsbv  3849  csbie  3872  csbied  3873  csbie2g  3877  cbvralcsf  3879  cbvreucsf  3881  cbvrabcsf  3882  sbcel12  4351  sbcel1g  4356  sbcel2  4358  prel12g  4807  eliuni  4939  iuneqconst  4945  iuneq12df  4960  iuneq12d  4963  cbviun  4977  cbviin  4978  cbviung  4979  cbviing  4980  cbviunv  4981  cbviinv  4982  iinxsng  5030  iinxprg  5031  iunxsng  5032  iunxsngf  5034  cbvdisj  5062  cbvdisjv  5063  disjor  5067  disjiund  5076  mpteq12da  5168  mpteq12f  5170  mpteq12dva  5171  axpweq  5292  rabxfrd  5359  rbropapd  5517  opeliunxp  5698  opeliun2xp  5699  opeliunxp2  5793  iunxpf  5803  elimampt  6008  elrelimasn  6051  elimasni  6056  imadifssran  6115  xpdifid  6132  ressn  6249  funfni  6604  fnbr  6606  dffv3  6836  elfv2ex  6883  fvelrnb  6900  foelcdmi  6901  fvun1  6931  fvco2  6937  funcnvmpt  6949  elfvmptrab1w  6975  elfvmptrab1  6976  elfvmptrab  6977  elpreima  7010  dff3  7052  fmptco  7082  fnelfp  7130  fnelnfp  7132  tpres  7156  fnprb  7163  fntpb  7164  funfvima3  7191  eluniima  7205  dff13  7209  f1ounsn  7227  f1eqcocnv  7256  isoini  7293  riotaeqdv  7325  mpoeq123dva  7441  cbvmpox  7460  elimampo  7504  ovelrn  7543  elovmpod  7611  elovmpo  7612  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  elovmpt3rab1  7627  fiun  7896  f1iun  7897  zfrep6OLD  7908  fmpox  8020  el2mpocsbcl  8035  el2mpocl  8036  bropopvvv  8040  bropfvvvv  8042  xpord2indlem  8097  xpord3inddlem  8104  elsuppfng  8119  elsuppfn  8120  suppfnss  8139  opeliunxp2f  8160  mpoxopn0yelv  8163  mpoxopovel  8170  rntpos  8189  mpocurryd  8219  fpr2  8254  wfr2  8277  onoviun  8283  smoel  8300  smoiso  8302  smoel2  8303  smo11  8304  tfrlem9  8324  oalimcl  8495  oaass  8496  omordi  8501  omordlim  8512  omlimcl  8513  odi  8514  omeulem1  8517  omeulem2  8518  oen0  8522  oeordi  8523  oeordsuc  8530  oelimcl  8536  oeeulem  8537  oeeui  8538  nnmordi  8567  oaabs2  8585  omabs  8587  omsmolem  8593  ereldm  8697  iiner  8736  elmapg  8786  elpmg  8790  elixpsn  8885  ixpsnf1o  8886  boxriin  8888  omxpenlem  9016  pw2f1olem  9019  phplem2  9139  php3  9143  infn0  9212  elfi  9326  dffi3  9344  marypha2lem2  9349  ordiso2  9430  wemapsolem  9465  elharval  9476  inf3lemd  9548  inf3lem1  9549  inf3lem2  9550  inf3lem3  9551  cantnfs  9587  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1  9610  ttrclselem2  9647  trcl  9649  frr2  9684  r1sdom  9698  r1ordg  9702  r1pwss  9708  tz9.12lem3  9713  tz9.12  9714  r1elwf  9720  rankr1ai  9722  rankidb  9724  rankr1bg  9727  rankval2  9742  rankunb  9774  tcrank  9808  acni  9967  acni2  9968  acndom  9973  infpwfien  9984  alephnbtwn  9993  cardaleph  10011  cardinfima  10019  iunfictbso  10036  dfac3  10043  dfac5lem5  10049  dfac5  10051  dfac9  10059  dfac12r  10069  kmlem2  10074  kmlem12  10084  kmlem13  10085  kmlem14  10086  ackbij2lem3  10162  ackbij2  10164  cofsmo  10191  alephsing  10198  fin23lem30  10264  isf32lem9  10283  itunisuc  10341  axcc2lem  10358  axcc3  10360  domtriomlem  10364  axdc2lem  10370  axdc2  10371  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  ac6c4  10403  zorn2lem1  10418  ttukeylem6  10436  pwcfsdom  10506  axregndlem2  10526  axinfndlem1  10528  axacndlem4  10533  axacnd  10535  pwfseqlem1  10581  inar1  10698  inatsk  10701  gruurn  10721  grur1  10743  eltskm  10766  genpelv  10923  eluz1  12792  elixx1  13307  elixx3g  13311  elioo2  13339  elfz1  13466  elfz2  13468  elfzp1  13528  fzpr  13533  fzsuc2  13536  fzrev3  13544  elfzp12  13557  fzm1  13561  elfzo  13615  fz0add1fz1  13690  elfzo0l  13711  elfzom1b  13721  fzosplitsni  13734  elfzr  13736  elfzlmr  13737  zmodidfzo  13859  seqp1  13978  seqf1o  14005  bcval  14266  bcpasc  14283  hashf1lem1  14417  fundmge2nop0  14464  wrdmap  14508  elovmpowrd  14520  ccatfval  14535  elfzelfzccat  14542  ccatlid  14549  ccatass  14551  ccatrn  14552  ccatalpha  14556  swrdfv2  14624  ccatswrd  14631  swrdccat2  14632  pfxfv  14645  pfxeq  14658  ccatpfx  14663  swrdswrd  14667  swrdpfx  14669  pfxpfx  14670  cats1un  14683  swrdccatfn  14686  swrdccatin1  14687  pfxccatin12lem4  14688  pfxccatin12lem1  14690  swrdccatin2  14691  pfxccatin12lem2c  14692  pfxccatin12lem2  14693  swrdccat3blem  14701  swrdccatin1d  14705  swrdccatin2d  14706  pfxccatin12d  14707  revccat  14728  revrev  14729  repswpfx  14747  repswccat  14748  cshwidxmod  14765  2cshw  14775  cshwcshid  14789  cshwcsh2id  14790  cshimadifsn  14791  cshimadifsn0  14792  revco  14796  ccatco  14797  cshco  14798  swrdco  14799  ofccat  14931  shftfn  15035  shftval  15036  limsupgle  15439  ello12  15478  elo12  15489  isercolllem3  15629  sumeq1  15651  fsumsplit  15703  sumsplit  15730  fsum2dlem  15732  fsumcom2  15736  fsumparts  15769  explecnv  15830  pwdif  15833  fprodser  15914  fprodsplit  15931  fprod2dlem  15945  fprodcom2  15949  eftlub  16076  divalgmod  16375  bitsval  16393  bitsp1e  16401  bitsp1o  16402  sadfval  16421  sadcp1  16424  sadval  16425  sadcadd  16427  sadadd2  16429  saddisjlem  16433  sadadd  16436  sadass  16440  smufval  16446  smuval  16450  smuval2  16451  smupvallem  16452  smu01lem  16454  smueqlem  16459  smumul  16462  bezoutlem2  16509  bezoutlem4  16511  algfx  16549  eucalgcvga  16555  reumodprminv  16775  nnnn0modprm0  16777  unbenlem  16879  prmreclem5  16891  vdwapval  16944  vdwapun  16945  vdwnnlem1  16966  vdwnn  16969  ramval  16979  0ram  16991  ramub1lem2  16998  prmgaplem7  17028  prmlem0  17076  elrest  17390  prdsbasmpt  17433  prdsleval  17440  prdsbasmpt2  17445  pwselbasb  17451  imasaddfnlem  17492  imasvscafn  17501  divsfval  17511  ismre  17552  mreunirn  17563  mrisval  17596  ismri  17597  isacs  17617  catidd  17646  iscatd2  17647  ismon  17700  isepi  17707  sectffval  17717  sectfval  17718  dfiso2  17739  cicsym  17771  issubc  17802  catsubcat  17806  isfunc  17831  funcres  17863  funcpropd  17869  ffthiso  17898  isnat  17917  isnat2  17918  fuciso  17945  initoval  17960  termoval  17961  isinito  17963  istermo  17964  iszeroo  17965  isinitoi  17966  istermoi  17967  initoid  17968  termoid  17969  iszeroi  17976  2initoinv  17977  initoeu1  17978  initoeu2  17983  2termoinv  17984  termoeu1  17985  arwhoma  18012  elsetchom  18048  setcmon  18054  setcepi  18055  setciso  18058  catciso  18078  elestrchom  18094  estrcbasbas  18097  funcestrcsetclem7  18112  funcestrcsetclem8  18113  funcestrcsetclem9  18114  fthestrcsetc  18116  fullestrcsetc  18117  equivestrcsetc  18118  setc1strwun  18119  funcsetcestrclem7  18127  funcsetcestrclem8  18128  funcsetcestrclem9  18129  fthsetcestrc  18131  fullsetcestrc  18132  hofcl  18225  hofpropd  18233  yonedalem4c  18243  yonedainv  18247  yonffthlem  18248  lubeldm  18317  glbeldm  18330  joindef  18340  meetdef  18354  poslubdg  18378  acsficl2d  18518  acsmapd  18520  psref  18540  psss  18546  dirge  18569  chnccats1  18591  chnccat  18592  chnrev  18593  mgmpropd  18619  issstrmgm  18621  grpidval  18629  grpidpropd  18630  grpidd  18639  ismgmhm  18664  issubmgm  18670  issgrpd  18698  sgrppropd  18699  ismndd  18724  mndpropd  18727  imasmnd2  18742  imasmnd  18743  xpsmnd0  18746  ismhm  18753  issubm  18771  gsumsgrpccat  18808  elefmndbas2  18842  smndex1mndlem  18880  imasgrp2  19031  imasgrp  19032  issubg  19102  subginv  19109  isnsg  19130  eqg0el  19158  quselbas  19159  isghm  19190  isghmOLD  19191  resghm2b  19209  conjnmzb  19228  conjnsg  19229  ghmpropd  19231  isga  19266  elcntz  19297  elcntzsn  19300  cntzrcl  19302  resscntz  19308  symgextf1  19396  gsmsymgreqlem2  19406  f1otrspeq  19422  pmtrfrn  19433  pmtrdifellem3  19453  pmtrdifellem4  19454  psgnunilem1  19468  psgnunilem5  19469  psgnunilem2  19470  psgnunilem3  19471  psgneldm2  19479  psgnfitr  19492  psgnsn  19495  gexdvds  19559  gex1  19566  isslw  19583  sylow3lem2  19603  lsmelvalx  19615  pj1ghm  19678  efgtlen  19701  efgsfo  19714  efgredlemc  19720  frgp0  19735  frgpmhm  19740  qusabl  19840  frgpnabllem1  19848  imasabl  19851  cycsubmcmn  19864  0cyg  19868  cycsubgcyg  19876  gsumval3  19882  gsumcllem  19883  gsumzaddlem  19896  gsumzsplit  19902  gsummptfzcl  19944  eldprd  19981  dprdcntz2  20015  dprd2d2  20021  dmdprdsplit2lem  20022  dmdprdsplit2  20023  dprdsplit  20025  ablfac2  20066  isrngd  20154  rngpropd  20155  imasrng  20158  qusrng  20161  ringurd  20166  isringd  20272  imasring  20310  xpsring1d  20313  dvdsrval  20341  isunit  20353  dvdsrpropd  20396  isirred  20399  isrnghm  20421  isrngim  20425  c0ghm  20441  c0snghm  20444  isrhm  20458  isrim0  20462  islring  20517  issubrng  20524  opprsubrng  20536  issubrg  20548  opprsubrg  20570  resrhm2b  20579  rhmpropd  20586  rnghmresel  20597  elrngchom  20601  rnghmsubcsetclem1  20608  rnghmsubcsetclem2  20609  rngcid  20612  rngcsect  20613  rngciso  20615  funcrngcsetcALT  20618  zrinitorngc  20619  zrtermorngc  20620  rhmresel  20626  elringchom  20630  rhmsubcsetclem1  20637  rhmsubcsetclem2  20638  ringcid  20641  rhmsscrnghm  20642  rhmsubcrngclem1  20643  rhmsubcrngclem2  20644  ringcsect  20647  ringciso  20649  ringcbasbas  20650  zrtermoringc  20652  srhmsubc  20657  rhmsubclem3  20664  rhmsubclem4  20665  drngunit  20711  isdrngd  20742  isdrngdOLD  20744  issdrg  20765  sdrgunit  20773  isabv  20788  issrngd  20832  islmod  20859  lmodprop2d  20919  islss  20929  islssd  20930  lssats2  20995  ellspsn  20998  islmhm  21022  lmhmf1o  21041  lmhmima  21042  lmhmpreima  21043  reslmhm  21047  pwssplit3  21056  lmhmpropd  21068  islbs  21071  lspprel  21089  lspfixed  21126  lbsacsbs  21154  lbsextlem1  21156  lbsextlem2  21157  lbsextlem3  21158  lbsextlem4  21159  ixpsnbasval  21203  isridlrng  21217  rnglidlmmgm  21243  isridl  21250  quscrng  21281  rngqiprngimfolem  21288  rngqiprngimf1lem  21292  rngqiprngimfo  21299  islpidl  21323  lidldvgen  21332  irinitoringc  21459  pzriprnglem13  21473  pzriprnglem14  21474  zrhrhmb  21490  znf1o  21531  frgpcyg  21553  psgnevpmb  21567  isphld  21634  phlssphl  21639  elocv  21648  iscss  21663  isobs  21700  obs2ss  21709  dsmmfi  21718  dsmmelbas  21719  dsmmlss  21724  frlmelbas  21736  frlmlbs  21777  frlmup1  21778  ellspd  21782  islinds  21789  islindf2  21794  f1lindf  21802  islindf4  21818  assamulgscmlem2  21880  psrgrp  21935  mplsubglem  21977  mpllsslem  21978  mplmonmul  22014  subrgascl  22044  subrgasclcl  22045  mpfind  22093  ismhp  22106  gsumply1subr  22197  lply1binomsc  22276  matbas2d  22388  matecl  22390  matvscl  22396  mat1  22412  mat0dim0  22432  mat0dimid  22433  mat0dimscm  22434  mat1dimelbas  22436  dmatel  22458  scmatel  22470  scmateALT  22477  scmataddcl  22481  scmatsubcl  22482  smatvscl  22489  scmatghm  22498  mat1scmat  22504  mdetunilem7  22583  mdetunilem9  22585  smadiadetr  22640  cramerimplem2  22649  cramer0  22655  pmatcoe1fsupp  22666  cpmatpmat  22675  cpmatel  22676  cpmatacl  22681  cpmatinvcl  22682  mat2pmatghm  22695  mat2pmatmul  22696  decpmatmullem  22736  pmatcollpwlem  22745  pmatcollpw3fi1lem1  22751  pmatcollpwscmatlem1  22754  monmat2matmon  22789  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  cayhamlem1  22831  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  cayhamlem2  22849  istopon  22877  eltg  22922  eltg2  22923  eltop  22939  eltop2  22940  eltop3  22941  pptbas  22973  iscld  22992  neiss2  23066  isnei  23068  neiptopnei  23097  neiptopreu  23098  lpfval  23103  lpval  23104  islp  23105  maxlp  23112  islpi  23114  neitr  23145  restlp  23148  ordtbas2  23156  ordtrest2  23169  lmfval  23197  cnfval  23198  iscn  23200  iscnp  23202  tgcn  23217  tgcnp  23218  lmbrf  23225  cnpresti  23253  ist1  23286  ist1-2  23312  cnt1  23315  haust1  23317  cmpfi  23373  cmpfii  23374  1stcfb  23410  2ndc1stc  23416  1stcrest  23418  2ndcdisj  23421  1stcelcls  23426  nllyi  23440  subislly  23446  islocfin  23482  lfinpfin  23489  locfindis  23495  locfincf  23496  comppfsc  23497  kgenval  23500  elkgen  23501  kgencn2  23522  txbas  23532  eltx  23533  ptval  23535  ptpjpre1  23536  ptopn2  23549  ptpjopn  23577  ptclsg  23580  xkoccn  23584  txdis  23597  txdis1cn  23600  ptrescn  23604  hausdiag  23610  hauseqlcld  23611  txhaus  23612  xkohaus  23618  elqtop  23662  qtopeu  23681  kqcldsat  23698  hmeofval  23723  ptuncnv  23772  ptunhmeo  23773  elmptrab  23792  fbdmn0  23799  elfg  23836  elfilss  23841  filunirn  23847  fixufil  23887  elfm  23912  rnelfmlem  23917  rnelfm  23918  fmfnfmlem4  23922  elflim2  23929  flimtopon  23935  elflim  23936  hausflim  23946  flimcls  23950  flfnei  23956  isflf  23958  hausflf  23962  cnpflf  23966  cnflf  23967  txflf  23971  isfcls  23974  fclstopon  23977  isfcls2  23978  fclssscls  23983  fclsnei  23984  fclsfnflim  23992  flimfnfcls  23993  isfcf  23999  fcfelbas  24001  cnpfcf  24006  cnfcf  24007  flfcntr  24008  alexsublem  24009  alexsubALTlem3  24014  cnextfun  24029  cnextfvval  24030  cnextf  24031  cnextcn  24032  tmdgsum2  24061  tgpconncomp  24078  ghmcnp  24080  qustgplem  24086  eltsms  24098  haustsms  24101  tsmsgsum  24104  tsmssubm  24108  tsmssplit  24117  isust  24169  ustbas  24192  elutop  24198  ustuqtoplem  24204  ustuqtop4  24209  ustuqtop  24211  utopsnneiplem  24212  utopsnneip  24213  utopsnnei  24214  isusp  24226  isucn  24242  ucncn  24249  iscfilu  24252  neipcfilu  24260  iscusp  24263  cnextucn  24267  ispsmet  24269  ismet  24288  isxmet  24289  elblps  24352  elbl  24353  elmopn  24407  prdsbl  24456  neibl  24466  met1stc  24486  metrest  24489  prdsxmslem2  24494  txmetcnp  24512  txmetcn  24513  metustsym  24520  cfilucfil2  24526  elbl4  24528  metuel  24529  psmetutop  24532  restmetu  24535  metucn  24536  tngngp  24619  isnmhm  24711  zcld  24779  metnrmlem1a  24824  elcncf  24856  cncfcnvcn  24892  cnheibor  24922  lebnumlem1  24928  ishtpy  24939  isphtpy  24948  om1elbas  24999  elpi1  25012  pi1xfr  25022  pi1coghm  25028  tcphcph  25204  lmmbrf  25229  iscfil  25232  iscau  25243  iscauf  25247  caucfil  25250  iscmet  25251  cmetcaulem  25255  iscmet3lem1  25258  iscmet3lem2  25259  iscmet3  25260  bcthlem1  25291  cmsss  25318  cmetcusp1  25320  cmetcusp  25321  cmscsscms  25340  rrxcph  25359  minveclem3b  25395  ovolfioo  25434  ovolficc  25435  ovolctb  25457  ovoliunnul  25474  ovolshftlem1  25476  sca2rab  25479  ovolscalem1  25480  ovolicc2lem1  25484  ovolicc2lem2  25485  ovolicc2lem4  25487  ovolicc2lem5  25488  iundisj  25515  iunmbl2  25524  uniioombllem3  25552  vitalilem2  25576  vitalilem3  25577  mbfss  25613  i1faddlem  25660  i1fmullem  25661  mbfi1fseqlem2  25683  mbfi1fseqlem4  25685  mbfi1fseq  25688  itg2splitlem  25715  itg2split  25716  itg2monolem1  25717  itg2gt0  25727  isibl  25732  iblss2  25773  itgss3  25782  itgsplit  25803  ellimc  25840  limcmo  25849  cnlimc  25855  limciun  25861  limcun  25862  eldv  25865  dvbsss  25869  dvreslem  25876  elcpn  25901  dvaddf  25909  dvmulf  25910  dvcof  25915  rolle  25957  dvlip2  25962  dvivthlem1  25975  lhop1  25981  lhop2  25982  ftc1cn  26010  fta1glem2  26134  plyco0  26157  elply  26160  ply1termlem  26168  eltayl  26325  tayl0  26327  taylplem1  26328  taylplem2  26329  dvtaylp  26335  taylthlem1  26338  taylthlem2  26339  abelth  26406  cxpcn3  26712  rlimcnp  26929  fsumharmonic  26975  dchrelbas  27199  pntrsumbnd2  27530  ostth2lem2  27597  nolesgn2ores  27636  nogesgn1ores  27638  nosupprefixmo  27664  noinfprefixmo  27665  nosupcbv  27666  nosupdm  27668  nosupfv  27670  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfcbv  27681  noinfdm  27683  noinffv  27685  noinfres  27686  noinfbnd1lem1  27687  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd2lem1  27694  elmade  27849  elold  27851  sltsleft  27852  sltsright  27853  oldlim  27879  madebday  27892  newbday  27894  ltslpss  27900  bdayiun  27907  cofcutr  27916  cofcutrtime  27919  lrrecval  27931  lrrecval2  27932  addsval  27954  precsexlem9  28207  precsexlem11  28209  ltonold  28253  onnolt  28258  onlts  28259  noseqrdgfn  28298  istrkgb  28523  istrkgcb  28524  istrkge  28525  istrkgl  28526  istrkgld  28527  axtgsegcon  28532  axtg5seg  28533  axtgbtwnid  28534  axtgpasch  28535  axtgupdim2  28539  axtgeucl  28540  tgdim01  28575  iscgrg  28580  isismt  28602  tglnunirn  28616  tglngval  28619  tgellng  28621  legval  28652  legov  28653  legov2  28654  ishlg  28670  mirreu3  28722  mirval  28723  mirfv  28724  mircgr  28725  mirbtwn  28726  ismir  28727  mireq  28733  symquadlem  28757  israg  28765  perpln1  28778  perpln2  28779  isperp  28780  islnopp  28807  outpasch  28823  ishpg  28827  iscgra  28877  dfcgra2  28898  isinag  28906  isleag  28915  iseqlg  28935  f1otrgitv  28938  f1otrg  28939  f1otrge  28940  ttgval  28943  ttgelitv  28951  elee  28962  brbtwn  28968  brcgr  28969  axlowdimlem16  29026  ebtwntg  29051  elntg2  29054  upgrex  29161  edgupgr  29203  upgredg  29206  edglnl  29212  numedglnl  29213  uhgr2edg  29277  umgr2edg1  29280  usgredg2vlem1  29294  usgredg2vlem2  29295  ushgredgedg  29298  ushgredgedgloop  29300  uhgrspansubgrlem  29359  fusgrfisstep  29398  nbgrval  29405  nbgrel  29409  nbupgrel  29414  nbgr2vtx1edg  29419  nbuhgr2vtx1edgblem  29420  nbuhgr2vtx1edgb  29421  nbusgreledg  29422  usgrnbcnvfv  29434  uvtxval  29456  uvtxel  29457  uvtx01vtx  29466  uvtxusgrel  29472  nbcplgr  29503  cplgr3v  29504  cusgrexi  29512  structtocusgr  29515  vtxdgfval  29536  vtxdg0v  29542  vtxdeqd  29546  vtxdun  29550  1loopgrnb0  29571  1loopgrvd0  29573  1hevtxdg0  29574  1hevtxdg1  29575  1egrvtxdg1  29578  umgr2v2evtxel  29591  umgr2v2enb1  29595  umgr2v2evd2  29596  vtxdginducedm1lem4  29611  vtxdginducedm1  29612  finsumvtxdg2sstep  29618  ewlksfval  29670  isewlk  29671  wksfval  29678  iswlk  29679  uspgr2wlkeq  29714  wlkres  29737  dfpth2  29797  usgr2pthlem  29831  clwlkcompim  29848  uspgrn2crct  29876  wwlks  29903  iswwlksn  29906  wwlknvtx  29913  wlkiswwlks2  29943  wwlksm1edg  29949  wwlksnred  29960  wwlksnext  29961  wwlksnredwwlkn  29963  wwlksnredwwlkn0  29964  wwlksnwwlksnon  29983  wspn0  29992  usgr2wspthons3  30035  rusgrnumwwlkb0  30042  clwwlk  30053  clwwlkccatlem  30059  clwlkclwwlklem2a4  30067  clwlkclwwlk  30072  clwwisshclwwslem  30084  clwwlkinwwlk  30110  clwwlkel  30116  clwwlkf  30117  clwwlkext2edg  30126  wwlksext2clwwlk  30127  wwlksubclwwlk  30128  clwwnisshclwwsn  30129  eleclclwwlknlem2  30131  erclwwlknsym  30140  erclwwlkntr  30141  umgrhashecclwwlk  30148  clwwlkvbij  30183  eupth2lem3lem3  30300  eupth2lem3lem4  30301  eupth2lem3lem6  30303  eupth2lemb  30307  eucrct2eupth  30315  fusgreg2wsplem  30403  2clwwlklem  30413  2clwwlk2clwwlklem  30416  2clwwlkel  30419  2clwwlk2clwwlk  30420  extwwlkfabel  30423  clwwlknonclwlknonf1o  30432  dlwwlknondlwlknonf1olem1  30434  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  ex-res  30511  isssp  30795  sspn  30807  islno  30824  isblo  30853  nmlno0  30866  ishmo  30882  dipdir  30913  dipass  30916  ubthlem1  30941  ubthlem2  30942  htthlem  30988  htth  30989  ocel  31352  ocnel  31369  shsel  31385  shsel2  31393  shmodsi  31460  pjhtheu  31465  pjeq  31470  axpjpj  31491  pjoc2  31510  elspani  31614  h1de2ctlem  31626  elspansn  31637  elspansn2  31638  elnlfn  31999  eleigvec  32028  riesz3i  32133  cbviunf  32625  iuneq12daf  32626  iunrdx  32633  iunrnmptss  32635  cbvdisjf  32641  disjorf  32649  disjabrex  32652  disjabrexf  32653  iundisjf  32659  disjrdx  32661  brab2d  32678  fresunsn  32698  2ndresdju  32722  abfmpunirn  32725  abfmpeld  32727  abfmpel  32728  fmptcof2  32730  acunirnmpt2  32733  acunirnmpt2f  32734  aciunf1lem  32735  suppss3  32796  fpwrelmap  32806  xrofsup  32840  iundisjfi  32869  eliccioo  32990  s3f1  33007  ccatf1  33009  ccatws1f1o  33011  swrdrn3  33015  ismnt  33043  mgcoval  33046  gsummpt2co  33109  gsumpart  33124  gsumhashmul  33128  gsummulsubdishift1  33129  xrge0tsmsbi  33135  gsumwrd2dccatlem  33138  gsumwrd2dccat  33139  cycpmco2  33194  cyc3co2  33201  isfxp  33229  cntrval2  33232  inftmrel  33241  isinftm  33242  isslmd  33263  urpropd  33292  elrgspn  33307  erlval  33319  rlocval  33320  rloccring  33331  rloc1r  33333  domnprodeq0  33337  domnpropd  33338  isdrng4  33356  fracfld  33369  resv1r  33399  ellspds  33428  ellpi  33433  lbslsp  33437  rhmimaidl  33492  isprmidl  33498  qsidomlem1  33512  qsidomlem2  33513  ismxidl  33522  crngmxidl  33529  drng0mxidl  33536  opprqus0g  33550  qsfld  33558  isrprm  33577  rsprprmprmidlb  33583  ressply1evls1  33625  ply1mulrtss  33642  ply1coedeg  33649  psrmonmul  33694  dimpropd  33753  lbslsat  33760  extdg1id  33810  fldextrspunlsplem  33817  fldextrspunlsp  33818  elirng  33830  ply1annidllem  33845  constrsuc  33882  constrconj  33889  constrllcllem  33896  constrlccllem  33897  constrcccllem  33898  nn0constr  33905  smatrcl  33940  smatcl  33946  ist0cld  33977  txomap  33978  locfinreflem  33984  zarclsiin  34015  zart0  34023  rhmpreimacnlem  34028  metidval  34034  cnre2csqima  34055  ordtrest2NEW  34067  fmcncfil  34075  fsumcvg4  34094  ofcfval  34242  measvuni  34358  meascnbl  34363  faeval  34390  ismbfm  34395  elunirnmbfm  34396  imambfm  34406  elcarsg  34449  itgeq12dv  34470  issibf  34477  eulerpartlems  34504  eulerpartlemgc  34506  eulerpartlemgvv  34520  eulerpartlemgu  34521  eulerpart  34526  rrvmbfm  34586  elorvc  34604  elorrvc  34608  dstfrvunirn  34619  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemsima  34660  ballotlemrv  34664  fzssfzo  34683  signstfvn  34713  signstfvneq0  34716  signstres  34719  repr0  34755  reprinrn  34762  reprdifc  34771  hgt750lemg  34798  hgt750lemb  34800  istrkg2d  34810  axtgupdim2ALTV  34812  afsval  34815  brafs  34816  bnj945  34916  bnj1400  34977  bnj18eq1  35069  bnj916  35075  bnj1014  35103  bnj1015  35104  bnj1110  35124  bnj1417  35183  rankval2b  35242  r1filimi  35246  r1ssel  35250  onvf1odlem3  35287  vonf1owev  35290  revpfxsfxrev  35298  cplgredgex  35303  pfxwlk  35306  revwlk  35307  subfacp1lem2b  35363  subfacp1lem4  35365  subfacp1lem5  35366  subfacp1lem6  35367  ptpconn  35415  cvmscbv  35440  iscvm  35441  cvmsi  35447  cvmsval  35448  cvmliftmolem1  35463  cvmlift2lem12  35496  cvmlift2lem13  35497  cvmlift3lem7  35507  snmlval  35513  satfv1  35545  satfvsucsuc  35547  satfrnmapom  35552  satf0op  35559  satf0n0  35560  sat1el2xp  35561  fmlafvel  35567  isfmlasuc  35570  fmlaomn0  35572  gonan0  35574  goaln0  35575  gonar  35577  goalr  35579  satffunlem1lem2  35585  satffunlem2lem2  35588  satfv0fvfmla0  35595  satef  35598  satefvfmla0  35600  sategoelfvb  35601  satfv1fvfmla1  35605  mrsubfval  35690  mrsubvrs  35704  mclsrcl  35743  mclsval  35745  mppsval  35754  mclsppslem  35765  opelco3  35957  wsuclem  36005  funtransport  36213  fvtransport  36214  brcolinear  36241  colineardim1  36243  funray  36322  fvray  36323  funline  36324  fvline  36326  lineelsb2  36330  fwddifval  36344  fwddifnval  36345  rankelg  36350  rankeq1o  36353  elhf2  36357  0hf  36359  rmoeqbidv  36395  disjeq12dv  36397  ixpeq12dv  36398  prodeq12sdv  36400  itgeq12sdv  36401  cbvralvw2  36408  cbvrexvw2  36409  cbvrmovw2  36410  cbvreuvw2  36411  cbvcsbvw2  36413  cbviunvw2  36414  cbviinvw2  36415  cbvmptvw2  36416  cbvdisjvw2  36417  cbvmpo1vw2  36425  cbvmpo2vw2  36426  cbvsbcdavw  36439  cbvcsbdavw  36441  cbvcsbdavw2  36442  cbviundavw  36444  cbviindavw  36445  cbvdisjdavw  36450  cbvrabdavw2  36467  cbviundavw2  36468  cbviindavw2  36469  cbvmptdavw2  36470  cbvdisjdavw2  36471  cbvriotadavw2  36472  cbvmpo1davw2  36474  cbvmpo2davw2  36475  cbvsumdavw2  36477  neibastop2lem  36542  neibastop3  36544  eltail  36556  ttctr  36675  dfttc2g  36688  mh-infprim2bi  36729  bj-projeq  37299  bj-projval  37303  bj-restsn  37394  opelopabbv  37457  brabd0  37461  bj-eldiag  37490  bj-eldiag2  37491  mptsnunlem  37654  dissneqlem  37656  iooelexlt  37678  relowlssretop  37679  rdgellim  37692  exrecfnlem  37695  finxpeq1  37702  finxpreclem6  37712  pibp21  37731  curf  37919  uncf  37920  curunc  37923  unccur  37924  fin2so  37928  lindsadd  37934  lindsdom  37935  lindsenlbs  37936  matunitlindflem1  37937  matunitlindflem2  37938  matunitlindf  37939  ptrest  37940  ptrecube  37941  poimirlem2  37943  poimirlem8  37949  poimirlem17  37958  poimirlem18  37959  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem24  37965  poimirlem26  37967  poimirlem29  37970  heicant  37976  mblfinlem1  37978  mblfinlem2  37979  volsupnfl  37986  itg2addnclem  37992  itg2gt0cn  37996  indexdom  38055  incsequz  38069  istotbnd  38090  istotbnd3  38092  0totbnd  38094  sstotbnd  38096  sstotbnd3  38097  isbnd  38101  prdstotbnd  38115  cntotbnd  38117  isismty  38122  heibor1lem  38130  heiborlem2  38133  heiborlem3  38134  heibor  38142  isass  38167  exidcl  38197  exidreslem  38198  elghomlem2OLD  38207  rngoidmlem  38257  rngo1cl  38260  divrngcl  38278  isdrngo2  38279  isrngohom  38286  isrngoiso  38299  isriscg  38305  iscom2  38316  iscringd  38319  isidl  38335  ispridl  38355  ismaxidl  38361  ac6s6  38493  dmecd  38631  dfpre4  38801  releldmqs  39064  releldmqscoss  39066  erimeq2  39084  qmapeldisjsim  39181  eldisjlem19  39234  membpartlem19  39235  prter3  39328  islshp  39425  islsat  39437  lcvfbr  39466  islfl  39506  ellkr  39535  islshpkrN  39566  ldual1dim  39612  isopos  39626  cmtfvalN  39656  cvrfval  39714  isat  39732  islln  39952  islpln  39976  islvol  40019  isline  40185  ispointN  40188  ispsubsp  40191  elpmap  40204  elpmapat  40210  elpadd  40245  paddclN  40288  elpclN  40338  elpcliN  40339  pclfinN  40346  pclcmpatN  40347  ispsubclN  40383  iswatN  40440  islhp  40442  islaut  40529  ispautN  40545  isldil  40556  isltrn  40565  isdilN  40600  istrnN  40603  istendo  41206  dvhb1dimN  41432  erng1lem  41433  erngdvlem4-rN  41445  diaelval  41479  diaeldm  41482  dia1dimid  41509  cdlemm10N  41564  dibopelvalN  41589  dibopelval2  41591  dibelval3  41593  dibelval1st  41595  dibelval2nd  41598  dibeldmN  41604  dibvalrel  41609  dibglbN  41612  dicffval  41620  dicfval  41621  dicopelval  41623  dicelvalN  41624  dicelval3  41626  dicvalrelN  41631  dicelval1sta  41633  diclspsn  41640  dihopelvalbN  41684  dihopelvalcqat  41692  dihopelvalcpre  41694  dihvalrel  41725  dih1  41732  dihmeetlem4preN  41752  dihmeetlem13N  41765  dih1dimatlem  41775  dochnel2  41838  dihjatcclem4  41867  dvh2dim  41891  dvh3dim  41892  dvh4dimN  41893  dochfln0  41923  lpolsetN  41928  islpolN  41929  lcfrvalsnN  41987  lcfrlem21  42009  lcfrlem27  42015  lcfrlem37  42025  lcfr  42031  lcdlss  42065  mapdcv  42106  hdmap1fval  42242  hdmapffval  42272  hdmapfval  42273  hdmapval  42274  hgmapffval  42331  hgmapfval  42332  hdmapellkr  42360  hlhilhillem  42406  fzsplitnd  42421  isprimroot  42532  primrootsunit1  42536  primrootscoprmpow  42538  primrootscoprbij  42541  aks6d1c1p2  42548  aks6d1c1p3  42549  aks6d1c1p4  42550  aks6d1c1p5  42551  aks6d1c1p6  42553  aks6d1c1  42555  evl1gprodd  42556  sticksstones11  42595  sticksstones12a  42596  rhmqusspan  42624  grpods  42633  fzosumm1  42689  frlmfielbas  42945  frlmsnic  42985  psrmnd  42988  isnacs  43136  mrefg2  43139  elmzpcl  43158  mzpcompact2  43184  eldiophb  43189  elpell1qr  43275  elpell14qr  43277  elpell1234qr  43279  pw2f1ocnv  43465  pw2f1o2val2  43468  aomclem4  43485  aomclem6  43487  islssfg2  43499  imasgim  43528  lnr2i  43544  elmnc  43564  rngunsnply  43597  onexomgt  43669  onexlimgt  43671  onexoegt  43672  oaordnr  43724  omnord1  43733  oenord1  43744  cantnfresb  43752  tfsconcatun  43765  tfsconcat0i  43773  ofoaf  43783  naddcnff  43790  naddcnffo  43792  naddcnfcom  43794  naddcnfid1  43795  naddcnfid2  43796  naddcnfass  43797  naddwordnexlem4  43829  fiinfi  44000  sqrtcvallem1  44058  elintima  44080  eliunov2  44106  ov2ssiunov2  44127  brtrclfv2  44154  rfovcnvf1od  44431  rfovcnvfvd  44434  fsovrfovd  44436  fsovfvd  44437  fsovcnvlem  44440  ntrclsfv1  44482  ntrclselnel1  44484  ntrclsneine0lem  44491  ntrneifv1  44506  ntrneifv2  44507  ntrneiel  44508  gneispace2  44559  gneispacess2  44573  extoimad  44591  mnringelbased  44644  dvconstbi  44761  bccbc  44772  wfac8prim  45429  permaxrep  45433  permac8prim  45441  eliin2f  45534  iineq12dv  45536  rabbida2  45562  disjinfi  45622  unirnmap  45637  elmptima  45687  iuneqfzuzlem  45764  iooiinioc  45986  fsumiunss  46005  fsumsupp0  46008  lptre2pt  46068  icccncfext  46315  cncfiooicclem1  46321  dvnprodlem2  46375  stoweidlem27  46455  stoweidlem29  46457  stoweidlem31  46459  stoweidlem34  46462  stoweidlem48  46476  stoweidlem59  46487  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem2  46537  fourierdlem3  46538  fourierdlem25  46560  fourierdlem32  46567  fourierdlem33  46568  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem62  46596  fourierdlem70  46604  fourierdlem80  46614  fourierdlem92  46626  fourierdlem93  46627  fourierdlem101  46635  etransclem37  46699  sge0val  46794  sge0f1o  46810  sge0iunmptlemre  46843  sge0iunmpt  46846  iundjiun  46888  caragenel  46923  ovncvrrp  46992  ovnsubaddlem1  46998  ovnsubadd  47000  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoidmvle  47028  ovncvr2  47039  hspdifhsp  47044  hoiqssbl  47053  hspmbllem2  47055  hspmbl  47057  opnvonmbllem1  47060  isvonmbl  47066  ovnovollem1  47084  issmflem  47155  smflimlem3  47201  smflimlem4  47202  smflim  47205  smfmullem2  47220  smflimmpt  47238  smfsuplem1  47239  smflimsuplem1  47248  smflimsuplem3  47250  smflimsuplem4  47251  smflimsuplem7  47254  smflimsup  47256  chnsubseq  47310  fcores  47515  fcoresf1  47517  afvelrnb  47611  afvelrnb0  47612  afv2co2  47705  el1fzopredsuc  47774  muldvdsfacm1  47835  iccpart  47876  iccpartgtprec  47880  iccpartiltu  47882  iccpartigtl  47883  iccpartltu  47885  iccpartgtl  47886  iccpartgt  47887  iccpartleu  47888  iccpartgel  47889  iccelpart  47893  iccpartiun  47894  icceuelpart  47896  fargshiftfv  47899  fargshiftfo  47902  sprel  47944  prprelb  47976  prprelprb  47977  nprmdvdsfacm1lem4  48086  fpprel  48204  sbgoldbo  48263  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem3  48283  bgoldbtbnd  48285  clnbgrval  48298  elclnbgrelnbgr  48301  clnbgrel  48304  clnbupgrel  48310  vopnbgrel  48330  isubgredg  48342  upgrimwlklem3  48375  upgrimwlklem5  48377  upgrimpths  48385  grtriprop  48417  isgrtri  48419  grtriclwlk3  48421  stgredgel  48433  gpgvtxel  48523  gpgiedgdmel  48525  gpgedgel  48526  opgpgvtx  48531  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg3kgrtriex  48565  grlimedgnedg  48607  upwlksfval  48611  isupwlk  48612  intop  48679  isclintop  48683  assintop  48685  isassintop  48686  assintopcllaw  48688  uzlidlring  48711  elrngchomALTV  48745  rngccatidALTV  48748  rngcsectALTV  48751  rngcisoALTV  48753  rhmsubcALTVlem3  48759  rhmsubcALTVlem4  48760  funcringcsetcALTV2lem7  48772  funcringcsetcALTV2lem9  48774  elringchomALTV  48779  ringccatidALTV  48782  ringcsectALTV  48785  ringcisoALTV  48787  ringcbasbasALTV  48788  funcringcsetclem7ALTV  48795  funcringcsetclem9ALTV  48797  srhmsubcALTV  48801  cbvmpox2  48812  ply1sclrmsm  48860  dmatALTbasel  48878  lcoval  48888  lindslinindsimp1  48933  lindslinindsimp2  48939  lmod1  48968  elbigo  49027  elbigo2  49028  elbigolo1  49033  dig2nn0ld  49080  naryfvalel  49106  rrxlines  49209  rrxlinesc  49211  rrxlinec  49212  eenglngeehlnm  49215  elrrx2linest2  49221  rrxsphere  49224  itsclc0  49247  itsclc0b  49248  itsclinecirc0  49249  itsclinecirc0b  49250  itscnhlinecirc02p  49261  brab2dd  49303  f1omo  49368  f1omoOLD  49369  lubeldm2d  49433  glbeldm2d  49434  catprs  49486  sectpropdlem  49511  nelsubc3lem  49545  initc  49566  imaid  49629  upfval  49651  upfval2  49652  upfval3  49653  uppropd  49656  oppcinito  49710  oppctermo  49711  oppczeroo  49712  initopropd  49718  termopropd  49719  isthinc  49894  isthincd2lem1  49900  thincmoALT  49904  thincmod  49905  isthincd  49911  thincpropd  49917  indcthing  49935  discthing  49936  prsthinc  49939  termcterm  49988  termc2  49993  isinito4  50022  2arwcatlem1  50070  setc1onsubc  50077  cnelsubclem  50078  ranval3  50106  lmdfval2  50130  cmdfval2  50131  termolmd  50145  elsetrecslem  50174