Theorem eleq2d 2814

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

Hypothesis

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eleq2d	⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Proof of Theorem eleq2d

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1d.1	. . . 4 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dfcleq 2722	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	sylib 218	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		anbi2 634	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1833	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 17	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		dfclel 2804	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		dfclel 2804	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eleq2  2817  eleq12d  2822  eleqtrd  2830  neleqtrd  2850  eqabrd  2870  raleqbidv  3316  rexeqbidv  3317  reueqbidv  3391  rabeqbidva  3419  elabd2  3633  sbcbid  3805  csbeq2d  3865  csbeq2dv  3866  cbvcsbw  3869  cbvcsb  3870  cbvcsbv  3871  csbie  3894  csbied  3895  csbie2g  3899  cbvralcsf  3901  cbvreucsf  3903  cbvrabcsf  3904  sbcel12  4370  sbcel1g  4375  sbcel2  4377  prel12g  4824  eliuni  4957  iuneqconst  4963  iuneq12df  4978  iuneq12d  4981  cbviun  4995  cbviin  4996  cbviung  4997  cbviing  4998  cbviunv  4999  cbviinv  5000  iinxsng  5047  iinxprg  5048  iunxsng  5049  iunxsngf  5051  cbvdisj  5079  cbvdisjv  5080  disjor  5084  disjiund  5093  mpteq12da  5185  mpteq12f  5187  mpteq12dva  5188  axpweq  5301  rabxfrd  5367  rbropapd  5517  opeliunxp  5698  opeliun2xp  5699  opeliunxp2  5792  iunxpf  5802  elimampt  6003  elrelimasn  6046  elimasni  6051  imadifssran  6112  xpdifid  6129  ressn  6246  funfni  6606  fnbr  6608  dffv3  6836  elfv2ex  6886  fvelrnb  6903  foelcdmi  6904  fvun1  6934  fvco2  6940  elfvmptrab1w  6977  elfvmptrab1  6978  elfvmptrab  6979  elpreima  7012  dff3  7054  fmptco  7083  fnelfp  7131  fnelnfp  7133  tpres  7157  fnprb  7164  fntpb  7165  funfvima3  7192  eluniima  7206  elunirn2OLD  7209  dff13  7211  f1ounsn  7229  f1eqcocnv  7258  isoini  7295  riotaeqdv  7327  mpoeq123dva  7443  cbvmpox  7462  elimampo  7506  ovelrn  7545  elovmpod  7613  elovmpo  7614  elovmporab  7615  elovmporab1w  7616  elovmporab1  7617  elovmpt3rab1  7629  fiun  7901  f1iun  7902  zfrep6  7913  fmpox  8025  el2mpocsbcl  8041  el2mpocl  8042  bropopvvv  8046  bropfvvvv  8048  xpord2indlem  8103  xpord3inddlem  8110  elsuppfng  8125  elsuppfn  8126  suppfnss  8145  opeliunxp2f  8166  mpoxopn0yelv  8169  mpoxopovel  8176  rntpos  8195  mpocurryd  8225  fpr2  8260  wfr2  8283  onoviun  8289  smoel  8306  smoiso  8308  smoel2  8309  smo11  8310  tfrlem9  8330  oalimcl  8501  oaass  8502  omordi  8507  omordlim  8518  omlimcl  8519  odi  8520  omeulem1  8523  omeulem2  8524  oen0  8527  oeordi  8528  oeordsuc  8535  oelimcl  8541  oeeulem  8542  oeeui  8543  nnmordi  8572  oaabs2  8590  omabs  8592  omsmolem  8598  ereldm  8701  iiner  8739  elmapg  8789  elpmg  8793  elixpsn  8887  ixpsnf1o  8888  boxriin  8890  omxpenlem  9019  pw2f1olem  9022  phplem2  9146  php3  9150  infn0  9227  elfi  9340  dffi3  9358  marypha2lem2  9363  ordiso2  9444  wemapsolem  9479  elharval  9490  inf3lemd  9556  inf3lem1  9557  inf3lem2  9558  inf3lem3  9559  cantnfs  9595  cantnfp1lem3  9609  cantnflem1b  9615  cantnflem1  9618  ttrclselem2  9655  trcl  9657  frr2  9689  r1sdom  9703  r1ordg  9707  r1pwss  9713  tz9.12lem3  9718  tz9.12  9719  r1elwf  9725  rankr1ai  9727  rankidb  9729  rankr1bg  9732  rankval2  9747  rankunb  9779  tcrank  9813  acni  9974  acni2  9975  acndom  9980  infpwfien  9991  alephnbtwn  10000  cardaleph  10018  cardinfima  10026  iunfictbso  10043  dfac3  10050  dfac5lem5  10056  dfac5  10058  dfac9  10066  dfac12r  10076  kmlem2  10081  kmlem12  10091  kmlem13  10092  kmlem14  10093  ackbij2lem3  10169  ackbij2  10171  cofsmo  10198  alephsing  10205  fin23lem30  10271  isf32lem9  10290  itunisuc  10348  axcc2lem  10365  axcc3  10367  domtriomlem  10371  axdc2lem  10377  axdc2  10378  axdc3lem2  10380  axdc3lem4  10382  axdc4lem  10384  ac6c4  10410  zorn2lem1  10425  ttukeylem6  10443  pwcfsdom  10512  axregndlem2  10532  axinfndlem1  10534  axacndlem4  10539  axacnd  10541  pwfseqlem1  10587  inar1  10704  inatsk  10707  gruurn  10727  grur1  10749  eltskm  10772  genpelv  10929  eluz1  12773  eluzaddOLD  12804  eluzsubOLD  12805  elixx1  13291  elixx3g  13295  elioo2  13323  elfz1  13449  elfz2  13451  elfzp1  13511  fzpr  13516  fzsuc2  13519  fzrev3  13527  elfzp12  13540  fzm1  13544  elfzo  13598  fz0add1fz1  13672  elfzo0l  13693  elfzom1b  13703  fzosplitsni  13715  elfzr  13717  elfzlmr  13718  zmodidfzo  13838  seqp1  13957  seqf1o  13984  bcval  14245  bcpasc  14262  hashf1lem1  14396  fundmge2nop0  14443  wrdmap  14487  elovmpowrd  14499  ccatfval  14514  elfzelfzccat  14521  ccatlid  14527  ccatass  14529  ccatrn  14530  ccatalpha  14534  swrdfv2  14602  ccatswrd  14609  swrdccat2  14610  pfxfv  14623  pfxeq  14637  ccatpfx  14642  swrdswrd  14646  swrdpfx  14648  pfxpfx  14649  cats1un  14662  swrdccatfn  14665  swrdccatin1  14666  pfxccatin12lem4  14667  pfxccatin12lem1  14669  swrdccatin2  14670  pfxccatin12lem2c  14671  pfxccatin12lem2  14672  swrdccat3blem  14680  swrdccatin1d  14684  swrdccatin2d  14685  pfxccatin12d  14686  revccat  14707  revrev  14708  repswpfx  14726  repswccat  14727  cshwidxmod  14744  2cshw  14754  cshwcshid  14769  cshwcsh2id  14770  cshimadifsn  14771  cshimadifsn0  14772  revco  14776  ccatco  14777  cshco  14778  swrdco  14779  ofccat  14911  shftfn  15015  shftval  15016  limsupgle  15419  ello12  15458  elo12  15469  isercolllem3  15609  sumeq1  15631  fsumsplit  15683  sumsplit  15710  fsum2dlem  15712  fsumcom2  15716  fsumparts  15748  explecnv  15807  pwdif  15810  fprodser  15891  fprodsplit  15908  fprod2dlem  15922  fprodcom2  15926  eftlub  16053  divalgmod  16352  bitsval  16370  bitsp1e  16378  bitsp1o  16379  sadfval  16398  sadcp1  16401  sadval  16402  sadcadd  16404  sadadd2  16406  saddisjlem  16410  sadadd  16413  sadass  16417  smufval  16423  smuval  16427  smuval2  16428  smupvallem  16429  smu01lem  16431  smueqlem  16436  smumul  16439  bezoutlem2  16486  bezoutlem4  16488  algfx  16526  eucalgcvga  16532  reumodprminv  16751  nnnn0modprm0  16753  unbenlem  16855  prmreclem5  16867  vdwapval  16920  vdwapun  16921  vdwnnlem1  16942  vdwnn  16945  ramval  16955  0ram  16967  ramub1lem2  16974  prmgaplem7  17004  prmlem0  17052  elrest  17366  prdsbasmpt  17409  prdsleval  17416  prdsbasmpt2  17421  pwselbasb  17427  imasaddfnlem  17467  imasvscafn  17476  divsfval  17486  ismre  17527  mreunirn  17538  mrisval  17567  ismri  17568  isacs  17588  catidd  17617  iscatd2  17618  ismon  17671  isepi  17678  sectffval  17688  sectfval  17689  dfiso2  17710  cicsym  17742  issubc  17773  catsubcat  17777  isfunc  17802  funcres  17834  funcpropd  17840  ffthiso  17869  isnat  17888  isnat2  17889  fuciso  17916  initoval  17931  termoval  17932  isinito  17934  istermo  17935  iszeroo  17936  isinitoi  17937  istermoi  17938  initoid  17939  termoid  17940  iszeroi  17947  2initoinv  17948  initoeu1  17949  initoeu2  17954  2termoinv  17955  termoeu1  17956  arwhoma  17983  elsetchom  18019  setcmon  18025  setcepi  18026  setciso  18029  catciso  18049  elestrchom  18065  estrcbasbas  18068  funcestrcsetclem7  18083  funcestrcsetclem8  18084  funcestrcsetclem9  18085  fthestrcsetc  18087  fullestrcsetc  18088  equivestrcsetc  18089  setc1strwun  18090  funcsetcestrclem7  18098  funcsetcestrclem8  18099  funcsetcestrclem9  18100  fthsetcestrc  18102  fullsetcestrc  18103  hofcl  18196  hofpropd  18204  yonedalem4c  18214  yonedainv  18218  yonffthlem  18219  lubeldm  18288  glbeldm  18301  joindef  18311  meetdef  18325  poslubdg  18349  acsficl2d  18487  acsmapd  18489  psref  18509  psss  18515  dirge  18538  mgmpropd  18554  issstrmgm  18556  grpidval  18564  grpidpropd  18565  grpidd  18574  ismgmhm  18599  issubmgm  18605  issgrpd  18633  sgrppropd  18634  ismndd  18659  mndpropd  18662  imasmnd2  18677  imasmnd  18678  xpsmnd0  18681  ismhm  18688  issubm  18706  gsumsgrpccat  18743  elefmndbas2  18777  smndex1mndlem  18812  imasgrp2  18963  imasgrp  18964  issubg  19034  subginv  19041  isnsg  19063  eqg0el  19091  quselbas  19092  isghm  19123  isghmOLD  19124  resghm2b  19142  conjnmzb  19161  conjnsg  19162  ghmpropd  19164  isga  19199  elcntz  19230  elcntzsn  19233  cntzrcl  19235  resscntz  19241  symgextf1  19327  gsmsymgreqlem2  19337  f1otrspeq  19353  pmtrfrn  19364  pmtrdifellem3  19384  pmtrdifellem4  19385  psgnunilem1  19399  psgnunilem5  19400  psgnunilem2  19401  psgnunilem3  19402  psgneldm2  19410  psgnfitr  19423  psgnsn  19426  gexdvds  19490  gex1  19497  isslw  19514  sylow3lem2  19534  lsmelvalx  19546  pj1ghm  19609  efgtlen  19632  efgsfo  19645  efgredlemc  19651  frgp0  19666  frgpmhm  19671  qusabl  19771  frgpnabllem1  19779  imasabl  19782  cycsubmcmn  19795  0cyg  19799  cycsubgcyg  19807  gsumval3  19813  gsumcllem  19814  gsumzaddlem  19827  gsumzsplit  19833  gsummptfzcl  19875  eldprd  19912  dprdcntz2  19946  dprd2d2  19952  dmdprdsplit2lem  19953  dmdprdsplit2  19954  dprdsplit  19956  ablfac2  19997  isrngd  20058  rngpropd  20059  imasrng  20062  qusrng  20065  ringurd  20070  isringd  20176  imasring  20215  xpsring1d  20218  dvdsrval  20246  isunit  20258  dvdsrpropd  20301  isirred  20304  isrnghm  20326  isrngim  20330  c0ghm  20346  c0snghm  20349  isrhm  20363  isrim0OLD  20366  isrim0  20368  islring  20425  issubrng  20432  opprsubrng  20444  issubrg  20456  opprsubrg  20478  resrhm2b  20487  rhmpropd  20494  rnghmresel  20505  elrngchom  20509  rnghmsubcsetclem1  20516  rnghmsubcsetclem2  20517  rngcid  20520  rngcsect  20521  rngciso  20523  funcrngcsetcALT  20526  zrinitorngc  20527  zrtermorngc  20528  rhmresel  20534  elringchom  20538  rhmsubcsetclem1  20545  rhmsubcsetclem2  20546  ringcid  20549  rhmsscrnghm  20550  rhmsubcrngclem1  20551  rhmsubcrngclem2  20552  ringcsect  20555  ringciso  20557  ringcbasbas  20558  zrtermoringc  20560  srhmsubc  20565  rhmsubclem3  20572  rhmsubclem4  20573  drngunit  20619  isdrngd  20650  isdrngdOLD  20652  issdrg  20673  sdrgunit  20681  isabv  20696  issrngd  20740  islmod  20746  lmodprop2d  20806  islss  20816  islssd  20817  lssats2  20882  ellspsn  20885  islmhm  20910  lmhmf1o  20929  lmhmima  20930  lmhmpreima  20931  reslmhm  20935  pwssplit3  20944  lmhmpropd  20956  islbs  20959  lspprel  20977  lspfixed  21014  lbsacsbs  21042  lbsextlem1  21044  lbsextlem2  21045  lbsextlem3  21046  lbsextlem4  21047  ixpsnbasval  21091  isridlrng  21105  rnglidlmmgm  21131  isridl  21138  quscrng  21169  rngqiprngimfolem  21176  rngqiprngimf1lem  21180  rngqiprngimfo  21187  islpidl  21211  lidldvgen  21220  irinitoringc  21365  pzriprnglem13  21379  pzriprnglem14  21380  zrhrhmb  21396  znf1o  21437  frgpcyg  21459  psgnevpmb  21472  isphld  21539  phlssphl  21544  elocv  21553  iscss  21568  isobs  21605  obs2ss  21614  dsmmfi  21623  dsmmelbas  21624  dsmmlss  21629  frlmelbas  21641  frlmlbs  21682  frlmup1  21683  ellspd  21687  islinds  21694  islindf2  21699  f1lindf  21707  islindf4  21723  assamulgscmlem2  21785  psrgrp  21841  mplsubglem  21884  mpllsslem  21885  mplmonmul  21919  subrgascl  21949  subrgasclcl  21950  mpfind  21990  ismhp  22003  gsumply1subr  22094  lply1binomsc  22174  matbas2d  22286  matecl  22288  matvscl  22294  mat1  22310  mat0dim0  22330  mat0dimid  22331  mat0dimscm  22332  mat1dimelbas  22334  dmatel  22356  scmatel  22368  scmateALT  22375  scmataddcl  22379  scmatsubcl  22380  smatvscl  22387  scmatghm  22396  mat1scmat  22402  mdetunilem7  22481  mdetunilem9  22483  smadiadetr  22538  cramerimplem2  22547  cramer0  22553  pmatcoe1fsupp  22564  cpmatpmat  22573  cpmatel  22574  cpmatacl  22579  cpmatinvcl  22580  mat2pmatghm  22593  mat2pmatmul  22594  decpmatmullem  22634  pmatcollpwlem  22643  pmatcollpw3fi1lem1  22649  pmatcollpwscmatlem1  22652  monmat2matmon  22687  chfacfscmul0  22721  chfacfscmulgsum  22723  chfacfpmmulgsum  22727  cayhamlem1  22729  cpmadugsumlemB  22737  cpmadugsumlemC  22738  cpmadugsumlemF  22739  cayhamlem2  22747  istopon  22775  eltg  22820  eltg2  22821  eltop  22837  eltop2  22838  eltop3  22839  pptbas  22871  iscld  22890  neiss2  22964  isnei  22966  neiptopnei  22995  neiptopreu  22996  lpfval  23001  lpval  23002  islp  23003  maxlp  23010  islpi  23012  neitr  23043  restlp  23046  ordtbas2  23054  ordtrest2  23067  lmfval  23095  cnfval  23096  iscn  23098  iscnp  23100  tgcn  23115  tgcnp  23116  lmbrf  23123  cnpresti  23151  ist1  23184  ist1-2  23210  cnt1  23213  haust1  23215  cmpfi  23271  cmpfii  23272  1stcfb  23308  2ndc1stc  23314  1stcrest  23316  2ndcdisj  23319  1stcelcls  23324  nllyi  23338  subislly  23344  islocfin  23380  lfinpfin  23387  locfindis  23393  locfincf  23394  comppfsc  23395  kgenval  23398  elkgen  23399  kgencn2  23420  txbas  23430  eltx  23431  ptval  23433  ptpjpre1  23434  ptopn2  23447  ptpjopn  23475  ptclsg  23478  xkoccn  23482  txdis  23495  txdis1cn  23498  ptrescn  23502  hausdiag  23508  hauseqlcld  23509  txhaus  23510  xkohaus  23516  elqtop  23560  qtopeu  23579  kqcldsat  23596  hmeofval  23621  ptuncnv  23670  ptunhmeo  23671  elmptrab  23690  fbdmn0  23697  elfg  23734  elfilss  23739  filunirn  23745  fixufil  23785  elfm  23810  rnelfmlem  23815  rnelfm  23816  fmfnfmlem4  23820  elflim2  23827  flimtopon  23833  elflim  23834  hausflim  23844  flimcls  23848  flfnei  23854  isflf  23856  hausflf  23860  cnpflf  23864  cnflf  23865  txflf  23869  isfcls  23872  fclstopon  23875  isfcls2  23876  fclssscls  23881  fclsnei  23882  fclsfnflim  23890  flimfnfcls  23891  isfcf  23897  fcfelbas  23899  cnpfcf  23904  cnfcf  23905  flfcntr  23906  alexsublem  23907  alexsubALTlem3  23912  cnextfun  23927  cnextfvval  23928  cnextf  23929  cnextcn  23930  tmdgsum2  23959  tgpconncomp  23976  ghmcnp  23978  qustgplem  23984  eltsms  23996  haustsms  23999  tsmsgsum  24002  tsmssubm  24006  tsmssplit  24015  isust  24067  ustbas  24091  elutop  24097  ustuqtoplem  24103  ustuqtop4  24108  ustuqtop  24110  utopsnneiplem  24111  utopsnneip  24112  utopsnnei  24113  isusp  24125  isucn  24141  ucncn  24148  iscfilu  24151  neipcfilu  24159  iscusp  24162  cnextucn  24166  ispsmet  24168  ismet  24187  isxmet  24188  elblps  24251  elbl  24252  elmopn  24306  prdsbl  24355  neibl  24365  met1stc  24385  metrest  24388  prdsxmslem2  24393  txmetcnp  24411  txmetcn  24412  metustsym  24419  cfilucfil2  24425  elbl4  24427  metuel  24428  psmetutop  24431  restmetu  24434  metucn  24435  tngngp  24518  isnmhm  24610  zcld  24678  metnrmlem1a  24723  elcncf  24758  cncfcnvcn  24795  cnheibor  24830  lebnumlem1  24836  ishtpy  24847  isphtpy  24856  om1elbas  24908  elpi1  24921  pi1xfr  24931  pi1coghm  24937  tcphcph  25113  lmmbrf  25138  iscfil  25141  iscau  25152  iscauf  25156  caucfil  25159  iscmet  25160  cmetcaulem  25164  iscmet3lem1  25167  iscmet3lem2  25168  iscmet3  25169  bcthlem1  25200  cmsss  25227  cmetcusp1  25229  cmetcusp  25230  cmscsscms  25249  rrxcph  25268  minveclem3b  25304  ovolfioo  25344  ovolficc  25345  ovolctb  25367  ovoliunnul  25384  ovolshftlem1  25386  sca2rab  25389  ovolscalem1  25390  ovolicc2lem1  25394  ovolicc2lem2  25395  ovolicc2lem4  25397  ovolicc2lem5  25398  iundisj  25425  iunmbl2  25434  uniioombllem3  25462  vitalilem2  25486  vitalilem3  25487  mbfss  25523  i1faddlem  25570  i1fmullem  25571  mbfi1fseqlem2  25593  mbfi1fseqlem4  25595  mbfi1fseq  25598  itg2splitlem  25625  itg2split  25626  itg2monolem1  25627  itg2gt0  25637  isibl  25642  iblss2  25683  itgss3  25692  itgsplit  25713  ellimc  25750  limcmo  25759  cnlimc  25765  limciun  25771  limcun  25772  eldv  25775  dvbsss  25779  dvreslem  25786  elcpn  25812  dvaddf  25821  dvmulf  25822  dvcof  25828  rolle  25870  dvlip2  25876  dvivthlem1  25889  lhop1  25895  lhop2  25896  ftc1cn  25926  fta1glem2  26050  plyco0  26073  elply  26076  ply1termlem  26084  eltayl  26243  tayl0  26245  taylplem1  26246  taylplem2  26247  dvtaylp  26254  taylthlem1  26257  taylthlem2  26258  taylthlem2OLD  26259  abelth  26327  cxpcn3  26634  rlimcnp  26851  fsumharmonic  26898  dchrelbas  27123  pntrsumbnd2  27454  ostth2lem2  27521  nolesgn2ores  27560  nogesgn1ores  27562  nosupprefixmo  27588  noinfprefixmo  27589  nosupcbv  27590  nosupdm  27592  nosupfv  27594  nosupres  27595  nosupbnd1lem1  27596  nosupbnd1lem3  27598  nosupbnd1lem5  27600  nosupbnd2lem1  27603  noinfcbv  27605  noinfdm  27607  noinffv  27609  noinfres  27610  noinfbnd1lem1  27611  noinfbnd1lem3  27613  noinfbnd1lem5  27615  noinfbnd2lem1  27618  elmade  27755  elold  27757  ssltleft  27758  ssltright  27759  oldlim  27774  madebday  27787  newbday  27789  sltlpss  27795  cofcutr  27808  cofcutrtime  27811  lrrecval  27822  lrrecval2  27823  addsval  27845  precsexlem9  28093  precsexlem11  28095  sltonold  28138  onnolt  28143  onslt  28144  noseqrdgfn  28176  istrkgb  28358  istrkgcb  28359  istrkge  28360  istrkgl  28361  istrkgld  28362  axtgsegcon  28367  axtg5seg  28368  axtgbtwnid  28369  axtgpasch  28370  axtgupdim2  28374  axtgeucl  28375  tgdim01  28410  iscgrg  28415  isismt  28437  tglnunirn  28451  tglngval  28454  tgellng  28456  legval  28487  legov  28488  legov2  28489  ishlg  28505  mirreu3  28557  mirval  28558  mirfv  28559  mircgr  28560  mirbtwn  28561  ismir  28562  mireq  28568  symquadlem  28592  israg  28600  perpln1  28613  perpln2  28614  isperp  28615  islnopp  28642  outpasch  28658  ishpg  28662  iscgra  28712  dfcgra2  28733  isinag  28741  isleag  28750  iseqlg  28770  f1otrgitv  28773  f1otrg  28774  f1otrge  28775  ttgval  28778  ttgelitv  28786  elee  28797  brbtwn  28802  brcgr  28803  axlowdimlem16  28860  ebtwntg  28885  elntg2  28888  upgrex  28995  edgupgr  29037  upgredg  29040  edglnl  29046  numedglnl  29047  uhgr2edg  29111  umgr2edg1  29114  usgredg2vlem1  29128  usgredg2vlem2  29129  ushgredgedg  29132  ushgredgedgloop  29134  uhgrspansubgrlem  29193  fusgrfisstep  29232  nbgrval  29239  nbgrel  29243  nbupgrel  29248  nbgr2vtx1edg  29253  nbuhgr2vtx1edgblem  29254  nbuhgr2vtx1edgb  29255  nbusgreledg  29256  usgrnbcnvfv  29268  uvtxval  29290  uvtxel  29291  uvtx01vtx  29300  uvtxusgrel  29306  nbcplgr  29337  cplgr3v  29338  cusgrexi  29346  structtocusgr  29349  vtxdgfval  29371  vtxdg0v  29377  vtxdeqd  29381  vtxdun  29385  1loopgrnb0  29406  1loopgrvd0  29408  1hevtxdg0  29409  1hevtxdg1  29410  1egrvtxdg1  29413  umgr2v2evtxel  29426  umgr2v2enb1  29430  umgr2v2evd2  29431  vtxdginducedm1lem4  29446  vtxdginducedm1  29447  finsumvtxdg2sstep  29453  ewlksfval  29505  isewlk  29506  wksfval  29513  iswlk  29514  uspgr2wlkeq  29549  wlkres  29572  dfpth2  29632  usgr2pthlem  29666  clwlkcompim  29683  uspgrn2crct  29711  wwlks  29738  iswwlksn  29741  wwlknvtx  29748  wlkiswwlks2  29778  wwlksm1edg  29784  wwlksnred  29795  wwlksnext  29796  wwlksnredwwlkn  29798  wwlksnredwwlkn0  29799  wwlksnwwlksnon  29818  wspn0  29827  usgr2wspthons3  29867  rusgrnumwwlkb0  29874  clwwlk  29885  clwwlkccatlem  29891  clwlkclwwlklem2a4  29899  clwlkclwwlk  29904  clwwisshclwwslem  29916  clwwlkinwwlk  29942  clwwlkel  29948  clwwlkf  29949  clwwlkext2edg  29958  wwlksext2clwwlk  29959  wwlksubclwwlk  29960  clwwnisshclwwsn  29961  eleclclwwlknlem2  29963  erclwwlknsym  29972  erclwwlkntr  29973  umgrhashecclwwlk  29980  clwwlkvbij  30015  eupth2lem3lem3  30132  eupth2lem3lem4  30133  eupth2lem3lem6  30135  eupth2lemb  30139  eucrct2eupth  30147  fusgreg2wsplem  30235  2clwwlklem  30245  2clwwlk2clwwlklem  30248  2clwwlkel  30251  2clwwlk2clwwlk  30252  extwwlkfabel  30255  clwwlknonclwlknonf1o  30264  dlwwlknondlwlknonf1olem1  30266  numclwwlk2lem1  30278  numclwlk2lem2f  30279  numclwlk2lem2f1o  30281  ex-res  30343  isssp  30626  sspn  30638  islno  30655  isblo  30684  nmlno0  30697  ishmo  30713  dipdir  30744  dipass  30747  ubthlem1  30772  ubthlem2  30773  htthlem  30819  htth  30820  ocel  31183  ocnel  31200  shsel  31216  shsel2  31224  shmodsi  31291  pjhtheu  31296  pjeq  31301  axpjpj  31322  pjoc2  31341  elspani  31445  h1de2ctlem  31457  elspansn  31468  elspansn2  31469  elnlfn  31830  eleigvec  31859  riesz3i  31964  cbviunf  32457  iuneq12daf  32458  iunrdx  32465  iunrnmptss  32467  cbvdisjf  32473  disjorf  32481  disjabrex  32484  disjabrexf  32485  iundisjf  32491  disjrdx  32493  brab2d  32508  2ndresdju  32546  abfmpunirn  32549  abfmpeld  32551  abfmpel  32552  fmptcof2  32554  acunirnmpt2  32557  acunirnmpt2f  32558  aciunf1lem  32559  funcnvmpt  32564  suppss3  32620  fpwrelmap  32629  xrofsup  32663  iundisjfi  32692  eliccioo  32824  s3f1  32841  ccatf1  32843  ccatws1f1o  32846  swrdrn3  32850  ismnt  32882  mgcoval  32885  chnccats1  32914  gsummpt2co  32961  gsumpart  32970  gsumhashmul  32974  xrge0tsmsbi  32976  gsumwrd2dccatlem  32979  gsumwrd2dccat  32980  cycpmco2  33063  cyc3co2  33070  isfxp  33098  cntrval2  33101  inftmrel  33107  isinftm  33108  isslmd  33128  urpropd  33156  elrgspn  33170  erlval  33182  rlocval  33183  rloccring  33194  rloc1r  33196  domnpropd  33200  isdrng4  33218  fracfld  33231  resv1r  33284  ellspds  33312  ellpi  33317  lbslsp  33321  rhmimaidl  33376  isprmidl  33382  qsidomlem1  33396  qsidomlem2  33397  ismxidl  33406  crngmxidl  33413  drng0mxidl  33420  opprqus0g  33434  qsfld  33442  isrprm  33461  rsprprmprmidlb  33467  ressply1evls1  33507  ply1mulrtss  33523  dimpropd  33577  lbslsat  33585  extdg1id  33634  fldextrspunlsplem  33641  fldextrspunlsp  33642  elirng  33654  ply1annidllem  33664  constrsuc  33701  constrconj  33708  constrllcllem  33715  constrlccllem  33716  constrcccllem  33717  nn0constr  33724  smatrcl  33759  smatcl  33765  ist0cld  33796  txomap  33797  locfinreflem  33803  zarclsiin  33834  zart0  33842  rhmpreimacnlem  33847  metidval  33853  cnre2csqima  33874  ordtrest2NEW  33886  fmcncfil  33894  fsumcvg4  33913  ofcfval  34061  measvuni  34177  meascnbl  34182  faeval  34209  ismbfm  34214  elunirnmbfm  34215  imambfm  34226  elcarsg  34269  itgeq12dv  34290  issibf  34297  eulerpartlems  34324  eulerpartlemgc  34326  eulerpartlemgvv  34340  eulerpartlemgu  34341  eulerpart  34346  rrvmbfm  34406  elorvc  34424  elorrvc  34428  dstfrvunirn  34439  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemsima  34480  ballotlemrv  34484  fzssfzo  34503  signstfvn  34533  signstfvneq0  34536  signstres  34539  repr0  34575  reprinrn  34582  reprdifc  34591  hgt750lemg  34618  hgt750lemb  34620  istrkg2d  34630  axtgupdim2ALTV  34632  afsval  34635  brafs  34636  bnj945  34736  bnj1400  34798  bnj18eq1  34890  bnj916  34896  bnj1014  34924  bnj1015  34925  bnj1110  34945  bnj1417  35004  onvf1odlem3  35065  vonf1owev  35068  revpfxsfxrev  35076  cplgredgex  35081  pfxwlk  35084  revwlk  35085  subfacp1lem2b  35141  subfacp1lem4  35143  subfacp1lem5  35144  subfacp1lem6  35145  ptpconn  35193  cvmscbv  35218  iscvm  35219  cvmsi  35225  cvmsval  35226  cvmliftmolem1  35241  cvmlift2lem12  35274  cvmlift2lem13  35275  cvmlift3lem7  35285  snmlval  35291  satfv1  35323  satfvsucsuc  35325  satfrnmapom  35330  satf0op  35337  satf0n0  35338  sat1el2xp  35339  fmlafvel  35345  isfmlasuc  35348  fmlaomn0  35350  gonan0  35352  goaln0  35353  gonar  35355  goalr  35357  satffunlem1lem2  35363  satffunlem2lem2  35366  satfv0fvfmla0  35373  satef  35376  satefvfmla0  35378  sategoelfvb  35379  satfv1fvfmla1  35383  mrsubfval  35468  mrsubvrs  35482  mclsrcl  35521  mclsval  35523  mppsval  35532  mclsppslem  35543  opelco3  35735  wsuclem  35786  funtransport  35992  fvtransport  35993  brcolinear  36020  colineardim1  36022  funray  36101  fvray  36102  funline  36103  fvline  36105  lineelsb2  36109  fwddifval  36123  fwddifnval  36124  rankelg  36129  rankeq1o  36132  elhf2  36136  0hf  36138  rmoeqbidv  36174  disjeq12dv  36176  ixpeq12dv  36177  prodeq12sdv  36179  itgeq12sdv  36180  cbvralvw2  36187  cbvrexvw2  36188  cbvrmovw2  36189  cbvreuvw2  36190  cbvcsbvw2  36192  cbviunvw2  36193  cbviinvw2  36194  cbvmptvw2  36195  cbvdisjvw2  36196  cbvmpo1vw2  36204  cbvmpo2vw2  36205  cbvsbcdavw  36218  cbvcsbdavw  36220  cbvcsbdavw2  36221  cbviundavw  36223  cbviindavw  36224  cbvdisjdavw  36229  cbvrabdavw2  36246  cbviundavw2  36247  cbviindavw2  36248  cbvmptdavw2  36249  cbvdisjdavw2  36250  cbvriotadavw2  36251  cbvmpo1davw2  36253  cbvmpo2davw2  36254  cbvsumdavw2  36256  neibastop2lem  36321  neibastop3  36323  eltail  36335  bj-projeq  36953  bj-projval  36957  bj-restsn  37043  opelopabbv  37104  brabd0  37108  bj-eldiag  37137  bj-eldiag2  37138  mptsnunlem  37299  dissneqlem  37301  iooelexlt  37323  relowlssretop  37324  rdgellim  37337  exrecfnlem  37340  finxpeq1  37347  finxpreclem6  37357  pibp21  37376  curf  37565  uncf  37566  curunc  37569  unccur  37570  fin2so  37574  lindsadd  37580  lindsdom  37581  lindsenlbs  37582  matunitlindflem1  37583  matunitlindflem2  37584  matunitlindf  37585  ptrest  37586  ptrecube  37587  poimirlem2  37589  poimirlem8  37595  poimirlem17  37604  poimirlem18  37605  poimirlem20  37607  poimirlem21  37608  poimirlem22  37609  poimirlem24  37611  poimirlem26  37613  poimirlem29  37616  heicant  37622  mblfinlem1  37624  mblfinlem2  37625  volsupnfl  37632  itg2addnclem  37638  itg2gt0cn  37642  indexdom  37701  incsequz  37715  istotbnd  37736  istotbnd3  37738  0totbnd  37740  sstotbnd  37742  sstotbnd3  37743  isbnd  37747  prdstotbnd  37761  cntotbnd  37763  isismty  37768  heibor1lem  37776  heiborlem2  37779  heiborlem3  37780  heibor  37788  isass  37813  exidcl  37843  exidreslem  37844  elghomlem2OLD  37853  rngoidmlem  37903  rngo1cl  37906  divrngcl  37924  isdrngo2  37925  isrngohom  37932  isrngoiso  37945  isriscg  37951  iscom2  37962  iscringd  37965  isidl  37981  ispridl  38001  ismaxidl  38007  ac6s6  38139  dmecd  38265  releldmqs  38623  releldmqscoss  38625  erimeq2  38643  eldisjlem19  38775  membpartlem19  38776  prter3  38848  islshp  38945  islsat  38957  lcvfbr  38986  islfl  39026  ellkr  39055  islshpkrN  39086  ldual1dim  39132  isopos  39146  cmtfvalN  39176  cvrfval  39234  isat  39252  islln  39473  islpln  39497  islvol  39540  isline  39706  ispointN  39709  ispsubsp  39712  elpmap  39725  elpmapat  39731  elpadd  39766  paddclN  39809  elpclN  39859  elpcliN  39860  pclfinN  39867  pclcmpatN  39868  ispsubclN  39904  iswatN  39961  islhp  39963  islaut  40050  ispautN  40066  isldil  40077  isltrn  40086  isdilN  40121  istrnN  40124  istendo  40727  dvhb1dimN  40953  erng1lem  40954  erngdvlem4-rN  40966  diaelval  41000  diaeldm  41003  dia1dimid  41030  cdlemm10N  41085  dibopelvalN  41110  dibopelval2  41112  dibelval3  41114  dibelval1st  41116  dibelval2nd  41119  dibeldmN  41125  dibvalrel  41130  dibglbN  41133  dicffval  41141  dicfval  41142  dicopelval  41144  dicelvalN  41145  dicelval3  41147  dicvalrelN  41152  dicelval1sta  41154  diclspsn  41161  dihopelvalbN  41205  dihopelvalcqat  41213  dihopelvalcpre  41215  dihvalrel  41246  dih1  41253  dihmeetlem4preN  41273  dihmeetlem13N  41286  dih1dimatlem  41296  dochnel2  41359  dihjatcclem4  41388  dvh2dim  41412  dvh3dim  41413  dvh4dimN  41414  dochfln0  41444  lpolsetN  41449  islpolN  41450  lcfrvalsnN  41508  lcfrlem21  41530  lcfrlem27  41536  lcfrlem37  41546  lcfr  41552  lcdlss  41586  mapdcv  41627  hdmap1fval  41763  hdmapffval  41793  hdmapfval  41794  hdmapval  41795  hgmapffval  41852  hgmapfval  41853  hdmapellkr  41881  hlhilhillem  41927  fzsplitnd  41943  isprimroot  42054  primrootsunit1  42058  primrootscoprmpow  42060  primrootscoprbij  42063  aks6d1c1p2  42070  aks6d1c1p3  42071  aks6d1c1p4  42072  aks6d1c1p5  42073  aks6d1c1p6  42075  aks6d1c1  42077  evl1gprodd  42078  sticksstones11  42117  sticksstones12a  42118  rhmqusspan  42146  grpods  42155  fzosumm1  42211  frlmfielbas  42461  frlmsnic  42501  psrmnd  42506  isnacs  42665  mrefg2  42668  elmzpcl  42687  mzpcompact2  42713  eldiophb  42718  elpell1qr  42808  elpell14qr  42810  elpell1234qr  42812  pw2f1ocnv  42999  pw2f1o2val2  43002  aomclem4  43019  aomclem6  43021  islssfg2  43033  imasgim  43062  lnr2i  43078  elmnc  43098  rngunsnply  43131  onexomgt  43203  onexlimgt  43205  onexoegt  43206  oaordnr  43258  omnord1  43267  oenord1  43278  cantnfresb  43286  tfsconcatun  43299  tfsconcat0i  43307  ofoaf  43317  naddcnff  43324  naddcnffo  43326  naddcnfcom  43328  naddcnfid1  43329  naddcnfid2  43330  naddcnfass  43331  naddwordnexlem4  43363  fiinfi  43535  sqrtcvallem1  43593  elintima  43615  eliunov2  43641  ov2ssiunov2  43662  brtrclfv2  43689  rfovcnvf1od  43966  rfovcnvfvd  43969  fsovrfovd  43971  fsovfvd  43972  fsovcnvlem  43975  ntrclsfv1  44017  ntrclselnel1  44019  ntrclsneine0lem  44026  ntrneifv1  44041  ntrneifv2  44042  ntrneiel  44043  gneispace2  44094  gneispacess2  44108  extoimad  44126  mnringelbased  44179  dvconstbi  44296  bccbc  44307  wfac8prim  44965  permaxrep  44969  permac8prim  44977  eliin2f  45071  iineq12dv  45073  rabbida2  45099  disjinfi  45159  unirnmap  45175  elmptima  45225  iuneqfzuzlem  45303  iooiinioc  45527  fsumiunss  45546  fsumsupp0  45549  lptre2pt  45611  icccncfext  45858  cncfiooicclem1  45864  dvnprodlem2  45918  stoweidlem27  45998  stoweidlem29  46000  stoweidlem31  46002  stoweidlem34  46005  stoweidlem48  46019  stoweidlem59  46030  dirkercncflem2  46075  dirkercncflem4  46077  fourierdlem2  46080  fourierdlem3  46081  fourierdlem25  46103  fourierdlem32  46110  fourierdlem33  46111  fourierdlem41  46119  fourierdlem48  46125  fourierdlem49  46126  fourierdlem62  46139  fourierdlem70  46147  fourierdlem80  46157  fourierdlem92  46169  fourierdlem93  46170  fourierdlem101  46178  etransclem37  46242  sge0val  46337  sge0f1o  46353  sge0iunmptlemre  46386  sge0iunmpt  46389  iundjiun  46431  caragenel  46466  ovncvrrp  46535  ovnsubaddlem1  46541  ovnsubadd  46543  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvlelem4  46569  hoidmvle  46571  ovncvr2  46582  hspdifhsp  46587  hoiqssbl  46596  hspmbllem2  46598  hspmbl  46600  opnvonmbllem1  46603  isvonmbl  46609  ovnovollem1  46627  issmflem  46698  smflimlem3  46744  smflimlem4  46745  smflim  46748  smfmullem2  46763  smflimmpt  46781  smfsuplem1  46782  smflimsuplem1  46791  smflimsuplem3  46793  smflimsuplem4  46794  smflimsuplem7  46797  smflimsup  46799  tworepnotupword  46857  fcores  47041  fcoresf1  47043  afvelrnb  47137  afvelrnb0  47138  afv2co2  47231  el1fzopredsuc  47299  iccpart  47390  iccpartgtprec  47394  iccpartiltu  47396  iccpartigtl  47397  iccpartltu  47399  iccpartgtl  47400  iccpartgt  47401  iccpartleu  47402  iccpartgel  47403  iccelpart  47407  iccpartiun  47408  icceuelpart  47410  fargshiftfv  47413  fargshiftfo  47416  sprel  47458  prprelb  47490  prprelprb  47491  fpprel  47702  sbgoldbo  47761  wtgoldbnnsum4prm  47776  bgoldbnnsum3prm  47778  bgoldbtbndlem3  47781  bgoldbtbnd  47783  clnbgrval  47796  elclnbgrelnbgr  47799  clnbgrel  47802  clnbupgrel  47808  vopnbgrel  47827  isubgredg  47839  upgrimwlklem3  47872  upgrimwlklem5  47874  upgrimpths  47882  grtriprop  47913  isgrtri  47915  grtriclwlk3  47917  stgredgel  47929  gpgvtxel  48011  gpgiedgdmel  48013  gpgedgel  48014  opgpgvtx  48019  gpg5nbgrvtx13starlem1  48035  gpg5nbgrvtx13starlem2  48036  gpg5nbgrvtx13starlem3  48037  gpg3kgrtriex  48053  upwlksfval  48096  isupwlk  48097  intop  48164  isclintop  48168  assintop  48170  isassintop  48171  assintopcllaw  48173  uzlidlring  48196  elrngchomALTV  48230  rngccatidALTV  48233  rngcsectALTV  48236  rngcisoALTV  48238  rhmsubcALTVlem3  48244  rhmsubcALTVlem4  48245  funcringcsetcALTV2lem7  48257  funcringcsetcALTV2lem9  48259  elringchomALTV  48264  ringccatidALTV  48267  ringcsectALTV  48270  ringcisoALTV  48272  ringcbasbasALTV  48273  funcringcsetclem7ALTV  48280  funcringcsetclem9ALTV  48282  srhmsubcALTV  48286  cbvmpox2  48297  ply1sclrmsm  48345  dmatALTbasel  48364  lcoval  48374  lindslinindsimp1  48419  lindslinindsimp2  48425  lmod1  48454  elbigo  48513  elbigo2  48514  elbigolo1  48519  dig2nn0ld  48566  naryfvalel  48592  rrxlines  48695  rrxlinesc  48697  rrxlinec  48698  eenglngeehlnm  48701  elrrx2linest2  48707  rrxsphere  48710  itsclc0  48733  itsclc0b  48734  itsclinecirc0  48735  itsclinecirc0b  48736  itscnhlinecirc02p  48747  brab2dd  48789  f1omo  48854  f1omoOLD  48855  lubeldm2d  48919  glbeldm2d  48920  catprs  48973  sectpropdlem  48998  nelsubc3lem  49032  initc  49053  imaid  49116  upfval  49138  upfval2  49139  upfval3  49140  uppropd  49143  oppcinito  49197  oppctermo  49198  oppczeroo  49199  initopropd  49205  termopropd  49206  isthinc  49381  isthincd2lem1  49387  thincmoALT  49391  thincmod  49392  isthincd  49398  thincpropd  49404  indcthing  49422  discthing  49423  prsthinc  49426  termcterm  49475  termc2  49480  isinito4  49509  2arwcatlem1  49557  setc1onsubc  49564  cnelsubclem  49565  ranval3  49593  lmdfval2  49617  cmdfval2  49618  termolmd  49632  elsetrecslem  49661