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  3319  rexeqbidv  3320  reueqbidv  3394  rabeqbidva  3422  elabd2  3636  sbcbid  3808  csbeq2d  3868  csbeq2dv  3869  cbvcsbw  3872  cbvcsb  3873  cbvcsbv  3874  csbie  3897  csbied  3898  csbie2g  3902  cbvralcsf  3904  cbvreucsf  3906  cbvrabcsf  3907  sbcel12  4374  sbcel1g  4379  sbcel2  4381  prel12g  4828  eliuni  4961  iuneqconst  4967  iuneq12df  4982  iuneq12d  4985  cbviun  5000  cbviin  5001  cbviung  5002  cbviing  5003  cbviunv  5004  cbviinv  5005  iinxsng  5052  iinxprg  5053  iunxsng  5054  iunxsngf  5056  cbvdisj  5084  cbvdisjv  5085  disjor  5089  disjiund  5098  mpteq12da  5190  mpteq12f  5192  mpteq12dva  5193  axpweq  5306  rabxfrd  5372  rbropapd  5524  opeliunxp  5705  opeliun2xp  5706  opeliunxp2  5802  iunxpf  5812  elimampt  6014  elrelimasn  6057  elimasni  6062  imadifssran  6124  xpdifid  6141  ressn  6258  funfni  6624  fnbr  6626  dffv3  6854  elfv2ex  6904  fvelrnb  6921  foelcdmi  6922  fvun1  6952  fvco2  6958  elfvmptrab1w  6995  elfvmptrab1  6996  elfvmptrab  6997  elpreima  7030  dff3  7072  fmptco  7101  fnelfp  7149  fnelnfp  7151  tpres  7175  fnprb  7182  fntpb  7183  funfvima3  7210  eluniima  7224  elunirn2OLD  7227  dff13  7229  f1ounsn  7247  f1eqcocnv  7276  isoini  7313  riotaeqdv  7345  mpoeq123dva  7463  cbvmpox  7482  elimampo  7526  ovelrn  7565  elovmpod  7633  elovmpo  7634  elovmporab  7635  elovmporab1w  7636  elovmporab1  7637  elovmpt3rab1  7649  fiun  7921  f1iun  7922  zfrep6  7933  fmpox  8046  el2mpocsbcl  8064  el2mpocl  8065  bropopvvv  8069  bropfvvvv  8071  xpord2indlem  8126  xpord3inddlem  8133  elsuppfng  8148  elsuppfn  8149  suppfnss  8168  opeliunxp2f  8189  mpoxopn0yelv  8192  mpoxopovel  8199  rntpos  8218  mpocurryd  8248  fpr2  8283  wfr2  8306  onoviun  8312  smoel  8329  smoiso  8331  smoel2  8332  smo11  8333  tfrlem9  8353  oalimcl  8524  oaass  8525  omordi  8530  omordlim  8541  omlimcl  8542  odi  8543  omeulem1  8546  omeulem2  8547  oen0  8550  oeordi  8551  oeordsuc  8558  oelimcl  8564  oeeulem  8565  oeeui  8566  nnmordi  8595  oaabs2  8613  omabs  8615  omsmolem  8621  ereldm  8724  iiner  8762  elmapg  8812  elpmg  8816  elixpsn  8910  ixpsnf1o  8911  boxriin  8913  omxpenlem  9042  pw2f1olem  9045  phplem2  9169  php3  9173  infn0  9251  elfi  9364  dffi3  9382  marypha2lem2  9387  ordiso2  9468  wemapsolem  9503  elharval  9514  inf3lemd  9580  inf3lem1  9581  inf3lem2  9582  inf3lem3  9583  cantnfs  9619  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1  9642  ttrclselem2  9679  trcl  9681  frr2  9713  r1sdom  9727  r1ordg  9731  r1pwss  9737  tz9.12lem3  9742  tz9.12  9743  r1elwf  9749  rankr1ai  9751  rankidb  9753  rankr1bg  9756  rankval2  9771  rankunb  9803  tcrank  9837  acni  9998  acni2  9999  acndom  10004  infpwfien  10015  alephnbtwn  10024  cardaleph  10042  cardinfima  10050  iunfictbso  10067  dfac3  10074  dfac5lem5  10080  dfac5  10082  dfac9  10090  dfac12r  10100  kmlem2  10105  kmlem12  10115  kmlem13  10116  kmlem14  10117  ackbij2lem3  10193  ackbij2  10195  cofsmo  10222  alephsing  10229  fin23lem30  10295  isf32lem9  10314  itunisuc  10372  axcc2lem  10389  axcc3  10391  domtriomlem  10395  axdc2lem  10401  axdc2  10402  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  ac6c4  10434  zorn2lem1  10449  ttukeylem6  10467  pwcfsdom  10536  axregndlem2  10556  axinfndlem1  10558  axacndlem4  10563  axacnd  10565  pwfseqlem1  10611  inar1  10728  inatsk  10731  gruurn  10751  grur1  10773  eltskm  10796  genpelv  10953  eluz1  12797  eluzaddOLD  12828  eluzsubOLD  12829  elixx1  13315  elixx3g  13319  elioo2  13347  elfz1  13473  elfz2  13475  elfzp1  13535  fzpr  13540  fzsuc2  13543  fzrev3  13551  elfzp12  13564  fzm1  13568  elfzo  13622  fz0add1fz1  13696  elfzo0l  13717  elfzom1b  13727  fzosplitsni  13739  elfzr  13741  elfzlmr  13742  zmodidfzo  13862  seqp1  13981  seqf1o  14008  bcval  14269  bcpasc  14286  hashf1lem1  14420  fundmge2nop0  14467  wrdmap  14511  elovmpowrd  14523  ccatfval  14538  elfzelfzccat  14545  ccatlid  14551  ccatass  14553  ccatrn  14554  ccatalpha  14558  swrdfv2  14626  ccatswrd  14633  swrdccat2  14634  pfxfv  14647  pfxeq  14661  ccatpfx  14666  swrdswrd  14670  swrdpfx  14672  pfxpfx  14673  cats1un  14686  swrdccatfn  14689  swrdccatin1  14690  pfxccatin12lem4  14691  pfxccatin12lem1  14693  swrdccatin2  14694  pfxccatin12lem2c  14695  pfxccatin12lem2  14696  swrdccat3blem  14704  swrdccatin1d  14708  swrdccatin2d  14709  pfxccatin12d  14710  revccat  14731  revrev  14732  repswpfx  14750  repswccat  14751  cshwidxmod  14768  2cshw  14778  cshwcshid  14793  cshwcsh2id  14794  cshimadifsn  14795  cshimadifsn0  14796  revco  14800  ccatco  14801  cshco  14802  swrdco  14803  ofccat  14935  shftfn  15039  shftval  15040  limsupgle  15443  ello12  15482  elo12  15493  isercolllem3  15633  sumeq1  15655  fsumsplit  15707  sumsplit  15734  fsum2dlem  15736  fsumcom2  15740  fsumparts  15772  explecnv  15831  pwdif  15834  fprodser  15915  fprodsplit  15932  fprod2dlem  15946  fprodcom2  15950  eftlub  16077  divalgmod  16376  bitsval  16394  bitsp1e  16402  bitsp1o  16403  sadfval  16422  sadcp1  16425  sadval  16426  sadcadd  16428  sadadd2  16430  saddisjlem  16434  sadadd  16437  sadass  16441  smufval  16447  smuval  16451  smuval2  16452  smupvallem  16453  smu01lem  16455  smueqlem  16460  smumul  16463  bezoutlem2  16510  bezoutlem4  16512  algfx  16550  eucalgcvga  16556  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  17491  imasvscafn  17500  divsfval  17510  ismre  17551  mreunirn  17562  mrisval  17591  ismri  17592  isacs  17612  catidd  17641  iscatd2  17642  ismon  17695  isepi  17702  sectffval  17712  sectfval  17713  dfiso2  17734  cicsym  17766  issubc  17797  catsubcat  17801  isfunc  17826  funcres  17858  funcpropd  17864  ffthiso  17893  isnat  17912  isnat2  17913  fuciso  17940  initoval  17955  termoval  17956  isinito  17958  istermo  17959  iszeroo  17960  isinitoi  17961  istermoi  17962  initoid  17963  termoid  17964  iszeroi  17971  2initoinv  17972  initoeu1  17973  initoeu2  17978  2termoinv  17979  termoeu1  17980  arwhoma  18007  elsetchom  18043  setcmon  18049  setcepi  18050  setciso  18053  catciso  18073  elestrchom  18089  estrcbasbas  18092  funcestrcsetclem7  18107  funcestrcsetclem8  18108  funcestrcsetclem9  18109  fthestrcsetc  18111  fullestrcsetc  18112  equivestrcsetc  18113  setc1strwun  18114  funcsetcestrclem7  18122  funcsetcestrclem8  18123  funcsetcestrclem9  18124  fthsetcestrc  18126  fullsetcestrc  18127  hofcl  18220  hofpropd  18228  yonedalem4c  18238  yonedainv  18242  yonffthlem  18243  lubeldm  18312  glbeldm  18325  joindef  18335  meetdef  18349  poslubdg  18373  acsficl2d  18511  acsmapd  18513  psref  18533  psss  18539  dirge  18562  mgmpropd  18578  issstrmgm  18580  grpidval  18588  grpidpropd  18589  grpidd  18598  ismgmhm  18623  issubmgm  18629  issgrpd  18657  sgrppropd  18658  ismndd  18683  mndpropd  18686  imasmnd2  18701  imasmnd  18702  xpsmnd0  18705  ismhm  18712  issubm  18730  gsumsgrpccat  18767  elefmndbas2  18801  smndex1mndlem  18836  imasgrp2  18987  imasgrp  18988  issubg  19058  subginv  19065  isnsg  19087  eqg0el  19115  quselbas  19116  isghm  19147  isghmOLD  19148  resghm2b  19166  conjnmzb  19185  conjnsg  19186  ghmpropd  19188  isga  19223  elcntz  19254  elcntzsn  19257  cntzrcl  19259  resscntz  19265  symgextf1  19351  gsmsymgreqlem2  19361  f1otrspeq  19377  pmtrfrn  19388  pmtrdifellem3  19408  pmtrdifellem4  19409  psgnunilem1  19423  psgnunilem5  19424  psgnunilem2  19425  psgnunilem3  19426  psgneldm2  19434  psgnfitr  19447  psgnsn  19450  gexdvds  19514  gex1  19521  isslw  19538  sylow3lem2  19558  lsmelvalx  19570  pj1ghm  19633  efgtlen  19656  efgsfo  19669  efgredlemc  19675  frgp0  19690  frgpmhm  19695  qusabl  19795  frgpnabllem1  19803  imasabl  19806  cycsubmcmn  19819  0cyg  19823  cycsubgcyg  19831  gsumval3  19837  gsumcllem  19838  gsumzaddlem  19851  gsumzsplit  19857  gsummptfzcl  19899  eldprd  19936  dprdcntz2  19970  dprd2d2  19976  dmdprdsplit2lem  19977  dmdprdsplit2  19978  dprdsplit  19980  ablfac2  20021  isrngd  20082  rngpropd  20083  imasrng  20086  qusrng  20089  ringurd  20094  isringd  20200  imasring  20239  xpsring1d  20242  dvdsrval  20270  isunit  20282  dvdsrpropd  20325  isirred  20328  isrnghm  20350  isrngim  20354  c0ghm  20370  c0snghm  20373  isrhm  20387  isrim0OLD  20390  isrim0  20392  islring  20449  issubrng  20456  opprsubrng  20468  issubrg  20480  opprsubrg  20502  resrhm2b  20511  rhmpropd  20518  rnghmresel  20529  elrngchom  20533  rnghmsubcsetclem1  20540  rnghmsubcsetclem2  20541  rngcid  20544  rngcsect  20545  rngciso  20547  funcrngcsetcALT  20550  zrinitorngc  20551  zrtermorngc  20552  rhmresel  20558  elringchom  20562  rhmsubcsetclem1  20569  rhmsubcsetclem2  20570  ringcid  20573  rhmsscrnghm  20574  rhmsubcrngclem1  20575  rhmsubcrngclem2  20576  ringcsect  20579  ringciso  20581  ringcbasbas  20582  zrtermoringc  20584  srhmsubc  20589  rhmsubclem3  20596  rhmsubclem4  20597  drngunit  20643  isdrngd  20674  isdrngdOLD  20676  issdrg  20697  sdrgunit  20705  isabv  20720  issrngd  20764  islmod  20770  lmodprop2d  20830  islss  20840  islssd  20841  lssats2  20906  ellspsn  20909  islmhm  20934  lmhmf1o  20953  lmhmima  20954  lmhmpreima  20955  reslmhm  20959  pwssplit3  20968  lmhmpropd  20980  islbs  20983  lspprel  21001  lspfixed  21038  lbsacsbs  21066  lbsextlem1  21068  lbsextlem2  21069  lbsextlem3  21070  lbsextlem4  21071  ixpsnbasval  21115  isridlrng  21129  rnglidlmmgm  21155  isridl  21162  quscrng  21193  rngqiprngimfolem  21200  rngqiprngimf1lem  21204  rngqiprngimfo  21211  islpidl  21235  lidldvgen  21244  irinitoringc  21389  pzriprnglem13  21403  pzriprnglem14  21404  zrhrhmb  21420  znf1o  21461  frgpcyg  21483  psgnevpmb  21496  isphld  21563  phlssphl  21568  elocv  21577  iscss  21592  isobs  21629  obs2ss  21638  dsmmfi  21647  dsmmelbas  21648  dsmmlss  21653  frlmelbas  21665  frlmlbs  21706  frlmup1  21707  ellspd  21711  islinds  21718  islindf2  21723  f1lindf  21731  islindf4  21747  assamulgscmlem2  21809  psrgrp  21865  mplsubglem  21908  mpllsslem  21909  mplmonmul  21943  subrgascl  21973  subrgasclcl  21974  mpfind  22014  ismhp  22027  gsumply1subr  22118  lply1binomsc  22198  matbas2d  22310  matecl  22312  matvscl  22318  mat1  22334  mat0dim0  22354  mat0dimid  22355  mat0dimscm  22356  mat1dimelbas  22358  dmatel  22380  scmatel  22392  scmateALT  22399  scmataddcl  22403  scmatsubcl  22404  smatvscl  22411  scmatghm  22420  mat1scmat  22426  mdetunilem7  22505  mdetunilem9  22507  smadiadetr  22562  cramerimplem2  22571  cramer0  22577  pmatcoe1fsupp  22588  cpmatpmat  22597  cpmatel  22598  cpmatacl  22603  cpmatinvcl  22604  mat2pmatghm  22617  mat2pmatmul  22618  decpmatmullem  22658  pmatcollpwlem  22667  pmatcollpw3fi1lem1  22673  pmatcollpwscmatlem1  22676  monmat2matmon  22711  chfacfscmul0  22745  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  cayhamlem1  22753  cpmadugsumlemB  22761  cpmadugsumlemC  22762  cpmadugsumlemF  22763  cayhamlem2  22771  istopon  22799  eltg  22844  eltg2  22845  eltop  22861  eltop2  22862  eltop3  22863  pptbas  22895  iscld  22914  neiss2  22988  isnei  22990  neiptopnei  23019  neiptopreu  23020  lpfval  23025  lpval  23026  islp  23027  maxlp  23034  islpi  23036  neitr  23067  restlp  23070  ordtbas2  23078  ordtrest2  23091  lmfval  23119  cnfval  23120  iscn  23122  iscnp  23124  tgcn  23139  tgcnp  23140  lmbrf  23147  cnpresti  23175  ist1  23208  ist1-2  23234  cnt1  23237  haust1  23239  cmpfi  23295  cmpfii  23296  1stcfb  23332  2ndc1stc  23338  1stcrest  23340  2ndcdisj  23343  1stcelcls  23348  nllyi  23362  subislly  23368  islocfin  23404  lfinpfin  23411  locfindis  23417  locfincf  23418  comppfsc  23419  kgenval  23422  elkgen  23423  kgencn2  23444  txbas  23454  eltx  23455  ptval  23457  ptpjpre1  23458  ptopn2  23471  ptpjopn  23499  ptclsg  23502  xkoccn  23506  txdis  23519  txdis1cn  23522  ptrescn  23526  hausdiag  23532  hauseqlcld  23533  txhaus  23534  xkohaus  23540  elqtop  23584  qtopeu  23603  kqcldsat  23620  hmeofval  23645  ptuncnv  23694  ptunhmeo  23695  elmptrab  23714  fbdmn0  23721  elfg  23758  elfilss  23763  filunirn  23769  fixufil  23809  elfm  23834  rnelfmlem  23839  rnelfm  23840  fmfnfmlem4  23844  elflim2  23851  flimtopon  23857  elflim  23858  hausflim  23868  flimcls  23872  flfnei  23878  isflf  23880  hausflf  23884  cnpflf  23888  cnflf  23889  txflf  23893  isfcls  23896  fclstopon  23899  isfcls2  23900  fclssscls  23905  fclsnei  23906  fclsfnflim  23914  flimfnfcls  23915  isfcf  23921  fcfelbas  23923  cnpfcf  23928  cnfcf  23929  flfcntr  23930  alexsublem  23931  alexsubALTlem3  23936  cnextfun  23951  cnextfvval  23952  cnextf  23953  cnextcn  23954  tmdgsum2  23983  tgpconncomp  24000  ghmcnp  24002  qustgplem  24008  eltsms  24020  haustsms  24023  tsmsgsum  24026  tsmssubm  24030  tsmssplit  24039  isust  24091  ustbas  24115  elutop  24121  ustuqtoplem  24127  ustuqtop4  24132  ustuqtop  24134  utopsnneiplem  24135  utopsnneip  24136  utopsnnei  24137  isusp  24149  isucn  24165  ucncn  24172  iscfilu  24175  neipcfilu  24183  iscusp  24186  cnextucn  24190  ispsmet  24192  ismet  24211  isxmet  24212  elblps  24275  elbl  24276  elmopn  24330  prdsbl  24379  neibl  24389  met1stc  24409  metrest  24412  prdsxmslem2  24417  txmetcnp  24435  txmetcn  24436  metustsym  24443  cfilucfil2  24449  elbl4  24451  metuel  24452  psmetutop  24455  restmetu  24458  metucn  24459  tngngp  24542  isnmhm  24634  zcld  24702  metnrmlem1a  24747  elcncf  24782  cncfcnvcn  24819  cnheibor  24854  lebnumlem1  24860  ishtpy  24871  isphtpy  24880  om1elbas  24932  elpi1  24945  pi1xfr  24955  pi1coghm  24961  tcphcph  25137  lmmbrf  25162  iscfil  25165  iscau  25176  iscauf  25180  caucfil  25183  iscmet  25184  cmetcaulem  25188  iscmet3lem1  25191  iscmet3lem2  25192  iscmet3  25193  bcthlem1  25224  cmsss  25251  cmetcusp1  25253  cmetcusp  25254  cmscsscms  25273  rrxcph  25292  minveclem3b  25328  ovolfioo  25368  ovolficc  25369  ovolctb  25391  ovoliunnul  25408  ovolshftlem1  25410  sca2rab  25413  ovolscalem1  25414  ovolicc2lem1  25418  ovolicc2lem2  25419  ovolicc2lem4  25421  ovolicc2lem5  25422  iundisj  25449  iunmbl2  25458  uniioombllem3  25486  vitalilem2  25510  vitalilem3  25511  mbfss  25547  i1faddlem  25594  i1fmullem  25595  mbfi1fseqlem2  25617  mbfi1fseqlem4  25619  mbfi1fseq  25622  itg2splitlem  25649  itg2split  25650  itg2monolem1  25651  itg2gt0  25661  isibl  25666  iblss2  25707  itgss3  25716  itgsplit  25737  ellimc  25774  limcmo  25783  cnlimc  25789  limciun  25795  limcun  25796  eldv  25799  dvbsss  25803  dvreslem  25810  elcpn  25836  dvaddf  25845  dvmulf  25846  dvcof  25852  rolle  25894  dvlip2  25900  dvivthlem1  25913  lhop1  25919  lhop2  25920  ftc1cn  25950  fta1glem2  26074  plyco0  26097  elply  26100  ply1termlem  26108  eltayl  26267  tayl0  26269  taylplem1  26270  taylplem2  26271  dvtaylp  26278  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  abelth  26351  cxpcn3  26658  rlimcnp  26875  fsumharmonic  26922  dchrelbas  27147  pntrsumbnd2  27478  ostth2lem2  27545  nolesgn2ores  27584  nogesgn1ores  27586  nosupprefixmo  27612  noinfprefixmo  27613  nosupcbv  27614  nosupdm  27616  nosupfv  27618  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1lem3  27622  nosupbnd1lem5  27624  nosupbnd2lem1  27627  noinfcbv  27629  noinfdm  27631  noinffv  27633  noinfres  27634  noinfbnd1lem1  27635  noinfbnd1lem3  27637  noinfbnd1lem5  27639  noinfbnd2lem1  27642  elmade  27779  elold  27781  ssltleft  27782  ssltright  27783  oldlim  27798  madebday  27811  newbday  27813  sltlpss  27819  cofcutr  27832  cofcutrtime  27835  lrrecval  27846  lrrecval2  27847  addsval  27869  precsexlem9  28117  precsexlem11  28119  sltonold  28162  onnolt  28167  onslt  28168  noseqrdgfn  28200  istrkgb  28382  istrkgcb  28383  istrkge  28384  istrkgl  28385  istrkgld  28386  axtgsegcon  28391  axtg5seg  28392  axtgbtwnid  28393  axtgpasch  28394  axtgupdim2  28398  axtgeucl  28399  tgdim01  28434  iscgrg  28439  isismt  28461  tglnunirn  28475  tglngval  28478  tgellng  28480  legval  28511  legov  28512  legov2  28513  ishlg  28529  mirreu3  28581  mirval  28582  mirfv  28583  mircgr  28584  mirbtwn  28585  ismir  28586  mireq  28592  symquadlem  28616  israg  28624  perpln1  28637  perpln2  28638  isperp  28639  islnopp  28666  outpasch  28682  ishpg  28686  iscgra  28736  dfcgra2  28757  isinag  28765  isleag  28774  iseqlg  28794  f1otrgitv  28797  f1otrg  28798  f1otrge  28799  ttgval  28802  ttgelitv  28810  elee  28821  brbtwn  28826  brcgr  28827  axlowdimlem16  28884  ebtwntg  28909  elntg2  28912  upgrex  29019  edgupgr  29061  upgredg  29064  edglnl  29070  numedglnl  29071  uhgr2edg  29135  umgr2edg1  29138  usgredg2vlem1  29152  usgredg2vlem2  29153  ushgredgedg  29156  ushgredgedgloop  29158  uhgrspansubgrlem  29217  fusgrfisstep  29256  nbgrval  29263  nbgrel  29267  nbupgrel  29272  nbgr2vtx1edg  29277  nbuhgr2vtx1edgblem  29278  nbuhgr2vtx1edgb  29279  nbusgreledg  29280  usgrnbcnvfv  29292  uvtxval  29314  uvtxel  29315  uvtx01vtx  29324  uvtxusgrel  29330  nbcplgr  29361  cplgr3v  29362  cusgrexi  29370  structtocusgr  29373  vtxdgfval  29395  vtxdg0v  29401  vtxdeqd  29405  vtxdun  29409  1loopgrnb0  29430  1loopgrvd0  29432  1hevtxdg0  29433  1hevtxdg1  29434  1egrvtxdg1  29437  umgr2v2evtxel  29450  umgr2v2enb1  29454  umgr2v2evd2  29455  vtxdginducedm1lem4  29470  vtxdginducedm1  29471  finsumvtxdg2sstep  29477  ewlksfval  29529  isewlk  29530  wksfval  29537  iswlk  29538  uspgr2wlkeq  29574  wlkres  29598  dfpth2  29659  usgr2pthlem  29693  clwlkcompim  29710  uspgrn2crct  29738  wwlks  29765  iswwlksn  29768  wwlknvtx  29775  wlkiswwlks2  29805  wwlksm1edg  29811  wwlksnred  29822  wwlksnext  29823  wwlksnredwwlkn  29825  wwlksnredwwlkn0  29826  wwlksnwwlksnon  29845  wspn0  29854  usgr2wspthons3  29894  rusgrnumwwlkb0  29901  clwwlk  29912  clwwlkccatlem  29918  clwlkclwwlklem2a4  29926  clwlkclwwlk  29931  clwwisshclwwslem  29943  clwwlkinwwlk  29969  clwwlkel  29975  clwwlkf  29976  clwwlkext2edg  29985  wwlksext2clwwlk  29986  wwlksubclwwlk  29987  clwwnisshclwwsn  29988  eleclclwwlknlem2  29990  erclwwlknsym  29999  erclwwlkntr  30000  umgrhashecclwwlk  30007  clwwlkvbij  30042  eupth2lem3lem3  30159  eupth2lem3lem4  30160  eupth2lem3lem6  30162  eupth2lemb  30166  eucrct2eupth  30174  fusgreg2wsplem  30262  2clwwlklem  30272  2clwwlk2clwwlklem  30275  2clwwlkel  30278  2clwwlk2clwwlk  30279  extwwlkfabel  30282  clwwlknonclwlknonf1o  30291  dlwwlknondlwlknonf1olem1  30293  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  ex-res  30370  isssp  30653  sspn  30665  islno  30682  isblo  30711  nmlno0  30724  ishmo  30740  dipdir  30771  dipass  30774  ubthlem1  30799  ubthlem2  30800  htthlem  30846  htth  30847  ocel  31210  ocnel  31227  shsel  31243  shsel2  31251  shmodsi  31318  pjhtheu  31323  pjeq  31328  axpjpj  31349  pjoc2  31368  elspani  31472  h1de2ctlem  31484  elspansn  31495  elspansn2  31496  elnlfn  31857  eleigvec  31886  riesz3i  31991  cbviunf  32484  iuneq12daf  32485  iunrdx  32492  iunrnmptss  32494  cbvdisjf  32500  disjorf  32508  disjabrex  32511  disjabrexf  32512  iundisjf  32518  disjrdx  32520  brab2d  32535  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  isfxp  33125  cntrval2  33128  inftmrel  33134  isinftm  33135  isslmd  33155  urpropd  33183  elrgspn  33197  erlval  33209  rlocval  33210  rloccring  33221  rloc1r  33223  domnpropd  33227  isdrng4  33245  fracfld  33258  resv1r  33311  ellspds  33339  ellpi  33344  lbslsp  33348  rhmimaidl  33403  isprmidl  33409  qsidomlem1  33423  qsidomlem2  33424  ismxidl  33433  crngmxidl  33440  drng0mxidl  33447  opprqus0g  33461  qsfld  33469  isrprm  33488  rsprprmprmidlb  33494  ressply1evls1  33534  ply1mulrtss  33550  dimpropd  33604  lbslsat  33612  extdg1id  33661  fldextrspunlsplem  33668  fldextrspunlsp  33669  elirng  33681  ply1annidllem  33691  constrsuc  33728  constrconj  33735  constrllcllem  33742  constrlccllem  33743  constrcccllem  33744  nn0constr  33751  smatrcl  33786  smatcl  33792  ist0cld  33823  txomap  33824  locfinreflem  33830  zarclsiin  33861  zart0  33869  rhmpreimacnlem  33874  metidval  33880  cnre2csqima  33901  ordtrest2NEW  33913  fmcncfil  33921  fsumcvg4  33940  ofcfval  34088  measvuni  34204  meascnbl  34209  faeval  34236  ismbfm  34241  elunirnmbfm  34242  imambfm  34253  elcarsg  34296  itgeq12dv  34317  issibf  34324  eulerpartlems  34351  eulerpartlemgc  34353  eulerpartlemgvv  34367  eulerpartlemgu  34368  eulerpart  34373  rrvmbfm  34433  elorvc  34451  elorrvc  34455  dstfrvunirn  34466  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemsima  34507  ballotlemrv  34511  fzssfzo  34530  signstfvn  34560  signstfvneq0  34563  signstres  34566  repr0  34602  reprinrn  34609  reprdifc  34618  hgt750lemg  34645  hgt750lemb  34647  istrkg2d  34657  axtgupdim2ALTV  34659  afsval  34662  brafs  34663  bnj945  34763  bnj1400  34825  bnj18eq1  34917  bnj916  34923  bnj1014  34951  bnj1015  34952  bnj1110  34972  bnj1417  35031  onvf1odlem3  35092  vonf1owev  35095  revpfxsfxrev  35103  cplgredgex  35108  pfxwlk  35111  revwlk  35112  subfacp1lem2b  35168  subfacp1lem4  35170  subfacp1lem5  35171  subfacp1lem6  35172  ptpconn  35220  cvmscbv  35245  iscvm  35246  cvmsi  35252  cvmsval  35253  cvmliftmolem1  35268  cvmlift2lem12  35301  cvmlift2lem13  35302  cvmlift3lem7  35312  snmlval  35318  satfv1  35350  satfvsucsuc  35352  satfrnmapom  35357  satf0op  35364  satf0n0  35365  sat1el2xp  35366  fmlafvel  35372  isfmlasuc  35375  fmlaomn0  35377  gonan0  35379  goaln0  35380  gonar  35382  goalr  35384  satffunlem1lem2  35390  satffunlem2lem2  35393  satfv0fvfmla0  35400  satef  35403  satefvfmla0  35405  sategoelfvb  35406  satfv1fvfmla1  35410  mrsubfval  35495  mrsubvrs  35509  mclsrcl  35548  mclsval  35550  mppsval  35559  mclsppslem  35570  opelco3  35762  wsuclem  35813  funtransport  36019  fvtransport  36020  brcolinear  36047  colineardim1  36049  funray  36128  fvray  36129  funline  36130  fvline  36132  lineelsb2  36136  fwddifval  36150  fwddifnval  36151  rankelg  36156  rankeq1o  36159  elhf2  36163  0hf  36165  rmoeqbidv  36201  disjeq12dv  36203  ixpeq12dv  36204  prodeq12sdv  36206  itgeq12sdv  36207  cbvralvw2  36214  cbvrexvw2  36215  cbvrmovw2  36216  cbvreuvw2  36217  cbvcsbvw2  36219  cbviunvw2  36220  cbviinvw2  36221  cbvmptvw2  36222  cbvdisjvw2  36223  cbvmpo1vw2  36231  cbvmpo2vw2  36232  cbvsbcdavw  36245  cbvcsbdavw  36247  cbvcsbdavw2  36248  cbviundavw  36250  cbviindavw  36251  cbvdisjdavw  36256  cbvrabdavw2  36273  cbviundavw2  36274  cbviindavw2  36275  cbvmptdavw2  36276  cbvdisjdavw2  36277  cbvriotadavw2  36278  cbvmpo1davw2  36280  cbvmpo2davw2  36281  cbvsumdavw2  36283  neibastop2lem  36348  neibastop3  36350  eltail  36362  bj-projeq  36980  bj-projval  36984  bj-restsn  37070  opelopabbv  37131  brabd0  37135  bj-eldiag  37164  bj-eldiag2  37165  mptsnunlem  37326  dissneqlem  37328  iooelexlt  37350  relowlssretop  37351  rdgellim  37364  exrecfnlem  37367  finxpeq1  37374  finxpreclem6  37384  pibp21  37403  curf  37592  uncf  37593  curunc  37596  unccur  37597  fin2so  37601  lindsadd  37607  lindsdom  37608  lindsenlbs  37609  matunitlindflem1  37610  matunitlindflem2  37611  matunitlindf  37612  ptrest  37613  ptrecube  37614  poimirlem2  37616  poimirlem8  37622  poimirlem17  37631  poimirlem18  37632  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem24  37638  poimirlem26  37640  poimirlem29  37643  heicant  37649  mblfinlem1  37651  mblfinlem2  37652  volsupnfl  37659  itg2addnclem  37665  itg2gt0cn  37669  indexdom  37728  incsequz  37742  istotbnd  37763  istotbnd3  37765  0totbnd  37767  sstotbnd  37769  sstotbnd3  37770  isbnd  37774  prdstotbnd  37788  cntotbnd  37790  isismty  37795  heibor1lem  37803  heiborlem2  37806  heiborlem3  37807  heibor  37815  isass  37840  exidcl  37870  exidreslem  37871  elghomlem2OLD  37880  rngoidmlem  37930  rngo1cl  37933  divrngcl  37951  isdrngo2  37952  isrngohom  37959  isrngoiso  37972  isriscg  37978  iscom2  37989  iscringd  37992  isidl  38008  ispridl  38028  ismaxidl  38034  ac6s6  38166  dmecd  38292  releldmqs  38650  releldmqscoss  38652  erimeq2  38670  eldisjlem19  38802  membpartlem19  38803  prter3  38875  islshp  38972  islsat  38984  lcvfbr  39013  islfl  39053  ellkr  39082  islshpkrN  39113  ldual1dim  39159  isopos  39173  cmtfvalN  39203  cvrfval  39261  isat  39279  islln  39500  islpln  39524  islvol  39567  isline  39733  ispointN  39736  ispsubsp  39739  elpmap  39752  elpmapat  39758  elpadd  39793  paddclN  39836  elpclN  39886  elpcliN  39887  pclfinN  39894  pclcmpatN  39895  ispsubclN  39931  iswatN  39988  islhp  39990  islaut  40077  ispautN  40093  isldil  40104  isltrn  40113  isdilN  40148  istrnN  40151  istendo  40754  dvhb1dimN  40980  erng1lem  40981  erngdvlem4-rN  40993  diaelval  41027  diaeldm  41030  dia1dimid  41057  cdlemm10N  41112  dibopelvalN  41137  dibopelval2  41139  dibelval3  41141  dibelval1st  41143  dibelval2nd  41146  dibeldmN  41152  dibvalrel  41157  dibglbN  41160  dicffval  41168  dicfval  41169  dicopelval  41171  dicelvalN  41172  dicelval3  41174  dicvalrelN  41179  dicelval1sta  41181  diclspsn  41188  dihopelvalbN  41232  dihopelvalcqat  41240  dihopelvalcpre  41242  dihvalrel  41273  dih1  41280  dihmeetlem4preN  41300  dihmeetlem13N  41313  dih1dimatlem  41323  dochnel2  41386  dihjatcclem4  41415  dvh2dim  41439  dvh3dim  41440  dvh4dimN  41441  dochfln0  41471  lpolsetN  41476  islpolN  41477  lcfrvalsnN  41535  lcfrlem21  41557  lcfrlem27  41563  lcfrlem37  41573  lcfr  41579  lcdlss  41613  mapdcv  41654  hdmap1fval  41790  hdmapffval  41820  hdmapfval  41821  hdmapval  41822  hgmapffval  41879  hgmapfval  41880  hdmapellkr  41908  hlhilhillem  41954  fzsplitnd  41970  isprimroot  42081  primrootsunit1  42085  primrootscoprmpow  42087  primrootscoprbij  42090  aks6d1c1p2  42097  aks6d1c1p3  42098  aks6d1c1p4  42099  aks6d1c1p5  42100  aks6d1c1p6  42102  aks6d1c1  42104  evl1gprodd  42105  sticksstones11  42144  sticksstones12a  42145  rhmqusspan  42173  grpods  42182  fzosumm1  42238  frlmfielbas  42488  frlmsnic  42528  psrmnd  42533  isnacs  42692  mrefg2  42695  elmzpcl  42714  mzpcompact2  42740  eldiophb  42745  elpell1qr  42835  elpell14qr  42837  elpell1234qr  42839  pw2f1ocnv  43026  pw2f1o2val2  43029  aomclem4  43046  aomclem6  43048  islssfg2  43060  imasgim  43089  lnr2i  43105  elmnc  43125  rngunsnply  43158  onexomgt  43230  onexlimgt  43232  onexoegt  43233  oaordnr  43285  omnord1  43294  oenord1  43305  cantnfresb  43313  tfsconcatun  43326  tfsconcat0i  43334  ofoaf  43344  naddcnff  43351  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddcnfid2  43357  naddcnfass  43358  naddwordnexlem4  43390  fiinfi  43562  sqrtcvallem1  43620  elintima  43642  eliunov2  43668  ov2ssiunov2  43689  brtrclfv2  43716  rfovcnvf1od  43993  rfovcnvfvd  43996  fsovrfovd  43998  fsovfvd  43999  fsovcnvlem  44002  ntrclsfv1  44044  ntrclselnel1  44046  ntrclsneine0lem  44053  ntrneifv1  44068  ntrneifv2  44069  ntrneiel  44070  gneispace2  44121  gneispacess2  44135  extoimad  44153  mnringelbased  44206  dvconstbi  44323  bccbc  44334  wfac8prim  44992  permaxrep  44996  permac8prim  45004  eliin2f  45098  iineq12dv  45100  rabbida2  45126  disjinfi  45186  unirnmap  45202  elmptima  45252  iuneqfzuzlem  45330  iooiinioc  45554  fsumiunss  45573  fsumsupp0  45576  lptre2pt  45638  icccncfext  45885  cncfiooicclem1  45891  dvnprodlem2  45945  stoweidlem27  46025  stoweidlem29  46027  stoweidlem31  46029  stoweidlem34  46032  stoweidlem48  46046  stoweidlem59  46057  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem2  46107  fourierdlem3  46108  fourierdlem25  46130  fourierdlem32  46137  fourierdlem33  46138  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem62  46166  fourierdlem70  46174  fourierdlem80  46184  fourierdlem92  46196  fourierdlem93  46197  fourierdlem101  46205  etransclem37  46269  sge0val  46364  sge0f1o  46380  sge0iunmptlemre  46413  sge0iunmpt  46416  iundjiun  46458  caragenel  46493  ovncvrrp  46562  ovnsubaddlem1  46568  ovnsubadd  46570  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hoidmvle  46598  ovncvr2  46609  hspdifhsp  46614  hoiqssbl  46623  hspmbllem2  46625  hspmbl  46627  opnvonmbllem1  46630  isvonmbl  46636  ovnovollem1  46654  issmflem  46725  smflimlem3  46771  smflimlem4  46772  smflim  46775  smfmullem2  46790  smflimmpt  46808  smfsuplem1  46809  smflimsuplem1  46818  smflimsuplem3  46820  smflimsuplem4  46821  smflimsuplem7  46824  smflimsup  46826  tworepnotupword  46884  fcores  47068  fcoresf1  47070  afvelrnb  47164  afvelrnb0  47165  afv2co2  47258  el1fzopredsuc  47326  iccpart  47417  iccpartgtprec  47421  iccpartiltu  47423  iccpartigtl  47424  iccpartltu  47426  iccpartgtl  47427  iccpartgt  47428  iccpartleu  47429  iccpartgel  47430  iccelpart  47434  iccpartiun  47435  icceuelpart  47437  fargshiftfv  47440  fargshiftfo  47443  sprel  47485  prprelb  47517  prprelprb  47518  fpprel  47729  sbgoldbo  47788  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem3  47808  bgoldbtbnd  47810  clnbgrval  47823  elclnbgrelnbgr  47826  clnbgrel  47829  clnbupgrel  47835  vopnbgrel  47854  isubgredg  47866  upgrimwlklem3  47899  upgrimwlklem5  47901  upgrimpths  47909  grtriprop  47940  isgrtri  47942  grtriclwlk3  47944  stgredgel  47956  gpgvtxel  48038  gpgiedgdmel  48040  gpgedgel  48041  opgpgvtx  48046  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpg3kgrtriex  48080  upwlksfval  48123  isupwlk  48124  intop  48191  isclintop  48195  assintop  48197  isassintop  48198  assintopcllaw  48200  uzlidlring  48223  elrngchomALTV  48257  rngccatidALTV  48260  rngcsectALTV  48263  rngcisoALTV  48265  rhmsubcALTVlem3  48271  rhmsubcALTVlem4  48272  funcringcsetcALTV2lem7  48284  funcringcsetcALTV2lem9  48286  elringchomALTV  48291  ringccatidALTV  48294  ringcsectALTV  48297  ringcisoALTV  48299  ringcbasbasALTV  48300  funcringcsetclem7ALTV  48307  funcringcsetclem9ALTV  48309  srhmsubcALTV  48313  cbvmpox2  48324  ply1sclrmsm  48372  dmatALTbasel  48391  lcoval  48401  lindslinindsimp1  48446  lindslinindsimp2  48452  lmod1  48481  elbigo  48540  elbigo2  48541  elbigolo1  48546  dig2nn0ld  48593  naryfvalel  48619  rrxlines  48722  rrxlinesc  48724  rrxlinec  48725  eenglngeehlnm  48728  elrrx2linest2  48734  rrxsphere  48737  itsclc0  48760  itsclc0b  48761  itsclinecirc0  48762  itsclinecirc0b  48763  itscnhlinecirc02p  48774  brab2dd  48816  f1omo  48881  f1omoOLD  48882  lubeldm2d  48946  glbeldm2d  48947  catprs  49000  sectpropdlem  49025  nelsubc3lem  49059  initc  49080  imaid  49143  upfval  49165  upfval2  49166  upfval3  49167  uppropd  49170  oppcinito  49224  oppctermo  49225  oppczeroo  49226  initopropd  49232  termopropd  49233  isthinc  49408  isthincd2lem1  49414  thincmoALT  49418  thincmod  49419  isthincd  49425  thincpropd  49431  indcthing  49449  discthing  49450  prsthinc  49453  termcterm  49502  termc2  49507  isinito4  49536  2arwcatlem1  49584  setc1onsubc  49591  cnelsubclem  49592  ranval3  49620  lmdfval2  49644  cmdfval2  49645  termolmd  49659  elsetrecslem  49688