Theorem eleq2d 2825

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 2732	. . . 4 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	1, 2	sylib 219	. . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		anbi2 640	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	alexbii 1840	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6	3, 5	syl 17	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
7		dfclel 2815	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
8		dfclel 2815	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4g 315	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545   = wceq 1547  ∃wex 1786   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  eleq2  2828  eleq12d  2833  eleqtrd  2841  neleqtrd  2861  eqabrd  2880  raleqbidv  3313  rexeqbidv  3314  reueqbidv  3380  rabeqbidva  3407  elabd2  3608  sbcbid  3777  sbcbi2  3781  csbeq2d  3837  csbeq2dv  3838  cbvcsbw  3841  cbvcsb  3842  cbvcsbv  3843  csbie  3866  csbied  3867  csbie2g  3871  cbvralcsf  3873  cbvreucsf  3875  cbvrabcsf  3876  sbcel12  4339  sbcel1g  4344  sbcel2  4346  prel12g  4795  eliuni  4927  iuneqconst  4933  iuneq12df  4948  iuneq12d  4951  cbviun  4964  cbviin  4965  cbviung  4966  cbviing  4967  cbviunv  4968  cbviinv  4969  iinxsng  5017  iinxprg  5018  iunxsng  5019  iunxsngf  5021  cbvdisj  5049  cbvdisjv  5050  disjor  5054  disjiund  5063  mpteq12da  5155  mpteq12f  5157  mpteq12dva  5158  axpweq  5279  rabxfrd  5346  rbropapd  5504  opeliunxp  5685  opeliun2xp  5686  opeliunxp2  5780  iunxpf  5790  elimampt  5995  elrelimasn  6038  elimasni  6043  imadifssran  6102  xpdifid  6119  ressn  6236  funfni  6591  fnbr  6593  dffv3  6823  elfv2ex  6870  fvelrnb  6887  foelcdmi  6888  fvun1  6918  fvco2  6924  funcnvmpt  6937  elfvmptrab1w  6963  elfvmptrab1  6964  elfvmptrab  6965  elpreima  6999  dff3  7041  fmptco  7071  fnelfp  7119  fnelnfp  7121  tpres  7145  fnprb  7152  fntpb  7153  funfvima3  7180  eluniima  7194  dff13  7198  f1ounsn  7216  f1eqcocnv  7245  isoini  7282  riotaeqdv  7314  mpoeq123dva  7430  cbvmpox  7449  elimampo  7493  ovelrn  7532  elovmpod  7600  elovmpo  7601  elovmporab  7602  elovmporab1w  7603  elovmporab1  7604  elovmpt3rab1  7616  fiun  7885  f1iun  7886  zfrep6OLD  7897  fmpox  8009  el2mpocsbcl  8024  el2mpocl  8025  bropopvvv  8029  bropfvvvv  8031  xpord2indlem  8087  xpord3inddlem  8094  elsuppfng  8109  elsuppfn  8110  suppfnss  8129  opeliunxp2f  8150  mpoxopn0yelv  8153  mpoxopovel  8160  rntpos  8179  mpocurryd  8209  fpr2  8244  wfr2  8267  onoviun  8273  smoel  8290  smoiso  8292  smoel2  8293  smo11  8294  tfrlem9  8314  oalimcl  8485  oaass  8486  omordi  8491  omordlim  8502  omlimcl  8503  odi  8504  omeulem1  8507  omeulem2  8508  oen0  8512  oeordi  8513  oeordsuc  8520  oelimcl  8526  oeeulem  8527  oeeui  8528  nnmordi  8557  oaabs2  8575  omabs  8577  omsmolem  8583  ereldm  8687  iiner  8726  elmapg  8776  elpmg  8780  elixpsn  8875  ixpsnf1o  8876  boxriin  8878  omxpenlem  9006  pw2f1olem  9009  phplem2  9129  php3  9133  infn0  9202  elfi  9316  dffi3  9334  marypha2lem2  9339  ordiso2  9420  wemapsolem  9455  elharval  9466  inf3lemd  9539  inf3lem1  9540  inf3lem2  9541  inf3lem3  9542  cantnfs  9578  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1  9601  ttrclselem2  9638  trcl  9640  frr2  9675  r1sdom  9689  r1ordg  9693  r1pwss  9699  tz9.12lem3  9704  tz9.12  9705  r1elwf  9711  rankr1ai  9713  rankidb  9715  rankr1bg  9718  rankval2  9733  rankunb  9765  tcrank  9799  acni  9958  acni2  9959  acndom  9964  infpwfien  9975  alephnbtwn  9984  cardaleph  10002  cardinfima  10010  iunfictbso  10027  dfac3  10034  dfac5lem5  10040  dfac5  10042  dfac9  10050  dfac12r  10060  kmlem2  10065  kmlem12  10075  kmlem13  10076  kmlem14  10077  ackbij2lem3  10153  ackbij2  10155  cofsmo  10182  alephsing  10189  fin23lem30  10255  isf32lem9  10274  itunisuc  10332  axcc2lem  10349  axcc3  10351  domtriomlem  10355  axdc2lem  10361  axdc2  10362  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  ac6c4  10394  zorn2lem1  10409  ttukeylem6  10427  pwcfsdom  10497  axregndlem2  10517  axinfndlem1  10519  axacndlem4  10524  axacnd  10526  pwfseqlem1  10572  inar1  10689  inatsk  10692  gruurn  10712  grur1  10734  eltskm  10757  genpelv  10914  eluz1  12783  elixx1  13298  elixx3g  13302  elioo2  13330  elfz1  13457  elfz2  13459  elfzp1  13519  fzpr  13524  fzsuc2  13527  fzrev3  13535  elfzp12  13548  fzm1  13552  elfzo  13606  fz0add1fz1  13681  elfzo0l  13702  elfzom1b  13712  fzosplitsni  13725  elfzr  13727  elfzlmr  13728  zmodidfzo  13850  seqp1  13969  seqf1o  13996  bcval  14257  bcpasc  14274  hashf1lem1  14408  fundmge2nop0  14455  wrdmap  14499  elovmpowrd  14511  ccatfval  14526  elfzelfzccat  14533  ccatlid  14540  ccatass  14542  ccatrn  14543  ccatalpha  14547  swrdfv2  14615  ccatswrd  14622  swrdccat2  14623  pfxfv  14636  pfxeq  14649  ccatpfx  14654  swrdswrd  14658  swrdpfx  14660  pfxpfx  14661  cats1un  14674  swrdccatfn  14677  swrdccatin1  14678  pfxccatin12lem4  14679  pfxccatin12lem1  14681  swrdccatin2  14682  pfxccatin12lem2c  14683  pfxccatin12lem2  14684  swrdccat3blem  14692  swrdccatin1d  14696  swrdccatin2d  14697  pfxccatin12d  14698  revccat  14719  revrev  14720  repswpfx  14738  repswccat  14739  cshwidxmod  14756  2cshw  14766  cshwcshid  14780  cshwcsh2id  14781  cshimadifsn  14782  cshimadifsn0  14783  revco  14787  ccatco  14788  cshco  14789  swrdco  14790  ofccat  14922  shftfn  15026  shftval  15027  limsupgle  15430  ello12  15469  elo12  15480  isercolllem3  15620  sumeq1  15642  fsumsplit  15694  sumsplit  15721  fsum2dlem  15723  fsumcom2  15727  fsumparts  15760  explecnv  15821  pwdif  15824  fprodser  15905  fprodsplit  15922  fprod2dlem  15936  fprodcom2  15940  eftlub  16067  divalgmod  16366  bitsval  16384  bitsp1e  16392  bitsp1o  16393  sadfval  16412  sadcp1  16415  sadval  16416  sadcadd  16418  sadadd2  16420  saddisjlem  16424  sadadd  16427  sadass  16431  smufval  16437  smuval  16441  smuval2  16442  smupvallem  16443  smu01lem  16445  smueqlem  16450  smumul  16453  bezoutlem2  16500  bezoutlem4  16502  algfx  16540  eucalgcvga  16546  reumodprminv  16766  nnnn0modprm0  16768  unbenlem  16870  prmreclem5  16882  vdwapval  16935  vdwapun  16936  vdwnnlem1  16957  vdwnn  16960  ramval  16970  0ram  16982  ramub1lem2  16989  prmgaplem7  17019  prmlem0  17067  elrest  17381  prdsbasmpt  17424  prdsleval  17431  prdsbasmpt2  17436  pwselbasb  17442  imasaddfnlem  17483  imasvscafn  17492  divsfval  17502  ismre  17543  mreunirn  17554  mrisval  17587  ismri  17588  isacs  17608  catidd  17637  iscatd2  17638  ismon  17691  isepi  17698  sectffval  17708  sectfval  17709  dfiso2  17730  cicsym  17762  issubc  17793  catsubcat  17797  isfunc  17822  funcres  17854  funcpropd  17860  ffthiso  17889  isnat  17908  isnat2  17909  fuciso  17936  initoval  17951  termoval  17952  isinito  17954  istermo  17955  iszeroo  17956  isinitoi  17957  istermoi  17958  initoid  17959  termoid  17960  iszeroi  17967  2initoinv  17968  initoeu1  17969  initoeu2  17974  2termoinv  17975  termoeu1  17976  arwhoma  18003  elsetchom  18039  setcmon  18045  setcepi  18046  setciso  18049  catciso  18069  elestrchom  18085  estrcbasbas  18088  funcestrcsetclem7  18103  funcestrcsetclem8  18104  funcestrcsetclem9  18105  fthestrcsetc  18107  fullestrcsetc  18108  equivestrcsetc  18109  setc1strwun  18110  funcsetcestrclem7  18118  funcsetcestrclem8  18119  funcsetcestrclem9  18120  fthsetcestrc  18122  fullsetcestrc  18123  hofcl  18216  hofpropd  18224  yonedalem4c  18234  yonedainv  18238  yonffthlem  18239  lubeldm  18308  glbeldm  18321  joindef  18331  meetdef  18345  poslubdg  18369  acsficl2d  18509  acsmapd  18511  psref  18531  psss  18537  dirge  18560  chnccats1  18582  chnccat  18583  chnrev  18584  mgmpropd  18610  issstrmgm  18612  grpidval  18620  grpidpropd  18621  grpidd  18630  ismgmhm  18655  issubmgm  18661  issgrpd  18689  sgrppropd  18690  ismndd  18715  mndpropd  18718  imasmnd2  18733  imasmnd  18734  xpsmnd0  18737  ismhm  18744  issubm  18762  gsumsgrpccat  18799  elefmndbas2  18833  smndex1mndlem  18871  imasgrp2  19022  imasgrp  19023  issubg  19093  subginv  19100  isnsg  19121  eqg0el  19149  quselbas  19150  isghm  19181  isghmOLD  19182  resghm2b  19200  conjnmzb  19219  conjnsg  19220  ghmpropd  19222  isga  19257  elcntz  19288  elcntzsn  19291  cntzrcl  19293  resscntz  19299  symgextf1  19387  gsmsymgreqlem2  19397  f1otrspeq  19413  pmtrfrn  19424  pmtrdifellem3  19444  pmtrdifellem4  19445  psgnunilem1  19459  psgnunilem5  19460  psgnunilem2  19461  psgnunilem3  19462  psgneldm2  19470  psgnfitr  19483  psgnsn  19486  gexdvds  19550  gex1  19557  isslw  19574  sylow3lem2  19594  lsmelvalx  19606  pj1ghm  19669  efgtlen  19692  efgsfo  19705  efgredlemc  19711  frgp0  19726  frgpmhm  19731  qusabl  19831  frgpnabllem1  19839  imasabl  19842  cycsubmcmn  19855  0cyg  19859  cycsubgcyg  19867  gsumval3  19873  gsumcllem  19874  gsumzaddlem  19887  gsumzsplit  19893  gsummptfzcl  19935  eldprd  19972  dprdcntz2  20006  dprd2d2  20012  dmdprdsplit2lem  20013  dmdprdsplit2  20014  dprdsplit  20016  ablfac2  20057  isrngd  20145  rngpropd  20146  imasrng  20149  qusrng  20152  ringurd  20157  isringd  20263  imasring  20301  xpsring1d  20304  dvdsrval  20332  isunit  20344  dvdsrpropd  20387  isirred  20390  isrnghm  20412  isrngim  20416  c0ghm  20432  c0snghm  20435  isrhm  20449  isrim0  20453  islring  20512  issubrng  20519  opprsubrng  20531  issubrg  20543  opprsubrg  20565  resrhm2b  20574  rhmpropd  20581  rnghmresel  20592  elrngchom  20596  rnghmsubcsetclem1  20603  rnghmsubcsetclem2  20604  rngcid  20607  rngcsect  20608  rngciso  20610  funcrngcsetcALT  20613  zrinitorngc  20614  zrtermorngc  20615  rhmresel  20621  elringchom  20625  rhmsubcsetclem1  20632  rhmsubcsetclem2  20633  ringcid  20636  rhmsscrnghm  20637  rhmsubcrngclem1  20638  rhmsubcrngclem2  20639  ringcsect  20642  ringciso  20644  ringcbasbas  20645  zrtermoringc  20647  srhmsubc  20652  rhmsubclem3  20659  rhmsubclem4  20660  drngunit  20706  isdrngd  20737  isdrngdOLD  20739  issdrg  20760  sdrgunit  20768  isabv  20783  issrngd  20827  islmod  20854  lmodprop2d  20914  islss  20924  islssd  20925  lssats2  20990  ellspsn  20993  islmhm  21017  lmhmf1o  21036  lmhmima  21037  lmhmpreima  21038  reslmhm  21042  pwssplit3  21051  lmhmpropd  21063  islbs  21066  lspprel  21084  lspfixed  21121  lbsacsbs  21149  lbsextlem1  21151  lbsextlem2  21152  lbsextlem3  21153  lbsextlem4  21154  ixpsnbasval  21198  isridlrng  21212  rnglidlmmgm  21238  isridl  21245  quscrng  21276  rngqiprngimfolem  21283  rngqiprngimf1lem  21287  rngqiprngimfo  21294  islpidl  21318  lidldvgen  21327  irinitoringc  21454  pzriprnglem13  21468  pzriprnglem14  21469  zrhrhmb  21485  znf1o  21526  frgpcyg  21548  psgnevpmb  21562  isphld  21629  phlssphl  21634  elocv  21643  iscss  21658  isobs  21695  obs2ss  21704  dsmmfi  21713  dsmmelbas  21714  dsmmlss  21719  frlmelbas  21731  frlmlbs  21772  frlmup1  21773  ellspd  21777  islinds  21784  islindf2  21789  f1lindf  21797  islindf4  21813  assamulgscmlem2  21875  psrgrp  21931  mplsubglem  21973  mpllsslem  21974  mplmonmul  22012  subrgascl  22042  subrgasclcl  22043  mpfind  22091  ismhp  22128  gsumply1subr  22218  lply1binomsc  22297  matbas2d  22406  matecl  22408  matvscl  22414  mat1  22430  mat0dim0  22450  mat0dimid  22451  mat0dimscm  22452  mat1dimelbas  22454  dmatel  22476  scmatel  22488  scmateALT  22495  scmataddcl  22499  scmatsubcl  22500  smatvscl  22507  scmatghm  22516  mat1scmat  22522  mdetunilem7  22601  mdetunilem9  22603  smadiadetr  22658  cramerimplem2  22667  cramer0  22673  pmatcoe1fsupp  22684  cpmatpmat  22693  cpmatel  22694  cpmatacl  22699  cpmatinvcl  22700  mat2pmatghm  22713  mat2pmatmul  22714  decpmatmullem  22754  pmatcollpwlem  22763  pmatcollpw3fi1lem1  22769  pmatcollpwscmatlem1  22772  monmat2matmon  22807  chfacfscmul0  22841  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  cayhamlem1  22849  cpmadugsumlemB  22857  cpmadugsumlemC  22858  cpmadugsumlemF  22859  cayhamlem2  22867  istopon  22895  eltg  22940  eltg2  22941  eltop  22957  eltop2  22958  eltop3  22959  pptbas  22991  iscld  23010  neiss2  23084  isnei  23086  neiptopnei  23115  neiptopreu  23116  lpfval  23121  lpval  23122  islp  23123  maxlp  23130  islpi  23132  neitr  23163  restlp  23166  ordtbas2  23174  ordtrest2  23187  lmfval  23215  cnfval  23216  iscn  23218  iscnp  23220  tgcn  23235  tgcnp  23236  lmbrf  23243  cnpresti  23271  ist1  23304  ist1-2  23330  cnt1  23333  haust1  23335  cmpfi  23391  cmpfii  23392  1stcfb  23428  2ndc1stc  23434  1stcrest  23436  2ndcdisj  23439  1stcelcls  23444  nllyi  23458  subislly  23464  islocfin  23500  lfinpfin  23507  locfindis  23513  locfincf  23514  comppfsc  23515  kgenval  23518  elkgen  23519  kgencn2  23540  txbas  23550  eltx  23551  ptval  23553  ptpjpre1  23554  ptopn2  23567  ptpjopn  23595  ptclsg  23598  xkoccn  23602  txdis  23615  txdis1cn  23618  ptrescn  23622  hausdiag  23628  hauseqlcld  23629  txhaus  23630  xkohaus  23636  elqtop  23680  qtopeu  23699  kqcldsat  23716  hmeofval  23741  ptuncnv  23790  ptunhmeo  23791  elmptrab  23810  fbdmn0  23817  elfg  23854  elfilss  23859  filunirn  23865  fixufil  23905  elfm  23930  rnelfmlem  23935  rnelfm  23936  fmfnfmlem4  23940  elflim2  23947  flimtopon  23953  elflim  23954  hausflim  23964  flimcls  23968  flfnei  23974  isflf  23976  hausflf  23980  cnpflf  23984  cnflf  23985  txflf  23989  isfcls  23992  fclstopon  23995  isfcls2  23996  fclssscls  24001  fclsnei  24002  fclsfnflim  24010  flimfnfcls  24011  isfcf  24017  fcfelbas  24019  cnpfcf  24024  cnfcf  24025  flfcntr  24026  alexsublem  24027  alexsubALTlem3  24032  cnextfun  24047  cnextfvval  24048  cnextf  24049  cnextcn  24050  tmdgsum2  24079  tgpconncomp  24096  ghmcnp  24098  qustgplem  24104  eltsms  24116  haustsms  24119  tsmsgsum  24122  tsmssubm  24126  tsmssplit  24135  isust  24187  ustbas  24210  elutop  24216  ustuqtoplem  24222  ustuqtop4  24227  ustuqtop  24229  utopsnneiplem  24230  utopsnneip  24231  utopsnnei  24232  isusp  24244  isucn  24260  ucncn  24267  iscfilu  24270  neipcfilu  24278  iscusp  24281  cnextucn  24285  ispsmet  24287  ismet  24306  isxmet  24307  elblps  24370  elbl  24371  elmopn  24425  prdsbl  24474  neibl  24484  met1stc  24504  metrest  24507  prdsxmslem2  24512  txmetcnp  24530  txmetcn  24531  metustsym  24538  cfilucfil2  24544  elbl4  24546  metuel  24547  psmetutop  24550  restmetu  24553  metucn  24554  tngngp  24637  isnmhm  24729  zcld  24797  metnrmlem1a  24842  elcncf  24874  cncfcnvcn  24910  cnheibor  24940  lebnumlem1  24946  ishtpy  24957  isphtpy  24966  om1elbas  25017  elpi1  25030  pi1xfr  25040  pi1coghm  25046  tcphcph  25222  lmmbrf  25247  iscfil  25250  iscau  25261  iscauf  25265  caucfil  25268  iscmet  25269  cmetcaulem  25273  iscmet3lem1  25276  iscmet3lem2  25277  iscmet3  25278  bcthlem1  25309  cmsss  25336  cmetcusp1  25338  cmetcusp  25339  cmscsscms  25358  rrxcph  25377  minveclem3b  25413  ovolfioo  25452  ovolficc  25453  ovolctb  25475  ovoliunnul  25492  ovolshftlem1  25494  sca2rab  25497  ovolscalem1  25498  ovolicc2lem1  25502  ovolicc2lem2  25503  ovolicc2lem4  25505  ovolicc2lem5  25506  iundisj  25533  iunmbl2  25542  uniioombllem3  25570  vitalilem2  25594  vitalilem3  25595  mbfss  25631  i1faddlem  25678  i1fmullem  25679  mbfi1fseqlem2  25701  mbfi1fseqlem4  25703  mbfi1fseq  25706  itg2splitlem  25733  itg2split  25734  itg2monolem1  25735  itg2gt0  25745  isibl  25750  iblss2  25791  itgss3  25800  itgsplit  25821  ellimc  25858  limcmo  25867  cnlimc  25873  limciun  25879  limcun  25880  eldv  25883  dvbsss  25887  dvreslem  25894  elcpn  25919  dvaddf  25927  dvmulf  25928  dvcof  25933  rolle  25975  dvlip2  25980  dvivthlem1  25993  lhop1  25999  lhop2  26000  ftc1cn  26028  fta1glem2  26152  plyco0  26175  elply  26178  ply1termlem  26186  eltayl  26343  tayl0  26345  taylplem1  26346  taylplem2  26347  dvtaylp  26353  taylthlem1  26356  taylthlem2  26357  abelth  26424  cxpcn3  26730  rlimcnp  26947  fsumharmonic  26993  dchrelbas  27217  pntrsumbnd2  27548  ostth2lem2  27615  nolesgn2ores  27654  nogesgn1ores  27656  nosupprefixmo  27682  noinfprefixmo  27683  nosupcbv  27684  nosupdm  27686  nosupfv  27688  nosupres  27689  nosupbnd1lem1  27690  nosupbnd1lem3  27692  nosupbnd1lem5  27694  nosupbnd2lem1  27697  noinfcbv  27699  noinfdm  27701  noinffv  27703  noinfres  27704  noinfbnd1lem1  27705  noinfbnd1lem3  27707  noinfbnd1lem5  27709  noinfbnd2lem1  27712  elmade  27867  elold  27869  sltsleft  27870  sltsright  27871  oldlim  27897  madebday  27910  newbday  27912  ltslpss  27918  bdayiun  27925  cofcutr  27934  cofcutrtime  27937  lrrecval  27949  lrrecval2  27950  addsval  27972  precsexlem9  28225  precsexlem11  28227  ltonold  28271  onnolt  28276  onlts  28277  noseqrdgfn  28316  istrkgb  28541  istrkgcb  28542  istrkge  28543  istrkgl  28544  istrkgld  28545  axtgsegcon  28550  axtg5seg  28551  axtgbtwnid  28552  axtgpasch  28553  axtgupdim2  28557  axtgeucl  28558  tgdim01  28593  iscgrg  28598  isismt  28620  tglnunirn  28634  tglngval  28637  tgellng  28639  legval  28670  legov  28671  legov2  28672  ishlg  28688  mirreu3  28740  mirval  28741  mirfv  28742  mircgr  28743  mirbtwn  28744  ismir  28745  mireq  28751  symquadlem  28775  israg  28783  perpln1  28796  perpln2  28797  isperp  28798  islnopp  28825  outpasch  28841  ishpg  28845  iscgra  28895  dfcgra2  28916  isinag  28924  isleag  28933  iseqlg  28953  f1otrgitv  28956  f1otrg  28957  f1otrge  28958  ttgval  28961  ttgelitv  28969  elee  28980  brbtwn  28986  brcgr  28987  axlowdimlem16  29044  ebtwntg  29069  elntg2  29072  upgrex  29179  edgupgr  29221  upgredg  29224  edglnl  29230  numedglnl  29231  uhgr2edg  29295  umgr2edg1  29298  usgredg2vlem1  29312  usgredg2vlem2  29313  ushgredgedg  29316  ushgredgedgloop  29318  uhgrspansubgrlem  29377  fusgrfisstep  29416  nbgrval  29423  nbgrel  29427  nbupgrel  29432  nbgr2vtx1edg  29437  nbuhgr2vtx1edgblem  29438  nbuhgr2vtx1edgb  29439  nbusgreledg  29440  usgrnbcnvfv  29452  uvtxval  29474  uvtxel  29475  uvtx01vtx  29484  uvtxusgrel  29490  nbcplgr  29521  cplgr3v  29522  cusgrexi  29530  structtocusgr  29533  vtxdgfval  29554  vtxdg0v  29560  vtxdeqd  29564  vtxdun  29568  1loopgrnb0  29589  1loopgrvd0  29591  1hevtxdg0  29592  1hevtxdg1  29593  1egrvtxdg1  29596  umgr2v2evtxel  29609  umgr2v2enb1  29613  umgr2v2evd2  29614  vtxdginducedm1lem4  29629  vtxdginducedm1  29630  finsumvtxdg2sstep  29636  ewlksfval  29688  isewlk  29689  wksfval  29696  iswlk  29697  uspgr2wlkeq  29732  wlkres  29755  dfpth2  29815  usgr2pthlem  29849  clwlkcompim  29866  uspgrn2crct  29894  wwlks  29921  iswwlksn  29924  wwlknvtx  29931  wlkiswwlks2  29961  wwlksm1edg  29967  wwlksnred  29978  wwlksnext  29979  wwlksnredwwlkn  29981  wwlksnredwwlkn0  29982  wwlksnwwlksnon  30001  wspn0  30010  usgr2wspthons3  30053  rusgrnumwwlkb0  30060  clwwlk  30071  clwwlkccatlem  30077  clwlkclwwlklem2a4  30085  clwlkclwwlk  30090  clwwisshclwwslem  30102  clwwlkinwwlk  30128  clwwlkel  30134  clwwlkf  30135  clwwlkext2edg  30144  wwlksext2clwwlk  30145  wwlksubclwwlk  30146  clwwnisshclwwsn  30147  eleclclwwlknlem2  30149  erclwwlknsym  30158  erclwwlkntr  30159  umgrhashecclwwlk  30166  clwwlkvbij  30201  eupth2lem3lem3  30318  eupth2lem3lem4  30319  eupth2lem3lem6  30321  eupth2lemb  30325  eucrct2eupth  30333  fusgreg2wsplem  30421  2clwwlklem  30431  2clwwlk2clwwlklem  30434  2clwwlkel  30437  2clwwlk2clwwlk  30438  extwwlkfabel  30441  clwwlknonclwlknonf1o  30450  dlwwlknondlwlknonf1olem1  30452  numclwwlk2lem1  30464  numclwlk2lem2f  30465  numclwlk2lem2f1o  30467  ex-res  30529  isssp  30813  sspn  30825  islno  30842  isblo  30871  nmlno0  30884  ishmo  30900  dipdir  30931  dipass  30934  ubthlem1  30959  ubthlem2  30960  htthlem  31006  htth  31007  ocel  31370  ocnel  31387  shsel  31403  shsel2  31411  shmodsi  31478  pjhtheu  31483  pjeq  31488  axpjpj  31509  pjoc2  31528  elspani  31632  h1de2ctlem  31644  elspansn  31655  elspansn2  31656  elnlfn  32017  eleigvec  32046  riesz3i  32151  cbviunf  32644  iuneq12daf  32645  iunrdx  32652  iunrnmptss  32654  cbvdisjf  32660  disjorf  32668  disjabrex  32671  disjabrexf  32672  iundisjf  32678  disjrdx  32680  brab2d  32697  fresunsn  32717  2ndresdju  32741  abfmpunirn  32744  abfmpeld  32746  abfmpel  32747  fmptcof2  32749  acunirnmpt2  32752  acunirnmpt2f  32753  aciunf1lem  32754  suppss3  32815  fpwrelmap  32825  xrofsup  32859  iundisjfi  32888  eliccioo  33009  s3f1  33026  ccatf1  33028  ccatws1f1o  33030  swrdrn3  33034  ismnt  33062  mgcoval  33065  gsummpt2co  33129  gsumpart  33144  gsumhashmul  33148  gsummulsubdishift1  33149  xrge0tsmsbi  33155  gsumwrd2dccatlem  33158  gsumwrd2dccat  33159  cycpmco2  33214  cyc3co2  33221  isfxp  33249  cntrval2  33252  inftmrel  33261  isinftm  33262  isslmd  33283  urpropd  33312  elrgspn  33327  erlval  33339  rlocval  33340  rloccring  33351  rloc1r  33353  domnprodeq0  33357  domnpropd  33358  isdrng4  33379  fracfld  33392  resv1r  33422  ellspds  33451  ellpi  33456  lbslsp  33460  rhmimaidl  33515  isprmidl  33521  qsidomlem1  33535  qsidomlem2  33536  ismxidl  33545  crngmxidl  33552  drng0mxidl  33559  opprqus0g  33573  qsfld  33581  isrprm  33600  rsprprmprmidlb  33606  ressply1evls1  33648  ply1mulrtss  33665  ply1coedeg  33672  psrmonmul  33734  dimpropd  33793  lbslsat  33800  extdg1id  33850  fldextrspunlsplem  33857  fldextrspunlsp  33858  elirng  33870  ply1annidllem  33885  constrsuc  33922  constrconj  33929  constrllcllem  33936  constrlccllem  33937  constrcccllem  33938  nn0constr  33945  smatrcl  33980  smatcl  33986  ist0cld  34017  txomap  34018  locfinreflem  34024  zarclsiin  34055  zart0  34063  rhmpreimacnlem  34068  metidval  34074  cnre2csqima  34095  ordtrest2NEW  34107  fmcncfil  34115  fsumcvg4  34134  ofcfval  34282  measvuni  34398  meascnbl  34403  faeval  34430  ismbfm  34435  elunirnmbfm  34436  imambfm  34446  elcarsg  34489  itgeq12dv  34510  issibf  34517  eulerpartlems  34544  eulerpartlemgc  34546  eulerpartlemgvv  34560  eulerpartlemgu  34561  eulerpart  34566  rrvmbfm  34626  elorvc  34644  elorrvc  34648  dstfrvunirn  34659  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemsima  34700  ballotlemrv  34704  fzssfzo  34723  signstfvn  34753  signstfvneq0  34756  signstres  34759  repr0  34795  reprinrn  34802  reprdifc  34811  hgt750lemg  34838  hgt750lemb  34840  istrkg2d  34850  axtgupdim2ALTV  34852  afsval  34855  brafs  34856  bnj945  34956  bnj1400  35017  bnj18eq1  35109  bnj916  35115  bnj1014  35143  bnj1015  35144  bnj1110  35164  bnj1417  35223  rankval2b  35280  r1filimi  35284  r1ssel  35288  onvf1odlem3  35333  vonf1owev  35336  revpfxsfxrev  35344  cplgredgex  35349  pfxwlk  35352  revwlk  35353  subfacp1lem2b  35409  subfacp1lem4  35411  subfacp1lem5  35412  subfacp1lem6  35413  ptpconn  35461  cvmscbv  35486  iscvm  35487  cvmsi  35493  cvmsval  35494  cvmliftmolem1  35509  cvmlift2lem12  35542  cvmlift2lem13  35543  cvmlift3lem7  35553  snmlval  35559  satfv1  35591  satfvsucsuc  35593  satfrnmapom  35598  satf0op  35605  satf0n0  35606  sat1el2xp  35607  fmlafvel  35613  isfmlasuc  35616  fmlaomn0  35618  gonan0  35620  goaln0  35621  gonar  35623  goalr  35625  satffunlem1lem2  35631  satffunlem2lem2  35634  satfv0fvfmla0  35641  satef  35644  satefvfmla0  35646  sategoelfvb  35647  satfv1fvfmla1  35651  mrsubfval  35736  mrsubvrs  35750  mclsrcl  35789  mclsval  35791  mppsval  35800  mclsppslem  35811  opelco3  36003  wsuclem  36051  funtransport  36259  fvtransport  36260  brcolinear  36287  colineardim1  36289  funray  36368  fvray  36369  funline  36370  fvline  36372  lineelsb2  36376  fwddifval  36390  fwddifnval  36391  rankelg  36396  rankeq1o  36399  elhf2  36403  0hf  36405  rmoeqbidv  36441  disjeq12dv  36443  ixpeq12dv  36444  prodeq12sdv  36446  itgeq12sdv  36447  cbvralvw2  36454  cbvrexvw2  36455  cbvrmovw2  36456  cbvreuvw2  36457  cbvcsbvw2  36459  cbviunvw2  36460  cbviinvw2  36461  cbvmptvw2  36462  cbvdisjvw2  36463  cbvmpo1vw2  36471  cbvmpo2vw2  36472  cbvsbcdavw  36485  cbvcsbdavw  36487  cbvcsbdavw2  36488  cbviundavw  36490  cbviindavw  36491  cbvdisjdavw  36496  cbvrabdavw2  36513  cbviundavw2  36514  cbviindavw2  36515  cbvmptdavw2  36516  cbvdisjdavw2  36517  cbvriotadavw2  36518  cbvmpo1davw2  36520  cbvmpo2davw2  36521  cbvsumdavw2  36523  neibastop2lem  36588  neibastop3  36590  eltail  36602  ttctr  36721  dfttc2g  36734  mh-infprim2bi  36775  bj-projeq  37345  bj-projval  37349  bj-restsn  37440  opelopabbv  37503  brabd0  37507  bj-eldiag  37536  bj-eldiag2  37537  mptsnunlem  37700  dissneqlem  37702  iooelexlt  37724  relowlssretop  37725  rdgellim  37738  exrecfnlem  37741  finxpeq1  37748  finxpreclem6  37758  pibp21  37777  curf  37965  uncf  37966  curunc  37969  unccur  37970  fin2so  37974  lindsadd  37980  lindsdom  37981  lindsenlbs  37982  matunitlindflem1  37983  matunitlindflem2  37984  matunitlindf  37985  ptrest  37986  ptrecube  37987  poimirlem2  37989  poimirlem8  37995  poimirlem17  38004  poimirlem18  38005  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  poimirlem24  38011  poimirlem26  38013  poimirlem29  38016  heicant  38022  mblfinlem1  38024  mblfinlem2  38025  volsupnfl  38032  itg2addnclem  38038  itg2gt0cn  38042  indexdom  38101  incsequz  38115  istotbnd  38136  istotbnd3  38138  0totbnd  38140  sstotbnd  38142  sstotbnd3  38143  isbnd  38147  prdstotbnd  38161  cntotbnd  38163  isismty  38168  heibor1lem  38176  heiborlem2  38179  heiborlem3  38180  heibor  38188  isass  38213  exidcl  38243  exidreslem  38244  elghomlem2OLD  38253  rngoidmlem  38303  rngo1cl  38306  divrngcl  38324  isdrngo2  38325  isrngohom  38332  isrngoiso  38345  isriscg  38351  iscom2  38362  iscringd  38365  isidl  38381  ispridl  38401  ismaxidl  38407  ac6s6  38539  dmecd  38677  dfpre4  38847  releldmqs  39110  releldmqscoss  39112  erimeq2  39130  qmapeldisjsim  39227  eldisjlem19  39280  membpartlem19  39281  prter3  39374  islshp  39471  islsat  39483  lcvfbr  39512  islfl  39552  ellkr  39581  islshpkrN  39612  ldual1dim  39658  isopos  39672  cmtfvalN  39702  cvrfval  39760  isat  39778  islln  39998  islpln  40022  islvol  40065  isline  40231  ispointN  40234  ispsubsp  40237  elpmap  40250  elpmapat  40256  elpadd  40291  paddclN  40334  elpclN  40384  elpcliN  40385  pclfinN  40392  pclcmpatN  40393  ispsubclN  40429  iswatN  40486  islhp  40488  islaut  40575  ispautN  40591  isldil  40602  isltrn  40611  isdilN  40646  istrnN  40649  istendo  41252  dvhb1dimN  41478  erng1lem  41479  erngdvlem4-rN  41491  diaelval  41525  diaeldm  41528  dia1dimid  41555  cdlemm10N  41610  dibopelvalN  41635  dibopelval2  41637  dibelval3  41639  dibelval1st  41641  dibelval2nd  41644  dibeldmN  41650  dibvalrel  41655  dibglbN  41658  dicffval  41666  dicfval  41667  dicopelval  41669  dicelvalN  41670  dicelval3  41672  dicvalrelN  41677  dicelval1sta  41679  diclspsn  41686  dihopelvalbN  41730  dihopelvalcqat  41738  dihopelvalcpre  41740  dihvalrel  41771  dih1  41778  dihmeetlem4preN  41798  dihmeetlem13N  41811  dih1dimatlem  41821  dochnel2  41884  dihjatcclem4  41913  dvh2dim  41937  dvh3dim  41938  dvh4dimN  41939  dochfln0  41969  lpolsetN  41974  islpolN  41975  lcfrvalsnN  42033  lcfrlem21  42055  lcfrlem27  42061  lcfrlem37  42071  lcfr  42077  lcdlss  42111  mapdcv  42152  hdmap1fval  42288  hdmapffval  42318  hdmapfval  42319  hdmapval  42320  hgmapffval  42377  hgmapfval  42378  hdmapellkr  42406  hlhilhillem  42452  fzsplitnd  42467  isprimroot  42578  primrootsunit1  42582  primrootscoprmpow  42584  primrootscoprbij  42587  aks6d1c1p2  42594  aks6d1c1p3  42595  aks6d1c1p4  42596  aks6d1c1p5  42597  aks6d1c1p6  42599  aks6d1c1  42601  evl1gprodd  42602  sticksstones11  42641  sticksstones12a  42642  rhmqusspan  42670  grpods  42679  fzosumm1  42734  frlmfielbas  42990  frlmsnic  43026  psrmnd  43029  isnacs  43153  mrefg2  43156  elmzpcl  43175  mzpcompact2  43201  eldiophb  43206  elpell1qr  43292  elpell14qr  43294  elpell1234qr  43296  pw2f1ocnv  43482  pw2f1o2val2  43485  aomclem4  43502  aomclem6  43504  islssfg2  43516  imasgim  43545  lnr2i  43561  elmnc  43581  rngunsnply  43614  onexomgt  43686  onexlimgt  43688  onexoegt  43689  oaordnr  43741  omnord1  43750  oenord1  43761  cantnfresb  43769  tfsconcatun  43782  tfsconcat0i  43790  ofoaf  43800  naddcnff  43807  naddcnffo  43809  naddcnfcom  43811  naddcnfid1  43812  naddcnfid2  43813  naddcnfass  43814  naddwordnexlem4  43846  fiinfi  44017  sqrtcvallem1  44075  elintima  44097  eliunov2  44123  ov2ssiunov2  44144  brtrclfv2  44171  rfovcnvf1od  44448  rfovcnvfvd  44451  fsovrfovd  44453  fsovfvd  44454  fsovcnvlem  44457  ntrclsfv1  44499  ntrclselnel1  44501  ntrclsneine0lem  44508  ntrneifv1  44523  ntrneifv2  44524  ntrneiel  44525  gneispace2  44576  gneispacess2  44590  extoimad  44608  mnringelbased  44661  dvconstbi  44778  bccbc  44789  wfac8prim  45446  permaxrep  45450  permac8prim  45458  eliin2f  45551  iineq12dv  45553  rabbida2  45579  disjinfi  45639  unirnmap  45653  elmptima  45702  iuneqfzuzlem  45779  iooiinioc  46001  fsumiunss  46020  fsumsupp0  46023  lptre2pt  46083  icccncfext  46330  cncfiooicclem1  46336  dvnprodlem2  46390  stoweidlem27  46470  stoweidlem29  46472  stoweidlem31  46474  stoweidlem34  46477  stoweidlem48  46491  stoweidlem59  46502  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem2  46552  fourierdlem3  46553  fourierdlem25  46575  fourierdlem32  46582  fourierdlem33  46583  fourierdlem41  46591  fourierdlem48  46597  fourierdlem49  46598  fourierdlem62  46611  fourierdlem70  46619  fourierdlem80  46629  fourierdlem92  46641  fourierdlem93  46642  fourierdlem101  46650  etransclem37  46714  sge0val  46809  sge0f1o  46825  sge0iunmptlemre  46858  sge0iunmpt  46861  iundjiun  46903  caragenel  46938  ovncvrrp  47007  ovnsubaddlem1  47013  ovnsubadd  47015  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  hoidmvle  47043  ovncvr2  47054  hspdifhsp  47059  hoiqssbl  47068  hspmbllem2  47070  hspmbl  47072  opnvonmbllem1  47075  isvonmbl  47081  ovnovollem1  47099  issmflem  47170  smflimlem3  47216  smflimlem4  47217  smflim  47220  smfmullem2  47235  smflimmpt  47253  smfsuplem1  47254  smflimsuplem1  47263  smflimsuplem3  47265  smflimsuplem4  47266  smflimsuplem7  47269  smflimsup  47271  chnsubseq  47325  fcores  47530  fcoresf1  47532  afvelrnb  47626  afvelrnb0  47627  afv2co2  47720  el1fzopredsuc  47789  muldvdsfacm1  47850  iccpart  47891  iccpartgtprec  47895  iccpartiltu  47897  iccpartigtl  47898  iccpartltu  47900  iccpartgtl  47901  iccpartgt  47902  iccpartleu  47903  iccpartgel  47904  iccelpart  47908  iccpartiun  47909  icceuelpart  47911  fargshiftfv  47914  fargshiftfo  47917  sprel  47959  prprelb  47991  prprelprb  47992  nprmdvdsfacm1lem4  48101  fpprel  48219  sbgoldbo  48278  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem3  48298  bgoldbtbnd  48300  clnbgrval  48313  elclnbgrelnbgr  48316  clnbgrel  48319  clnbupgrel  48325  vopnbgrel  48345  isubgredg  48357  upgrimwlklem3  48390  upgrimwlklem5  48392  upgrimpths  48400  grtriprop  48432  isgrtri  48434  grtriclwlk3  48436  stgredgel  48448  gpgvtxel  48538  gpgiedgdmel  48540  gpgedgel  48541  opgpgvtx  48546  gpg5nbgrvtx13starlem1  48562  gpg5nbgrvtx13starlem2  48563  gpg5nbgrvtx13starlem3  48564  gpg3kgrtriex  48580  grlimedgnedg  48622  upwlksfval  48626  isupwlk  48627  intop  48694  isclintop  48698  assintop  48700  isassintop  48701  assintopcllaw  48703  uzlidlring  48726  elrngchomALTV  48760  rngccatidALTV  48763  rngcsectALTV  48766  rngcisoALTV  48768  rhmsubcALTVlem3  48774  rhmsubcALTVlem4  48775  funcringcsetcALTV2lem7  48787  funcringcsetcALTV2lem9  48789  elringchomALTV  48794  ringccatidALTV  48797  ringcsectALTV  48800  ringcisoALTV  48802  ringcbasbasALTV  48803  funcringcsetclem7ALTV  48810  funcringcsetclem9ALTV  48812  srhmsubcALTV  48816  cbvmpox2  48827  ply1sclrmsm  48875  dmatALTbasel  48893  lcoval  48903  lindslinindsimp1  48948  lindslinindsimp2  48954  lmod1  48983  elbigo  49042  elbigo2  49043  elbigolo1  49048  dig2nn0ld  49095  naryfvalel  49121  rrxlines  49224  rrxlinesc  49226  rrxlinec  49227  eenglngeehlnm  49230  elrrx2linest2  49236  rrxsphere  49239  itsclc0  49262  itsclc0b  49263  itsclinecirc0  49264  itsclinecirc0b  49265  itscnhlinecirc02p  49276  brab2dd  49318  f1omo  49383  f1omoOLD  49384  lubeldm2d  49448  glbeldm2d  49449  catprs  49501  sectpropdlem  49526  nelsubc3lem  49560  initc  49581  imaid  49644  upfval  49666  upfval2  49667  upfval3  49668  uppropd  49671  oppcinito  49725  oppctermo  49726  oppczeroo  49727  initopropd  49733  termopropd  49734  isthinc  49909  isthincd2lem1  49915  thincmoALT  49919  thincmod  49920  isthincd  49926  thincpropd  49932  indcthing  49950  discthing  49951  prsthinc  49954  termcterm  50003  termc2  50008  isinito4  50037  2arwcatlem1  50085  setc1onsubc  50092  cnelsubclem  50093  ranval3  50121  lmdfval2  50145  cmdfval2  50146  termolmd  50160  elsetrecslem  50189