Theorem eleq2d 2820

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  eleq2  2823  eleq12d  2828  eleqtrd  2836  neleqtrd  2856  eqabrd  2877  raleqbidv  3325  rexeqbidv  3326  reueqbidv  3402  rabeqbidva  3432  elabd2  3649  sbcbid  3820  csbeq2d  3880  csbeq2dv  3881  cbvcsbw  3884  cbvcsb  3885  cbvcsbv  3886  csbie  3909  csbied  3910  csbie2g  3914  cbvralcsf  3916  cbvreucsf  3918  cbvrabcsf  3919  sbcel12  4386  sbcel1g  4391  sbcel2  4393  prel12g  4840  eliuni  4973  iuneqconst  4979  iuneq12df  4994  iuneq12d  4997  cbviun  5012  cbviin  5013  cbviung  5014  cbviing  5015  cbviunv  5016  cbviinv  5017  iinxsng  5064  iinxprg  5065  iunxsng  5066  iunxsngf  5068  cbvdisj  5096  cbvdisjv  5097  disjor  5101  disjiund  5110  mpteq12da  5203  mpteq12f  5205  mpteq12dva  5206  axpweq  5321  rabxfrd  5387  rbropapd  5539  opeliunxp  5721  opeliun2xp  5722  opeliunxp2  5818  iunxpf  5828  elimampt  6030  elrelimasn  6073  elimasni  6078  imadifssran  6140  xpdifid  6157  ressn  6274  funfni  6643  fnbr  6645  dffv3  6871  elfv2ex  6921  fvelrnb  6938  foelcdmi  6939  fvun1  6969  fvco2  6975  elfvmptrab1w  7012  elfvmptrab1  7013  elfvmptrab  7014  elpreima  7047  dff3  7089  fmptco  7118  fnelfp  7166  fnelnfp  7168  tpres  7192  fnprb  7199  fntpb  7200  funfvima3  7227  eluniima  7241  elunirn2OLD  7244  dff13  7246  f1ounsn  7264  f1eqcocnv  7293  isoini  7330  riotaeqdv  7361  mpoeq123dva  7479  cbvmpox  7498  elimampo  7542  ovelrn  7581  elovmpod  7649  elovmpo  7650  elovmporab  7651  elovmporab1w  7652  elovmporab1  7653  elovmpt3rab1  7665  fiun  7939  f1iun  7940  zfrep6  7951  fmpox  8064  el2mpocsbcl  8082  el2mpocl  8083  bropopvvv  8087  bropfvvvv  8089  xpord2indlem  8144  xpord3inddlem  8151  elsuppfng  8166  elsuppfn  8167  suppfnss  8186  opeliunxp2f  8207  mpoxopn0yelv  8210  mpoxopovel  8217  rntpos  8236  mpocurryd  8266  fpr2  8301  wfrdmclOLD  8329  wfrlem12OLD  8332  wfr2  8348  onoviun  8355  smoel  8372  smoiso  8374  smoel2  8375  smo11  8376  tfrlem9  8397  oalimcl  8570  oaass  8571  omordi  8576  omordlim  8587  omlimcl  8588  odi  8589  omeulem1  8592  omeulem2  8593  oen0  8596  oeordi  8597  oeordsuc  8604  oelimcl  8610  oeeulem  8611  oeeui  8612  nnmordi  8641  oaabs2  8659  omabs  8661  omsmolem  8667  ereldm  8767  iiner  8801  elmapg  8851  elpmg  8855  elixpsn  8949  ixpsnf1o  8950  boxriin  8952  omxpenlem  9085  pw2f1olem  9088  phplem2  9217  php3  9221  php3OLD  9231  infn0  9310  elfi  9423  dffi3  9441  marypha2lem2  9446  ordiso2  9527  wemapsolem  9562  elharval  9573  inf3lemd  9639  inf3lem1  9640  inf3lem2  9641  inf3lem3  9642  cantnfs  9678  cantnfp1lem3  9692  cantnflem1b  9698  cantnflem1  9701  ttrclselem2  9738  trcl  9740  frr2  9772  r1sdom  9786  r1ordg  9790  r1pwss  9796  tz9.12lem3  9801  tz9.12  9802  r1elwf  9808  rankr1ai  9810  rankidb  9812  rankr1bg  9815  rankval2  9830  rankunb  9862  tcrank  9896  acni  10057  acni2  10058  acndom  10063  infpwfien  10074  alephnbtwn  10083  cardaleph  10101  cardinfima  10109  iunfictbso  10126  dfac3  10133  dfac5lem5  10139  dfac5  10141  dfac9  10149  dfac12r  10159  kmlem2  10164  kmlem12  10174  kmlem13  10175  kmlem14  10176  ackbij2lem3  10252  ackbij2  10254  cofsmo  10281  alephsing  10288  fin23lem30  10354  isf32lem9  10373  itunisuc  10431  axcc2lem  10448  axcc3  10450  domtriomlem  10454  axdc2lem  10460  axdc2  10461  axdc3lem2  10463  axdc3lem4  10465  axdc4lem  10467  ac6c4  10493  zorn2lem1  10508  ttukeylem6  10526  pwcfsdom  10595  axregndlem2  10615  axinfndlem1  10617  axacndlem4  10622  axacnd  10624  pwfseqlem1  10670  inar1  10787  inatsk  10790  gruurn  10810  grur1  10832  eltskm  10855  genpelv  11012  eluz1  12854  eluzaddOLD  12885  eluzsubOLD  12886  elixx1  13369  elixx3g  13373  elioo2  13401  elfz1  13527  elfz2  13529  elfzp1  13589  fzpr  13594  fzsuc2  13597  fzrev3  13605  elfzp12  13618  fzm1  13622  elfzo  13676  fz0add1fz1  13749  elfzo0l  13770  elfzom1b  13780  fzosplitsni  13792  elfzr  13794  elfzlmr  13795  zmodidfzo  13915  seqp1  14032  seqf1o  14059  bcval  14320  bcpasc  14337  hashf1lem1  14471  fundmge2nop0  14518  wrdmap  14562  elovmpowrd  14574  ccatfval  14589  elfzelfzccat  14596  ccatlid  14602  ccatass  14604  ccatrn  14605  ccatalpha  14609  swrdfv2  14677  ccatswrd  14684  swrdccat2  14685  pfxfv  14698  pfxeq  14712  ccatpfx  14717  swrdswrd  14721  swrdpfx  14723  pfxpfx  14724  cats1un  14737  swrdccatfn  14740  swrdccatin1  14741  pfxccatin12lem4  14742  pfxccatin12lem1  14744  swrdccatin2  14745  pfxccatin12lem2c  14746  pfxccatin12lem2  14747  swrdccat3blem  14755  swrdccatin1d  14759  swrdccatin2d  14760  pfxccatin12d  14761  revccat  14782  revrev  14783  repswpfx  14801  repswccat  14802  cshwidxmod  14819  2cshw  14829  cshwcshid  14844  cshwcsh2id  14845  cshimadifsn  14846  cshimadifsn0  14847  revco  14851  ccatco  14852  cshco  14853  swrdco  14854  ofccat  14986  shftfn  15090  shftval  15091  limsupgle  15491  ello12  15530  elo12  15541  isercolllem3  15681  sumeq1  15703  fsumsplit  15755  sumsplit  15782  fsum2dlem  15784  fsumcom2  15788  fsumparts  15820  explecnv  15879  pwdif  15882  fprodser  15963  fprodsplit  15980  fprod2dlem  15994  fprodcom2  15998  eftlub  16125  divalgmod  16423  bitsval  16441  bitsp1e  16449  bitsp1o  16450  sadfval  16469  sadcp1  16472  sadval  16473  sadcadd  16475  sadadd2  16477  saddisjlem  16481  sadadd  16484  sadass  16488  smufval  16494  smuval  16498  smuval2  16499  smupvallem  16500  smu01lem  16502  smueqlem  16507  smumul  16510  bezoutlem2  16557  bezoutlem4  16559  algfx  16597  eucalgcvga  16603  reumodprminv  16822  nnnn0modprm0  16824  unbenlem  16926  prmreclem5  16938  vdwapval  16991  vdwapun  16992  vdwnnlem1  17013  vdwnn  17016  ramval  17026  0ram  17038  ramub1lem2  17045  prmgaplem7  17075  prmlem0  17123  elrest  17439  prdsbasmpt  17482  prdsleval  17489  prdsbasmpt2  17494  pwselbasb  17500  imasaddfnlem  17540  imasvscafn  17549  divsfval  17559  ismre  17600  mreunirn  17611  mrisval  17640  ismri  17641  isacs  17661  catidd  17690  iscatd2  17691  ismon  17744  isepi  17751  sectffval  17761  sectfval  17762  dfiso2  17783  cicsym  17815  issubc  17846  catsubcat  17850  isfunc  17875  funcres  17907  funcpropd  17913  ffthiso  17942  isnat  17961  isnat2  17962  fuciso  17989  initoval  18004  termoval  18005  isinito  18007  istermo  18008  iszeroo  18009  isinitoi  18010  istermoi  18011  initoid  18012  termoid  18013  iszeroi  18020  2initoinv  18021  initoeu1  18022  initoeu2  18027  2termoinv  18028  termoeu1  18029  arwhoma  18056  elsetchom  18092  setcmon  18098  setcepi  18099  setciso  18102  catciso  18122  elestrchom  18138  estrcbasbas  18141  funcestrcsetclem7  18156  funcestrcsetclem8  18157  funcestrcsetclem9  18158  fthestrcsetc  18160  fullestrcsetc  18161  equivestrcsetc  18162  setc1strwun  18163  funcsetcestrclem7  18171  funcsetcestrclem8  18172  funcsetcestrclem9  18173  fthsetcestrc  18175  fullsetcestrc  18176  hofcl  18269  hofpropd  18277  yonedalem4c  18287  yonedainv  18291  yonffthlem  18292  lubeldm  18361  glbeldm  18374  joindef  18384  meetdef  18398  poslubdg  18422  acsficl2d  18560  acsmapd  18562  psref  18582  psss  18588  dirge  18611  mgmpropd  18627  issstrmgm  18629  grpidval  18637  grpidpropd  18638  grpidd  18647  ismgmhm  18672  issubmgm  18678  issgrpd  18706  sgrppropd  18707  ismndd  18732  mndpropd  18735  imasmnd2  18750  imasmnd  18751  xpsmnd0  18754  ismhm  18761  issubm  18779  gsumsgrpccat  18816  elefmndbas2  18850  smndex1mndlem  18885  imasgrp2  19036  imasgrp  19037  issubg  19107  subginv  19114  isnsg  19136  eqg0el  19164  quselbas  19165  isghm  19196  isghmOLD  19197  resghm2b  19215  conjnmzb  19234  conjnsg  19235  ghmpropd  19237  isga  19272  elcntz  19303  elcntzsn  19306  cntzrcl  19308  resscntz  19314  symgextf1  19400  gsmsymgreqlem2  19410  f1otrspeq  19426  pmtrfrn  19437  pmtrdifellem3  19457  pmtrdifellem4  19458  psgnunilem1  19472  psgnunilem5  19473  psgnunilem2  19474  psgnunilem3  19475  psgneldm2  19483  psgnfitr  19496  psgnsn  19499  gexdvds  19563  gex1  19570  isslw  19587  sylow3lem2  19607  lsmelvalx  19619  pj1ghm  19682  efgtlen  19705  efgsfo  19718  efgredlemc  19724  frgp0  19739  frgpmhm  19744  qusabl  19844  frgpnabllem1  19852  imasabl  19855  cycsubmcmn  19868  0cyg  19872  cycsubgcyg  19880  gsumval3  19886  gsumcllem  19887  gsumzaddlem  19900  gsumzsplit  19906  gsummptfzcl  19948  eldprd  19985  dprdcntz2  20019  dprd2d2  20025  dmdprdsplit2lem  20026  dmdprdsplit2  20027  dprdsplit  20029  ablfac2  20070  isrngd  20131  rngpropd  20132  imasrng  20135  qusrng  20138  ringurd  20143  isringd  20249  imasring  20288  xpsring1d  20291  dvdsrval  20319  isunit  20331  dvdsrpropd  20374  isirred  20377  isrnghm  20399  isrngim  20403  c0ghm  20419  c0snghm  20422  isrhm  20436  isrim0OLD  20439  isrim0  20441  islring  20498  issubrng  20505  opprsubrng  20517  issubrg  20529  opprsubrg  20551  resrhm2b  20560  rhmpropd  20567  rnghmresel  20578  elrngchom  20582  rnghmsubcsetclem1  20589  rnghmsubcsetclem2  20590  rngcid  20593  rngcsect  20594  rngciso  20596  funcrngcsetcALT  20599  zrinitorngc  20600  zrtermorngc  20601  rhmresel  20607  elringchom  20611  rhmsubcsetclem1  20618  rhmsubcsetclem2  20619  ringcid  20622  rhmsscrnghm  20623  rhmsubcrngclem1  20624  rhmsubcrngclem2  20625  ringcsect  20628  ringciso  20630  ringcbasbas  20631  zrtermoringc  20633  srhmsubc  20638  rhmsubclem3  20645  rhmsubclem4  20646  drngunit  20692  isdrngd  20723  isdrngdOLD  20725  issdrg  20746  sdrgunit  20754  isabv  20769  issrngd  20813  islmod  20819  lmodprop2d  20879  islss  20889  islssd  20890  lssats2  20955  ellspsn  20958  islmhm  20983  lmhmf1o  21002  lmhmima  21003  lmhmpreima  21004  reslmhm  21008  pwssplit3  21017  lmhmpropd  21029  islbs  21032  lspprel  21050  lspfixed  21087  lbsacsbs  21115  lbsextlem1  21117  lbsextlem2  21118  lbsextlem3  21119  lbsextlem4  21120  ixpsnbasval  21164  isridlrng  21178  rnglidlmmgm  21204  isridl  21211  quscrng  21242  rngqiprngimfolem  21249  rngqiprngimf1lem  21253  rngqiprngimfo  21260  islpidl  21284  lidldvgen  21293  irinitoringc  21438  pzriprnglem13  21452  pzriprnglem14  21453  zrhrhmb  21469  znf1o  21510  frgpcyg  21532  psgnevpmb  21545  isphld  21612  phlssphl  21617  elocv  21626  iscss  21641  isobs  21678  obs2ss  21687  dsmmfi  21696  dsmmelbas  21697  dsmmlss  21702  frlmelbas  21714  frlmlbs  21755  frlmup1  21756  ellspd  21760  islinds  21767  islindf2  21772  f1lindf  21780  islindf4  21796  assamulgscmlem2  21858  psrgrp  21914  mplsubglem  21957  mpllsslem  21958  mplmonmul  21992  subrgascl  22022  subrgasclcl  22023  mpfind  22063  ismhp  22076  gsumply1subr  22167  lply1binomsc  22247  matbas2d  22359  matecl  22361  matvscl  22367  mat1  22383  mat0dim0  22403  mat0dimid  22404  mat0dimscm  22405  mat1dimelbas  22407  dmatel  22429  scmatel  22441  scmateALT  22448  scmataddcl  22452  scmatsubcl  22453  smatvscl  22460  scmatghm  22469  mat1scmat  22475  mdetunilem7  22554  mdetunilem9  22556  smadiadetr  22611  cramerimplem2  22620  cramer0  22626  pmatcoe1fsupp  22637  cpmatpmat  22646  cpmatel  22647  cpmatacl  22652  cpmatinvcl  22653  mat2pmatghm  22666  mat2pmatmul  22667  decpmatmullem  22707  pmatcollpwlem  22716  pmatcollpw3fi1lem1  22722  pmatcollpwscmatlem1  22725  monmat2matmon  22760  chfacfscmul0  22794  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  cayhamlem1  22802  cpmadugsumlemB  22810  cpmadugsumlemC  22811  cpmadugsumlemF  22812  cayhamlem2  22820  istopon  22848  eltg  22893  eltg2  22894  eltop  22910  eltop2  22911  eltop3  22912  pptbas  22944  iscld  22963  neiss2  23037  isnei  23039  neiptopnei  23068  neiptopreu  23069  lpfval  23074  lpval  23075  islp  23076  maxlp  23083  islpi  23085  neitr  23116  restlp  23119  ordtbas2  23127  ordtrest2  23140  lmfval  23168  cnfval  23169  iscn  23171  iscnp  23173  tgcn  23188  tgcnp  23189  lmbrf  23196  cnpresti  23224  ist1  23257  ist1-2  23283  cnt1  23286  haust1  23288  cmpfi  23344  cmpfii  23345  1stcfb  23381  2ndc1stc  23387  1stcrest  23389  2ndcdisj  23392  1stcelcls  23397  nllyi  23411  subislly  23417  islocfin  23453  lfinpfin  23460  locfindis  23466  locfincf  23467  comppfsc  23468  kgenval  23471  elkgen  23472  kgencn2  23493  txbas  23503  eltx  23504  ptval  23506  ptpjpre1  23507  ptopn2  23520  ptpjopn  23548  ptclsg  23551  xkoccn  23555  txdis  23568  txdis1cn  23571  ptrescn  23575  hausdiag  23581  hauseqlcld  23582  txhaus  23583  xkohaus  23589  elqtop  23633  qtopeu  23652  kqcldsat  23669  hmeofval  23694  ptuncnv  23743  ptunhmeo  23744  elmptrab  23763  fbdmn0  23770  elfg  23807  elfilss  23812  filunirn  23818  fixufil  23858  elfm  23883  rnelfmlem  23888  rnelfm  23889  fmfnfmlem4  23893  elflim2  23900  flimtopon  23906  elflim  23907  hausflim  23917  flimcls  23921  flfnei  23927  isflf  23929  hausflf  23933  cnpflf  23937  cnflf  23938  txflf  23942  isfcls  23945  fclstopon  23948  isfcls2  23949  fclssscls  23954  fclsnei  23955  fclsfnflim  23963  flimfnfcls  23964  isfcf  23970  fcfelbas  23972  cnpfcf  23977  cnfcf  23978  flfcntr  23979  alexsublem  23980  alexsubALTlem3  23985  cnextfun  24000  cnextfvval  24001  cnextf  24002  cnextcn  24003  tmdgsum2  24032  tgpconncomp  24049  ghmcnp  24051  qustgplem  24057  eltsms  24069  haustsms  24072  tsmsgsum  24075  tsmssubm  24079  tsmssplit  24088  isust  24140  ustbas  24164  elutop  24170  ustuqtoplem  24176  ustuqtop4  24181  ustuqtop  24183  utopsnneiplem  24184  utopsnneip  24185  utopsnnei  24186  isusp  24198  isucn  24214  ucncn  24221  iscfilu  24224  neipcfilu  24232  iscusp  24235  cnextucn  24239  ispsmet  24241  ismet  24260  isxmet  24261  elblps  24324  elbl  24325  elmopn  24379  prdsbl  24428  neibl  24438  met1stc  24458  metrest  24461  prdsxmslem2  24466  txmetcnp  24484  txmetcn  24485  metustsym  24492  cfilucfil2  24498  elbl4  24500  metuel  24501  psmetutop  24504  restmetu  24507  metucn  24508  tngngp  24591  isnmhm  24683  zcld  24751  metnrmlem1a  24796  elcncf  24831  cncfcnvcn  24868  cnheibor  24903  lebnumlem1  24909  ishtpy  24920  isphtpy  24929  om1elbas  24981  elpi1  24994  pi1xfr  25004  pi1coghm  25010  tcphcph  25187  lmmbrf  25212  iscfil  25215  iscau  25226  iscauf  25230  caucfil  25233  iscmet  25234  cmetcaulem  25238  iscmet3lem1  25241  iscmet3lem2  25242  iscmet3  25243  bcthlem1  25274  cmsss  25301  cmetcusp1  25303  cmetcusp  25304  cmscsscms  25323  rrxcph  25342  minveclem3b  25378  ovolfioo  25418  ovolficc  25419  ovolctb  25441  ovoliunnul  25458  ovolshftlem1  25460  sca2rab  25463  ovolscalem1  25464  ovolicc2lem1  25468  ovolicc2lem2  25469  ovolicc2lem4  25471  ovolicc2lem5  25472  iundisj  25499  iunmbl2  25508  uniioombllem3  25536  vitalilem2  25560  vitalilem3  25561  mbfss  25597  i1faddlem  25644  i1fmullem  25645  mbfi1fseqlem2  25667  mbfi1fseqlem4  25669  mbfi1fseq  25672  itg2splitlem  25699  itg2split  25700  itg2monolem1  25701  itg2gt0  25711  isibl  25716  iblss2  25757  itgss3  25766  itgsplit  25787  ellimc  25824  limcmo  25833  cnlimc  25839  limciun  25845  limcun  25846  eldv  25849  dvbsss  25853  dvreslem  25860  elcpn  25886  dvaddf  25895  dvmulf  25896  dvcof  25902  rolle  25944  dvlip2  25950  dvivthlem1  25963  lhop1  25969  lhop2  25970  ftc1cn  26000  fta1glem2  26124  plyco0  26147  elply  26150  ply1termlem  26158  eltayl  26317  tayl0  26319  taylplem1  26320  taylplem2  26321  dvtaylp  26328  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  abelth  26401  cxpcn3  26708  rlimcnp  26925  fsumharmonic  26972  dchrelbas  27197  pntrsumbnd2  27528  ostth2lem2  27595  nolesgn2ores  27634  nogesgn1ores  27636  nosupprefixmo  27662  noinfprefixmo  27663  nosupcbv  27664  nosupdm  27666  nosupfv  27668  nosupres  27669  nosupbnd1lem1  27670  nosupbnd1lem3  27672  nosupbnd1lem5  27674  nosupbnd2lem1  27677  noinfcbv  27679  noinfdm  27681  noinffv  27683  noinfres  27684  noinfbnd1lem1  27685  noinfbnd1lem3  27687  noinfbnd1lem5  27689  noinfbnd2lem1  27692  elmade  27823  elold  27825  ssltleft  27826  ssltright  27827  oldlim  27842  madebday  27855  newbday  27857  sltlpss  27862  cofcutr  27875  cofcutrtime  27878  lrrecval  27889  lrrecval2  27890  addsval  27912  precsexlem9  28156  precsexlem11  28158  sltonold  28200  noseqrdgfn  28229  istrkgb  28380  istrkgcb  28381  istrkge  28382  istrkgl  28383  istrkgld  28384  axtgsegcon  28389  axtg5seg  28390  axtgbtwnid  28391  axtgpasch  28392  axtgupdim2  28396  axtgeucl  28397  tgdim01  28432  iscgrg  28437  isismt  28459  tglnunirn  28473  tglngval  28476  tgellng  28478  legval  28509  legov  28510  legov2  28511  ishlg  28527  mirreu3  28579  mirval  28580  mirfv  28581  mircgr  28582  mirbtwn  28583  ismir  28584  mireq  28590  symquadlem  28614  israg  28622  perpln1  28635  perpln2  28636  isperp  28637  islnopp  28664  outpasch  28680  ishpg  28684  iscgra  28734  dfcgra2  28755  isinag  28763  isleag  28772  iseqlg  28792  f1otrgitv  28795  f1otrg  28796  f1otrge  28797  ttgval  28800  ttgelitv  28808  elee  28819  brbtwn  28824  brcgr  28825  axlowdimlem16  28882  ebtwntg  28907  elntg2  28910  upgrex  29017  edgupgr  29059  upgredg  29062  edglnl  29068  numedglnl  29069  uhgr2edg  29133  umgr2edg1  29136  usgredg2vlem1  29150  usgredg2vlem2  29151  ushgredgedg  29154  ushgredgedgloop  29156  uhgrspansubgrlem  29215  fusgrfisstep  29254  nbgrval  29261  nbgrel  29265  nbupgrel  29270  nbgr2vtx1edg  29275  nbuhgr2vtx1edgblem  29276  nbuhgr2vtx1edgb  29277  nbusgreledg  29278  usgrnbcnvfv  29290  uvtxval  29312  uvtxel  29313  uvtx01vtx  29322  uvtxusgrel  29328  nbcplgr  29359  cplgr3v  29360  cusgrexi  29368  structtocusgr  29371  vtxdgfval  29393  vtxdg0v  29399  vtxdeqd  29403  vtxdun  29407  1loopgrnb0  29428  1loopgrvd0  29430  1hevtxdg0  29431  1hevtxdg1  29432  1egrvtxdg1  29435  umgr2v2evtxel  29448  umgr2v2enb1  29452  umgr2v2evd2  29453  vtxdginducedm1lem4  29468  vtxdginducedm1  29469  finsumvtxdg2sstep  29475  ewlksfval  29527  isewlk  29528  wksfval  29535  iswlk  29536  uspgr2wlkeq  29572  wlkres  29596  dfpth2  29657  usgr2pthlem  29691  clwlkcompim  29708  uspgrn2crct  29736  wwlks  29763  iswwlksn  29766  wwlknvtx  29773  wlkiswwlks2  29803  wwlksm1edg  29809  wwlksnred  29820  wwlksnext  29821  wwlksnredwwlkn  29823  wwlksnredwwlkn0  29824  wwlksnwwlksnon  29843  wspn0  29852  usgr2wspthons3  29892  rusgrnumwwlkb0  29899  clwwlk  29910  clwwlkccatlem  29916  clwlkclwwlklem2a4  29924  clwlkclwwlk  29929  clwwisshclwwslem  29941  clwwlkinwwlk  29967  clwwlkel  29973  clwwlkf  29974  clwwlkext2edg  29983  wwlksext2clwwlk  29984  wwlksubclwwlk  29985  clwwnisshclwwsn  29986  eleclclwwlknlem2  29988  erclwwlknsym  29997  erclwwlkntr  29998  umgrhashecclwwlk  30005  clwwlkvbij  30040  eupth2lem3lem3  30157  eupth2lem3lem4  30158  eupth2lem3lem6  30160  eupth2lemb  30164  eucrct2eupth  30172  fusgreg2wsplem  30260  2clwwlklem  30270  2clwwlk2clwwlklem  30273  2clwwlkel  30276  2clwwlk2clwwlk  30277  extwwlkfabel  30280  clwwlknonclwlknonf1o  30289  dlwwlknondlwlknonf1olem1  30291  numclwwlk2lem1  30303  numclwlk2lem2f  30304  numclwlk2lem2f1o  30306  ex-res  30368  isssp  30651  sspn  30663  islno  30680  isblo  30709  nmlno0  30722  ishmo  30738  dipdir  30769  dipass  30772  ubthlem1  30797  ubthlem2  30798  htthlem  30844  htth  30845  ocel  31208  ocnel  31225  shsel  31241  shsel2  31249  shmodsi  31316  pjhtheu  31321  pjeq  31326  axpjpj  31347  pjoc2  31366  elspani  31470  h1de2ctlem  31482  elspansn  31493  elspansn2  31494  elnlfn  31855  eleigvec  31884  riesz3i  31989  cbviunf  32482  iuneq12daf  32483  iunrdx  32490  iunrnmptss  32492  cbvdisjf  32498  disjorf  32506  disjabrex  32509  disjabrexf  32510  iundisjf  32516  disjrdx  32518  brab2d  32533  2ndresdju  32573  abfmpunirn  32576  abfmpeld  32578  abfmpel  32579  fmptcof2  32581  acunirnmpt2  32584  acunirnmpt2f  32585  aciunf1lem  32586  funcnvmpt  32591  suppss3  32647  fpwrelmap  32656  xrofsup  32690  iundisjfi  32719  eliccioo  32851  s3f1  32868  ccatf1  32870  ccatws1f1o  32873  swrdrn3  32877  ismnt  32909  mgcoval  32912  chnccats1  32941  gsummpt2co  32988  gsumpart  32997  gsumhashmul  33001  xrge0tsmsbi  33003  gsumwrd2dccatlem  33006  gsumwrd2dccat  33007  cycpmco2  33090  cyc3co2  33097  inftmrel  33124  isinftm  33125  isslmd  33145  urpropd  33173  elrgspn  33187  erlval  33199  rlocval  33200  rloccring  33211  rloc1r  33213  domnpropd  33217  isdrng4  33235  fracfld  33248  resv1r  33301  ellspds  33329  ellpi  33334  lbslsp  33338  rhmimaidl  33393  isprmidl  33399  qsidomlem1  33413  qsidomlem2  33414  ismxidl  33423  crngmxidl  33430  drng0mxidl  33437  opprqus0g  33451  qsfld  33459  isrprm  33478  rsprprmprmidlb  33484  ressply1evls1  33524  ply1mulrtss  33540  dimpropd  33594  lbslsat  33602  extdg1id  33653  fldextrspunlsplem  33660  fldextrspunlsp  33661  elirng  33673  ply1annidllem  33681  constrsuc  33718  constrconj  33725  constrllcllem  33732  constrlccllem  33733  constrcccllem  33734  nn0constr  33741  smatrcl  33773  smatcl  33779  ist0cld  33810  txomap  33811  locfinreflem  33817  zarclsiin  33848  zart0  33856  rhmpreimacnlem  33861  metidval  33867  cnre2csqima  33888  ordtrest2NEW  33900  fmcncfil  33908  fsumcvg4  33927  ofcfval  34075  measvuni  34191  meascnbl  34196  faeval  34223  ismbfm  34228  elunirnmbfm  34229  imambfm  34240  elcarsg  34283  itgeq12dv  34304  issibf  34311  eulerpartlems  34338  eulerpartlemgc  34340  eulerpartlemgvv  34354  eulerpartlemgu  34355  eulerpart  34360  rrvmbfm  34420  elorvc  34438  elorrvc  34442  dstfrvunirn  34453  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemsima  34494  ballotlemrv  34498  fzssfzo  34517  signstfvn  34547  signstfvneq0  34550  signstres  34553  repr0  34589  reprinrn  34596  reprdifc  34605  hgt750lemg  34632  hgt750lemb  34634  istrkg2d  34644  axtgupdim2ALTV  34646  afsval  34649  brafs  34650  bnj945  34750  bnj1400  34812  bnj18eq1  34904  bnj916  34910  bnj1014  34938  bnj1015  34939  bnj1110  34959  bnj1417  35018  revpfxsfxrev  35084  cplgredgex  35089  pfxwlk  35092  revwlk  35093  subfacp1lem2b  35149  subfacp1lem4  35151  subfacp1lem5  35152  subfacp1lem6  35153  ptpconn  35201  cvmscbv  35226  iscvm  35227  cvmsi  35233  cvmsval  35234  cvmliftmolem1  35249  cvmlift2lem12  35282  cvmlift2lem13  35283  cvmlift3lem7  35293  snmlval  35299  satfv1  35331  satfvsucsuc  35333  satfrnmapom  35338  satf0op  35345  satf0n0  35346  sat1el2xp  35347  fmlafvel  35353  isfmlasuc  35356  fmlaomn0  35358  gonan0  35360  goaln0  35361  gonar  35363  goalr  35365  satffunlem1lem2  35371  satffunlem2lem2  35374  satfv0fvfmla0  35381  satef  35384  satefvfmla0  35386  sategoelfvb  35387  satfv1fvfmla1  35391  mrsubfval  35476  mrsubvrs  35490  mclsrcl  35529  mclsval  35531  mppsval  35540  mclsppslem  35551  opelco3  35738  wsuclem  35789  funtransport  35995  fvtransport  35996  brcolinear  36023  colineardim1  36025  funray  36104  fvray  36105  funline  36106  fvline  36108  lineelsb2  36112  fwddifval  36126  fwddifnval  36127  rankelg  36132  rankeq1o  36135  elhf2  36139  0hf  36141  rmoeqbidv  36177  disjeq12dv  36179  ixpeq12dv  36180  prodeq12sdv  36182  itgeq12sdv  36183  cbvralvw2  36190  cbvrexvw2  36191  cbvrmovw2  36192  cbvreuvw2  36193  cbvcsbvw2  36195  cbviunvw2  36196  cbviinvw2  36197  cbvmptvw2  36198  cbvdisjvw2  36199  cbvmpo1vw2  36207  cbvmpo2vw2  36208  cbvsbcdavw  36221  cbvcsbdavw  36223  cbvcsbdavw2  36224  cbviundavw  36226  cbviindavw  36227  cbvdisjdavw  36232  cbvrabdavw2  36249  cbviundavw2  36250  cbviindavw2  36251  cbvmptdavw2  36252  cbvdisjdavw2  36253  cbvriotadavw2  36254  cbvmpo1davw2  36256  cbvmpo2davw2  36257  cbvsumdavw2  36259  neibastop2lem  36324  neibastop3  36326  eltail  36338  bj-projeq  36956  bj-projval  36960  bj-restsn  37046  opelopabbv  37107  brabd0  37111  bj-eldiag  37140  bj-eldiag2  37141  mptsnunlem  37302  dissneqlem  37304  iooelexlt  37326  relowlssretop  37327  rdgellim  37340  exrecfnlem  37343  finxpeq1  37350  finxpreclem6  37360  pibp21  37379  curf  37568  uncf  37569  curunc  37572  unccur  37573  fin2so  37577  lindsadd  37583  lindsdom  37584  lindsenlbs  37585  matunitlindflem1  37586  matunitlindflem2  37587  matunitlindf  37588  ptrest  37589  ptrecube  37590  poimirlem2  37592  poimirlem8  37598  poimirlem17  37607  poimirlem18  37608  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem24  37614  poimirlem26  37616  poimirlem29  37619  heicant  37625  mblfinlem1  37627  mblfinlem2  37628  volsupnfl  37635  itg2addnclem  37641  itg2gt0cn  37645  indexdom  37704  incsequz  37718  istotbnd  37739  istotbnd3  37741  0totbnd  37743  sstotbnd  37745  sstotbnd3  37746  isbnd  37750  prdstotbnd  37764  cntotbnd  37766  isismty  37771  heibor1lem  37779  heiborlem2  37782  heiborlem3  37783  heibor  37791  isass  37816  exidcl  37846  exidreslem  37847  elghomlem2OLD  37856  rngoidmlem  37906  rngo1cl  37909  divrngcl  37927  isdrngo2  37928  isrngohom  37935  isrngoiso  37948  isriscg  37954  iscom2  37965  iscringd  37968  isidl  37984  ispridl  38004  ismaxidl  38010  ac6s6  38142  dmecd  38268  releldmqs  38622  releldmqscoss  38624  erimeq2  38642  eldisjlem19  38774  membpartlem19  38775  prter3  38846  islshp  38943  islsat  38955  lcvfbr  38984  islfl  39024  ellkr  39053  islshpkrN  39084  ldual1dim  39130  isopos  39144  cmtfvalN  39174  cvrfval  39232  isat  39250  islln  39471  islpln  39495  islvol  39538  isline  39704  ispointN  39707  ispsubsp  39710  elpmap  39723  elpmapat  39729  elpadd  39764  paddclN  39807  elpclN  39857  elpcliN  39858  pclfinN  39865  pclcmpatN  39866  ispsubclN  39902  iswatN  39959  islhp  39961  islaut  40048  ispautN  40064  isldil  40075  isltrn  40084  isdilN  40119  istrnN  40122  istendo  40725  dvhb1dimN  40951  erng1lem  40952  erngdvlem4-rN  40964  diaelval  40998  diaeldm  41001  dia1dimid  41028  cdlemm10N  41083  dibopelvalN  41108  dibopelval2  41110  dibelval3  41112  dibelval1st  41114  dibelval2nd  41117  dibeldmN  41123  dibvalrel  41128  dibglbN  41131  dicffval  41139  dicfval  41140  dicopelval  41142  dicelvalN  41143  dicelval3  41145  dicvalrelN  41150  dicelval1sta  41152  diclspsn  41159  dihopelvalbN  41203  dihopelvalcqat  41211  dihopelvalcpre  41213  dihvalrel  41244  dih1  41251  dihmeetlem4preN  41271  dihmeetlem13N  41284  dih1dimatlem  41294  dochnel2  41357  dihjatcclem4  41386  dvh2dim  41410  dvh3dim  41411  dvh4dimN  41412  dochfln0  41442  lpolsetN  41447  islpolN  41448  lcfrvalsnN  41506  lcfrlem21  41528  lcfrlem27  41534  lcfrlem37  41544  lcfr  41550  lcdlss  41584  mapdcv  41625  hdmap1fval  41761  hdmapffval  41791  hdmapfval  41792  hdmapval  41793  hgmapffval  41850  hgmapfval  41851  hdmapellkr  41879  hlhilhillem  41925  fzsplitnd  41941  isprimroot  42052  primrootsunit1  42056  primrootscoprmpow  42058  primrootscoprbij  42061  aks6d1c1p2  42068  aks6d1c1p3  42069  aks6d1c1p4  42070  aks6d1c1p5  42071  aks6d1c1p6  42073  aks6d1c1  42075  evl1gprodd  42076  sticksstones11  42115  sticksstones12a  42116  rhmqusspan  42144  grpods  42153  fzosumm1  42248  frlmfielbas  42470  frlmsnic  42510  psrmnd  42515  isnacs  42674  mrefg2  42677  elmzpcl  42696  mzpcompact2  42722  eldiophb  42727  elpell1qr  42817  elpell14qr  42819  elpell1234qr  42821  pw2f1ocnv  43008  pw2f1o2val2  43011  aomclem4  43028  aomclem6  43030  islssfg2  43042  imasgim  43071  lnr2i  43087  elmnc  43107  rngunsnply  43140  onexomgt  43212  onexlimgt  43214  onexoegt  43215  oaordnr  43267  omnord1  43276  oenord1  43287  cantnfresb  43295  tfsconcatun  43308  tfsconcat0i  43316  ofoaf  43326  naddcnff  43333  naddcnffo  43335  naddcnfcom  43337  naddcnfid1  43338  naddcnfid2  43339  naddcnfass  43340  naddwordnexlem4  43372  fiinfi  43544  sqrtcvallem1  43602  elintima  43624  eliunov2  43650  ov2ssiunov2  43671  brtrclfv2  43698  rfovcnvf1od  43975  rfovcnvfvd  43978  fsovrfovd  43980  fsovfvd  43981  fsovcnvlem  43984  ntrclsfv1  44026  ntrclselnel1  44028  ntrclsneine0lem  44035  ntrneifv1  44050  ntrneifv2  44051  ntrneiel  44052  gneispace2  44103  gneispacess2  44117  extoimad  44135  mnringelbased  44189  dvconstbi  44306  bccbc  44317  wfac8prim  44975  permaxrep  44979  eliin2f  45076  iineq12dv  45078  rabbida2  45104  disjinfi  45164  unirnmap  45180  elmptima  45230  iuneqfzuzlem  45309  iooiinioc  45533  fsumiunss  45552  fsumsupp0  45555  lptre2pt  45617  icccncfext  45864  cncfiooicclem1  45870  dvnprodlem2  45924  stoweidlem27  46004  stoweidlem29  46006  stoweidlem31  46008  stoweidlem34  46011  stoweidlem48  46025  stoweidlem59  46036  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem2  46086  fourierdlem3  46087  fourierdlem25  46109  fourierdlem32  46116  fourierdlem33  46117  fourierdlem41  46125  fourierdlem48  46131  fourierdlem49  46132  fourierdlem62  46145  fourierdlem70  46153  fourierdlem80  46163  fourierdlem92  46175  fourierdlem93  46176  fourierdlem101  46184  etransclem37  46248  sge0val  46343  sge0f1o  46359  sge0iunmptlemre  46392  sge0iunmpt  46395  iundjiun  46437  caragenel  46472  ovncvrrp  46541  ovnsubaddlem1  46547  ovnsubadd  46549  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  hoidmvle  46577  ovncvr2  46588  hspdifhsp  46593  hoiqssbl  46602  hspmbllem2  46604  hspmbl  46606  opnvonmbllem1  46609  isvonmbl  46615  ovnovollem1  46633  issmflem  46704  smflimlem3  46750  smflimlem4  46751  smflim  46754  smfmullem2  46769  smflimmpt  46787  smfsuplem1  46788  smflimsuplem1  46797  smflimsuplem3  46799  smflimsuplem4  46800  smflimsuplem7  46803  smflimsup  46805  tworepnotupword  46863  fcores  47044  fcoresf1  47046  afvelrnb  47140  afvelrnb0  47141  afv2co2  47234  el1fzopredsuc  47302  iccpart  47378  iccpartgtprec  47382  iccpartiltu  47384  iccpartigtl  47385  iccpartltu  47387  iccpartgtl  47388  iccpartgt  47389  iccpartleu  47390  iccpartgel  47391  iccelpart  47395  iccpartiun  47396  icceuelpart  47398  fargshiftfv  47401  fargshiftfo  47404  sprel  47446  prprelb  47478  prprelprb  47479  fpprel  47690  sbgoldbo  47749  wtgoldbnnsum4prm  47764  bgoldbnnsum3prm  47766  bgoldbtbndlem3  47769  bgoldbtbnd  47771  clnbgrval  47784  elclnbgrelnbgr  47787  clnbgrel  47790  clnbupgrel  47796  vopnbgrel  47815  isubgredg  47827  upgrimwlklem3  47860  upgrimwlklem5  47862  upgrimpths  47870  grtriprop  47901  isgrtri  47903  grtriclwlk3  47905  stgredgel  47917  gpgvtxel  47999  gpgiedgdmel  48001  gpgedgel  48002  opgpgvtx  48007  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  gpg3kgrtriex  48039  upwlksfval  48058  isupwlk  48059  intop  48126  isclintop  48130  assintop  48132  isassintop  48133  assintopcllaw  48135  uzlidlring  48158  elrngchomALTV  48192  rngccatidALTV  48195  rngcsectALTV  48198  rngcisoALTV  48200  rhmsubcALTVlem3  48206  rhmsubcALTVlem4  48207  funcringcsetcALTV2lem7  48219  funcringcsetcALTV2lem9  48221  elringchomALTV  48226  ringccatidALTV  48229  ringcsectALTV  48232  ringcisoALTV  48234  ringcbasbasALTV  48235  funcringcsetclem7ALTV  48242  funcringcsetclem9ALTV  48244  srhmsubcALTV  48248  cbvmpox2  48259  ply1sclrmsm  48307  dmatALTbasel  48326  lcoval  48336  lindslinindsimp1  48381  lindslinindsimp2  48387  lmod1  48416  elbigo  48479  elbigo2  48480  elbigolo1  48485  dig2nn0ld  48532  naryfvalel  48558  rrxlines  48661  rrxlinesc  48663  rrxlinec  48664  eenglngeehlnm  48667  elrrx2linest2  48673  rrxsphere  48676  itsclc0  48699  itsclc0b  48700  itsclinecirc0  48701  itsclinecirc0b  48702  itscnhlinecirc02p  48713  brab2dd  48754  f1omo  48816  lubeldm2d  48880  glbeldm2d  48881  catprs  48934  sectpropdlem  48951  nelsubc3lem  48985  imaid  49042  upfval  49059  upfval2  49060  upfval3  49061  oppcinito  49100  oppctermo  49101  oppczeroo  49102  initopropd  49108  termopropd  49109  isthinc  49253  isthincd2lem1  49259  thincmoALT  49263  thincmod  49264  isthincd  49270  thincpropd  49276  indcthing  49294  discthing  49295  prsthinc  49298  termcterm  49346  termc2  49351  2arwcatlem1  49420  setc1onsubc  49427  cnelsubclem  49428  lmdfval2  49475  cmdfval2  49476  elsetrecslem  49511