Theorem eleq1d 2813

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) Allow shortening of eleq1 2816. (Revised by Wolf Lammen, 20-Nov-2019.)

Hypothesis

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

Assertion

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

Proof of Theorem eleq1d

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1d.1	. . . . 5 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqeq2d 2740	. . . 4 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
3	2	anbi1d 631	. . 3 ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
4	3	exbidv 1921	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
5		dfclel 2804	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶))
6		dfclel 2804	. 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = 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:  eleq1  2816  eleq12d  2822  eqeltrd  2828  eqneltrd  2848  rspcimdv  3569  reuind  3715  sbcel2  4371  sbccsb2  4390  disjiun  5083  breq1  5098  breq2  5099  axrep6g  5232  inex1g  5261  intex  5286  pwexg  5320  reusv2lem4  5343  reusv2  5345  reusv3  5347  rabxfrd  5359  prex  5379  opelopabsb  5477  csbmpt12  5504  pofun  5549  seex  5582  seinxp  5707  opabid2  5775  opeliunxp2  5785  elrn2g  5837  opeldmd  5853  opeldm  5854  elreldm  5881  elsnres  5976  iss  5990  unielrel  6226  onunel  6418  funopg  6520  brprcneu  6816  brprcneuALT  6817  tz6.12f  6851  ndmfvrcl  6860  ssimaex  6912  dmfco  6923  fvmpti  6933  fvmpt3  6938  fvmptf  6955  fvmptss2  6960  respreima  7004  fvn0ssdmfun  7012  fvelrn  7014  ffnfvf  7058  ffvresb  7063  fmptco  7067  fmptcof  7068  fsn  7073  fsn2g  7076  fressnfv  7098  fvrnressn  7099  fvn0fvelrnOLD  7101  fnex  7157  funfvima  7170  funfvima3  7176  f1mpt  7202  fliftfuns  7255  isoselem  7282  isowe2  7291  riotaclb  7351  ovrspc2v  7379  ffnov  7479  fovcld  7480  ovmpos  7501  ov2gf  7502  ovg  7518  funimassov  7530  oprssdm  7534  ndmovrcl  7539  caovclg  7545  elovmpo  7598  ofmpteq  7640  sorpsscmpl  7674  uniexg  7680  unexbOLD  7688  abnexg  7696  difsnexi  7701  onint  7730  limsuc  7789  tfisi  7799  peano5  7833  xpexr  7858  xpexcnv  7860  fnexALT  7893  focdmex  7898  f1stres  7955  f2ndres  7956  xp1st  7963  xp2nd  7964  unielxp  7969  opiota  8001  fmpox  8009  offval22  8028  frxp  8066  fnse  8073  frxp2  8084  sexp2  8086  frxp3  8091  sexp3  8093  opeliunxp2f  8150  dftpos4  8185  fvmpocurryd  8211  undefnel2  8217  onnseq  8274  smoel  8290  smo11  8294  tfrlem8  8313  tfrlem9  8314  tfrlem15  8321  tfr2b  8325  tz7.44-2  8336  tz7.44-3  8337  oacl  8460  omcl  8461  oecl  8462  oaord1  8476  omordi  8491  oen0  8511  oeeui  8527  nnacl  8536  nnmcl  8537  nnecl  8538  nnmordi  8556  nnaordex  8563  omsmolem  8582  naddcllem  8601  naddov2  8604  naddf  8606  naddssim  8610  naddelim  8611  naddasslem1  8619  naddasslem2  8620  naddsuc2  8626  erexb  8657  elecex  8682  qliftfuns  8738  ixpsnval  8834  elixp2  8835  resixp  8867  undifixp  8868  mptelixpg  8869  resixpfo  8870  elixpsn  8871  fundmen  8963  fopwdom  9009  disjen  9058  xpf1o  9063  unfi  9095  cnvfi  9100  fnfi  9102  f1oenfirn  9104  f1domfi  9105  unblem2  9198  imafiOLD  9223  pwfi  9226  xpfiOLD  9228  fiint  9235  fiintOLD  9236  iunfi  9252  isfsupp  9274  fsuppun  9296  ffsuppbi  9307  elfi2  9323  wdom2d  9491  ixpiunwdom  9501  dfom3  9562  cantnfvalf  9580  cantnflt  9587  cantnflem1  9604  r1fin  9688  tz9.12lem3  9704  ranksnb  9742  ranklim  9759  r1pw  9760  r1pwALT  9761  r1pwcl  9762  rankuni2b  9768  djuexb  9824  cardmin2  9914  infxpenc2lem1  9932  dfac8alem  9942  dfac8clem  9945  ac5num  9949  acni2  9959  acnlem  9961  alephon  9982  alephfplem3  10019  alephfplem4  10020  dfac4  10035  dfac5lem1  10036  dfac5lem5  10040  dfac2a  10043  dfac2b  10044  dfacacn  10055  dfac12lem2  10058  dfac12r  10060  dfac12k  10061  cofsmo  10182  cfsmolem  10183  isfin1a  10205  fin1ai  10206  isfin3  10209  infpssrlem3  10218  fin23lem7  10229  fin23lem11  10230  enfin2i  10234  isf34lem4  10290  fin1a2lem7  10319  hsmexlem9  10338  hsmexlem4  10342  hsmex  10345  axcc2lem  10349  axcc3  10351  axdc3lem2  10364  axcclem  10370  zornn0g  10418  ttukeylem3  10424  ttukeylem6  10427  ttukey2g  10429  brdom7disj  10444  brdom6disj  10445  fnct  10450  konigthlem  10481  axregndlem2  10516  axinfnd  10519  axacndlem5  10524  axacnd  10525  fpwwe2lem4  10547  fpwwe2lem12  10555  fpwwe  10559  pwfseqlem1  10571  pwfseqlem3  10573  pwfseqlem4a  10574  pwfseqlem4  10575  wununi  10619  wunpw  10620  wunpr  10622  wunr1om  10632  tskpw  10666  tskr1om  10680  inar1  10688  grupw  10708  grupr  10710  gruurn  10711  gruiun  10712  ingru  10728  grur1a  10732  grothomex  10742  grothac  10743  addnidpi  10814  indpi  10820  adderpq  10869  mulerpq  10870  addclprlem2  10930  mulclprlem  10932  distrlem4pr  10939  prlem934  10946  ltexprlem3  10951  ltexprlem4  10952  ltexprlem7  10955  ltexpri  10956  prlem936  10960  reclem2pr  10961  reclem3pr  10962  addclsr  10996  mulclsr  10997  supsrlem  11024  supsr  11025  axaddf  11058  axmulf  11059  axaddrcl  11065  axmulrcl  11067  renegcl  11445  negreb  11447  negn0  11567  negf1o  11568  ltord1  11664  leord1  11665  eqord1  11666  ltord2  11667  leord2  11668  eqord2  11669  negfi  12092  infm3  12102  cju  12142  peano5nni  12149  peano2nn  12158  dfnn2  12159  nn1m1nn  12167  nnaddcl  12169  nnmulcl  12170  nnsub  12190  nndivtr  12193  un0addcl  12435  un0mulcl  12436  elnnnn0  12445  nn0sub  12452  fcdmnn0fsuppg  12462  elz  12491  nnnegz  12492  elz2  12507  znegclb  12530  zaddcl  12533  nzadd  12541  zmulcl  12542  zneo  12577  nneo  12578  zeo  12580  peano5uzi  12583  zindd  12595  eluzsubOLD  12789  uzp1  12794  uzaddcl  12823  ublbneg  12852  eqreznegel  12853  supminf  12854  zsupss  12856  qmulz  12870  qnegcl  12885  irradd  12892  irrmul  12893  xnn0xaddcl  13155  fzrev2  13509  injresinjlem  13708  negmod0  13800  om2uzuzi  13874  uzindi  13907  fsuppmapnn0ub  13920  mptnn0fsuppr  13924  seqexw  13942  seqcl2  13945  seqcl  13947  seqf  13948  monoord  13957  monoord2  13958  sermono  13959  seqsplit  13960  seqcaopr2  13963  seqid3  13971  seqhomo  13974  expcllem  13997  expcl2lem  13998  m1expcl2  14010  faccl  14208  facdiv  14212  facndiv  14213  bccmpl  14234  bccl  14247  hashclb  14283  hasheq0  14288  hashfn  14300  seqcoll  14389  opfi1uzind  14436  ccatalpha  14518  reuccatpfxs1lem  14670  reuccatpfxs1  14671  repswccat  14710  repswrevw  14711  2cshw  14737  2cshwcshw  14750  cshimadifsn  14754  cshco  14761  swrd2lsw  14877  wwlktovf  14881  wwlktovf1  14882  wwlktovfo  14883  wrd2f1tovbij  14885  shftlem  14993  shftf  15004  cjval  15027  cjth  15028  remim  15042  cnpart  15165  uzin2  15270  caubnd2  15283  sqreulem  15285  clim  15419  clim2  15429  lo1o12  15458  climrlim2  15472  lo1resb  15489  o1resb  15491  lo1eq  15493  climmpt2  15498  climshftlem  15499  rlimcld2  15503  climcn1  15517  climcn2  15518  o1dif  15555  iserex  15582  climub  15587  climserle  15588  isercoll  15593  climcau  15596  caurcvg2  15603  caucvgb  15605  summolem3  15639  summolem2a  15640  zsum  15643  fsum  15645  sumss2  15651  fsumcvg2  15652  fsumclf  15663  fsumsplitf  15667  fsumsplit1  15670  sumpr  15673  sumtp  15674  fsumm1  15676  fsum1p  15678  isummulc2  15687  fsum2dlem  15695  fsumcom2  15699  fsumshftm  15706  fsum0diag2  15708  fsumge1  15722  fsum00  15723  fsumabs  15726  telfsumo  15727  telfsumo2  15728  fsumparts  15731  fsumrlim  15736  fsumo1  15737  o1fsum  15738  fsumiun  15746  binomlem  15754  isumshft  15764  isum1p  15766  isumrpcl  15768  climcndslem1  15774  climcndslem2  15775  climcnds  15776  infcvgaux2i  15783  cvgrat  15808  mertens  15811  clim2prod  15813  prodfn0  15819  prodfrec  15820  prodfdiv  15821  ntrivcvgfvn0  15824  prodmolem3  15858  prodmolem2a  15859  zprod  15862  fprod  15866  prodss  15872  fprodser  15874  fprodm1  15892  fprod1p  15893  fprodm1s  15895  fprodp1s  15896  fprodabs  15899  fprodn0  15904  fprod2dlem  15905  fprodcnv  15908  fprodcom2  15909  fproddivf  15912  fprodsplitf  15913  fprodsplit1f  15915  bpolycl  15977  fprodefsum  16020  rpnnen2lem11  16151  mod2eq1n2dvds  16276  mulsucdiv2z  16282  zob  16288  nn0o1gt2  16310  nno  16311  nn0o  16312  divalglem7  16328  bitsf1  16375  sadcp1  16384  smupp1  16409  qnumdencl  16668  iserodd  16765  pcqcl  16786  pcxnn0cl  16790  pcxcl  16791  pcgcd1  16807  dvdsprmpweqle  16816  pcmpt  16822  pcmpt2  16823  pcmptdvds  16824  infpnlem2  16841  infpn2  16843  1arith  16857  elgz  16861  mul4sq  16884  4sqlem13  16887  4sqlem17  16891  4sqlem18  16892  4sqlem19  16893  vdwlem1  16911  vdwlem2  16912  vdwnn  16928  ramtcl2  16941  ramcl  16959  prmonn2  16969  prmodvdslcmf  16977  isstruct2  17078  wunress  17178  firest  17354  imasaddfnlem  17450  imasvscafn  17459  xpsfrnel2  17486  mreintcl  17515  ismred2  17523  mreexexlemd  17568  mreexexlem3d  17570  mreexexlem4d  17571  iscatd2  17605  catpropd  17633  subsubc  17778  isfunc  17789  inclfusubc  17868  fncnvimaeqv  18044  joindef  18298  joinval  18299  meetdef  18312  meetval  18313  oduclatb  18431  acsdrsel  18467  isacs4lem  18468  isacs5lem  18469  acsdrscl  18470  mgmsscl  18537  mgmpropd  18543  mgm1  18550  gsumvalx  18568  issubmgm  18594  issubmgm2  18595  mgmhmima  18607  sgrppropd  18623  mndpropd  18651  issubm  18695  0subm  18709  insubm  18710  mhmimalem  18716  gsumwsubmcl  18729  gsumwspan  18738  symggrplem  18776  sursubmefmnd  18788  injsubmefmnd  18789  smndex1basss  18797  mulgsubcl  18985  issubg  19023  issubg2  19038  issubg4  19042  0subg  19048  0subgOLD  19049  isnsg  19052  isnsg2  19053  nsgbi  19054  isnsg3  19057  elnmz  19060  nmzbi  19061  nmzsubg  19062  eqgval  19074  eqgid  19077  cycsubgcl  19103  ghmrn  19126  ghmnsgima  19137  gass  19198  oppgsubg  19260  f1omvdconj  19343  symgfisg  19365  psgneldm  19400  0subgALT  19465  odhash3  19473  sylow2blem2  19518  lsmsubm  19550  lsmsubg  19551  efgsf  19626  efgsdm  19627  efgs1b  19633  efgredlema  19637  eqgabl  19731  ablnsg  19744  cyggenod2  19782  gsumzaddlem  19818  gsummhm2  19836  gsum2dlem2  19868  gsum2d2lem  19870  gsumcom2  19872  dprdfeq0  19921  dprdsubg  19923  dprd2da  19941  ablfacrp  19965  pgpfac1lem3  19976  pgpfaclem1  19980  ablfaclem3  19986  ablfac2  19988  cycsubggenodd  20008  isrng  20057  issrg  20091  srgfcl  20099  rglcom4d  20114  srgbinomlem4  20132  isring  20140  iscrng  20143  dvdsr  20265  irredrmul  20330  isrngim  20348  isrim0OLD  20384  isrim0  20386  issubrng  20450  subrngringnsg  20456  issubrng2  20461  rhmimasubrnglem  20468  issubrg  20474  issubrg2  20495  subrgpropd  20511  isdrngd  20668  isdrngdOLD  20670  issdrg  20691  sdrgacs  20704  issrngd  20758  islmod  20785  lmodlema  20786  islmodd  20787  lmodprop2d  20845  rmodislmodlem  20850  rmodislmod  20851  lssset  20854  islssd  20856  lsscl  20863  lsslss  20882  lsspropd  20939  lmhmima  20969  lbsind  21002  lsmcl  21005  islvec  21026  lmhmlvec  21032  lspsolvlem  21067  lspsolv  21068  lvecpropd  21092  rnglidlmcl  21141  rnglidl0  21154  rnglidlmmgm  21170  rngqiprngimf1lem  21219  rngqiprngimf1  21225  ring2idlqus  21234  xrsdsreclblem  21337  xrsdsreclb  21338  cnsubrglem  21341  prmirred  21399  pzriprnglem4  21409  pzriprnglem8  21413  pzriprngALT  21420  znunithash  21489  cofipsgn  21518  zrhpsgnelbas  21519  rzgrp  21548  isphl  21553  phllmhm  21557  ipcl  21558  isphld  21579  phlpropd  21580  phlssphl  21584  cssincl  21613  pjdm  21632  dsmmval  21659  dsmmbas2  21662  dsmmelbas  21664  frlmbas  21680  frlmup1  21723  lindfind  21741  lindsind  21742  f1lindf  21747  islindf4  21763  psrbag  21842  psrbaglefi  21851  mplsubglem  21924  mpllsslem  21925  ltbwe  21967  psrbagsn  21986  subrgasclcl  21990  mplind  21993  mpfind  22030  psdmul  22069  coe1mul2lem2  22170  gsumply1eq  22212  evl1vsd  22247  mpfpf1  22254  pf1mpf  22255  pf1ind  22258  matecl  22328  m1detdiag  22500  mdetralt  22511  mdetralt2  22512  mdetunilem2  22516  mdetunilem9  22523  m2detleiblem3  22532  m2detleiblem4  22533  smadiadetlem0  22564  cpmatacl  22619  chpscmat  22745  uniopn  22800  inopn  22802  fiinopn  22804  istps  22837  fctop  22907  iscld  22930  isopn2  22935  mretopd  22995  iscldtop  22998  perfi  23058  tgrest  23062  restcld  23075  ordtbaslem  23091  ordtrest2lem  23106  ordtrest2  23107  iscn  23138  cnpval  23139  iscnp  23140  tgcn  23155  subbascn  23157  ssidcn  23158  lmbrf  23163  cnpnei  23167  cnima  23168  iscncl  23172  cnconst2  23186  cnrest2  23189  cnpresti  23191  cnprest  23192  cnindis  23195  lmres  23203  lmcnp  23207  iscnrm  23226  t1sncld  23229  cnrmi  23263  cncmp  23295  cmpsublem  23302  fiuncmp  23307  unconn  23332  conncompid  23334  conncompconn  23335  conncompss  23336  1stcfb  23348  2ndcrest  23357  2ndcctbss  23358  2ndcdisj  23359  1stccnp  23365  islly  23371  isnlly  23372  subislly  23384  restnlly  23385  restlly  23386  islly2  23387  hausllycmp  23397  cldllycmp  23398  dislly  23400  isptfin  23419  islocfin  23420  ptfinfin  23422  finlocfin  23423  dissnlocfin  23432  locfindis  23433  comppfsc  23435  kgenval  23438  elkgen  23439  kgeni  23440  cmpkgen  23454  1stckgenlem  23456  kgencn2  23460  ptpjpre1  23474  elpt  23475  elptr  23476  ptbasin  23480  xkobval  23489  xkoval  23490  xkoopn  23492  txbasval  23509  tx1cn  23512  tx2cn  23513  dfac14  23521  xkoccn  23522  txcnp  23523  ptcnplem  23524  txcnmpt  23527  txindislem  23536  txdis1cn  23538  txlly  23539  txnlly  23540  pthaus  23541  ptrescn  23542  hauseqlcld  23549  txlm  23551  tx2ndc  23554  txkgen  23555  xkoptsub  23557  xkopt  23558  xkoco1cn  23560  xkoco2cn  23561  xkococnlem  23562  xkococn  23563  cnmpt11  23566  cnmpt12  23570  cnmpt21  23574  cnmpt22  23577  cnmptkp  23583  cnmptk1p  23588  xkoinjcn  23590  txconn  23592  qtopval2  23599  elqtop  23600  idqtop  23609  qtopcld  23616  qtopeu  23619  qtoprest  23620  qtopomap  23621  qtopcmap  23622  ishmeo  23662  hmeoopn  23669  hmeocld  23670  ordthmeolem  23704  ptcmpfi  23716  elmptrab  23730  fgcl  23781  trfil2  23790  cfinfil  23796  uzrest  23800  ufilss  23808  trufil  23813  cfinufil  23831  ufinffr  23832  ufildr  23834  rnelfm  23856  flfcntr  23946  ptcmplem2  23956  ptcmplem3  23957  ptcmplem4  23958  ptcmplem5  23959  cnextfvval  23968  tmdcn2  23992  tmdmulg  23995  tmdgsum2  23999  symgtgp  24009  opnsubg  24011  clssubg  24012  tgpconncompeqg  24015  ghmcnp  24018  tgphaus  24020  tgpt0  24022  qustgpopn  24023  qustgplem  24024  tsmsgsum  24042  tsmssubm  24046  tsmsres  24047  tsmsf1o  24048  tsmsxplem1  24056  tsmsxplem2  24057  tsmsxp  24058  istrg  24067  istdrg  24069  istdrg2  24081  istlm  24088  istvc  24095  ustval  24106  ustincl  24111  ustdiag  24112  ustinvel  24113  ustexhalf  24114  ust0  24123  ucnima  24184  fmucndlem  24194  prdsdsf  24271  prdsxmet  24273  imasf1oxmet  24279  imasf1omet  24280  prdsxmslem2  24433  metustsym  24459  isnlm  24579  qtopbaslem  24662  xrtgioo  24711  reperflem  24723  fsumcn  24777  expcn  24779  expcnOLD  24781  xrhmeo  24860  cnllycmp  24871  bndth  24873  isclm  24980  lmhmclm  25003  lmmcvg  25177  fmcfil  25188  iscfil3  25189  iscau2  25193  iscau4  25195  iscmet3lem1  25207  iscmet3  25209  cfilres  25212  caussi  25213  equivcfil  25215  flimcfil  25230  bcthlem1  25240  isbn  25254  srabn  25276  ishl2  25286  cmslssbn  25288  cmscsscms  25289  minveclem3b  25344  ivthlem1  25368  ivthlem2  25369  ivthlem3  25370  ivth2  25372  ivthle  25373  ivthle2  25374  ivthicc  25375  ovolficcss  25386  ovolunlem1a  25413  ovolunlem1  25414  ovolfiniun  25418  ovoliunlem1  25419  ovoliunlem3  25421  ovoliun  25422  ovoliun2  25423  shft2rab  25425  ovolshftlem1  25426  sca2rab  25429  ovolscalem1  25430  mblsplit  25449  finiunmbl  25461  volun  25462  volfiniun  25464  voliunlem1  25467  voliunlem3  25469  iunmbl  25470  voliun  25471  volsup  25473  ioombl  25482  ioorcl  25494  vitalilem1  25525  vitalilem2  25526  vitalilem3  25527  vitalilem4  25528  vitali  25530  ismbf1  25541  mbfdm  25543  ismbf  25545  ismbfcn  25546  mbfima  25547  mbfimaicc  25548  ismbfcn2  25555  ismbfd  25556  ismbf2d  25557  mbfeqalem1  25558  mbfmax  25566  mbfposr  25569  mbfposb  25570  ismbf3d  25571  mbfimaopnlem  25572  mbfimaopn2  25574  cncombf  25575  isi1f  25591  i1fd  25598  itg1mulc  25621  mbfi1fseqlem4  25635  itg2lcl  25644  isibl  25682  iblitg  25685  iblcnlem1  25705  iblcnlem  25706  iblrelem  25708  iblpos  25710  itgeqa  25731  itgfsum  25744  itgabs  25752  limcvallem  25788  ellimc  25790  ellimc2  25794  limcmpt  25800  cnmptlimc  25807  dvbsss  25819  cpnfval  25850  elcpn  25852  dvmptfsum  25895  dvle  25928  dvfsumle  25942  dvfsumleOLD  25943  dvfsumge  25944  dvfsumabs  25945  dvfsumrlimf  25947  dvfsumlem1  25948  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumlem3  25951  dvfsumlem4  25952  dvfsumrlimge0  25953  dvfsumrlim  25954  dvfsumrlim2  25955  dvfsum2  25957  itgsubstlem  25971  itgsubst  25972  mdegcl  25990  deg1nn0clb  26011  isuc1p  26062  plyeq0lem  26131  plyco  26162  plycj  26199  plycjOLD  26201  dvply2g  26208  dvnply2  26211  plydivlem4  26220  fta1lem  26231  fta1  26232  elqaalem1  26243  elqaalem2  26244  elqaalem3  26245  elqaa  26246  ulmcau  26320  radcnv0  26341  radcnvlt1  26343  radcnvle  26345  pserdvlem2  26354  coseq1  26450  efeq1  26453  sinord  26459  efif1olem2  26468  efif1olem4  26470  lognegb  26515  logcj  26531  argimgt0  26537  logtayl  26585  2irrexpq  26656  root1eq1  26681  logrec  26689  2irrexpqALT  26726  angrteqvd  26732  angpieqvdlem  26754  atans  26856  atans2  26857  dmarea  26883  areambl  26884  rlimcnp  26891  rlimcnp2  26892  xrlimcnp  26894  harmonicbnd  26930  harmonicbnd2  26931  lgamcvglem  26966  wilthlem2  26995  wilth  26997  efnnfsumcl  27029  vmacl  27044  efvmacl  27046  efchtdvds  27085  sqff1o  27108  fsumdvdscom  27111  musumsum  27118  fsumdvdsmul  27121  fsumdvdsmulOLD  27123  fsumvma  27140  perfect  27158  dchrelbasd  27166  lgsval  27228  lgsval2lem  27234  lgsdir2lem4  27255  lgsdir2  27257  lgsqrlem1  27273  lgsdchr  27282  m1lgs  27315  2lgs  27334  mul2sq  27346  2sqlem6  27350  2sqblem  27358  2sq2  27360  rplogsumlem2  27412  dchrisumlema  27415  dchrisumlem2  27417  dchrisumlem3  27418  dchrvmasumlem2  27425  dchrvmasumlem3  27426  dchrisum0flblem2  27436  dchrisum0flb  27437  dchrisum0fno1  27438  ostthlem1  27554  nodmon  27578  noextendseq  27595  nodense  27620  madefi  27845  addsproplem1  27899  addsproplem3  27901  addsprop  27906  addsf  27912  addsbdaylem  27946  negsproplem1  27957  negsproplem3  27959  negsprop  27964  negsbdaylem  27985  mulsproplemcbv  28041  mulsproplem1  28042  mulsproplem10  28051  mulsprop  28056  noseqp1  28208  noseqind  28209  peano5n0s  28235  dfn0s2  28247  n0addscl  28259  n0mulscl  28260  n0sbday  28267  onsfi  28270  n0s0m1  28275  n0subs  28276  n0p1nns  28283  dfnns2  28284  nn1m1nns  28286  zaddscl  28305  zmulscld  28308  elzn0s  28309  peano5uzs  28315  expscllem  28340  zs12addscl  28372  zs12half  28375  zs12negsclb  28376  zs12zodd  28377  zs12bday  28379  mirval  28618  perpneq  28677  isperp2  28678  isperp2d  28679  foot  28685  islnopp  28702  islnoppd  28703  outpasch  28718  hlpasch  28719  ishpg  28722  colopp  28732  colhp  28733  lmif  28748  islmib  28750  lmiinv  28755  trgcopy  28767  trgcopyeu  28769  acopyeu  28797  inaghl  28808  tgasa1  28821  f1otrgitv  28833  f1otrg  28834  isfusgr  29281  opfusgr  29286  fusgrfisbase  29291  fusgrfisstep  29292  nbupgrel  29308  nbumgrvtx  29309  nbusgreledg  29316  edgnbusgreu  29330  nb3grprlem1  29343  uvtxusgrel  29366  cusgredg  29387  cplgr2vpr  29396  cusgrexg  29407  usgredgsscusgredg  29423  fusgrn0degnn0  29463  rusgrnumwrdl2  29550  rgrx0ndm  29557  wlkcomp  29594  wlkdlem2  29645  clwlkcomp  29742  iswwlks  29799  wwlknllvtx  29809  0enwwlksnge1  29827  wlkiswwlks2lem5  29836  wwlksm1edg  29844  wwlksnred  29855  wwlksnext  29856  wwlksnextbi  29857  wwlksnredwwlkn  29858  wwlksnextfun  29861  wwlksnextinj  29862  wwlksnextsurj  29863  wwlksnextbij  29865  wwlksnfi  29869  wwlksnextproplem2  29873  wwlksnextprop  29875  2wlkdlem4  29891  rusgrnumwwlkl1  29931  rusgrnumwwlks  29937  isclwwlk  29946  clwwlk1loop  29950  clwwlkccatlem  29951  clwlkclwwlklem2a1  29954  clwlkclwwlklem2a4  29959  clwlkclwwlklem2a  29960  clwlkclwwlklem2  29962  clwlkclwwlklem3  29963  clwlkclwwlk  29964  clwlkclwwlk2  29965  clwwisshclwwslemlem  29975  clwwisshclwwslem  29976  clwwisshclwws  29977  clwwlknlbonbgr1  30001  clwwlkinwwlk  30002  clwwlkn1  30003  loopclwwlkn1b  30004  clwwlkn1loopb  30005  clwwlkn2  30006  clwwlkel  30008  clwwlkf  30009  clwwlkwwlksb  30016  clwwlkext2edg  30018  wwlksext2clwwlk  30019  wwlksubclwwlk  30020  eleclclwwlknlem2  30023  umgr2cwwk2dif  30026  s2elclwwlknon2  30066  clwwlknonwwlknonb  30068  clwwlknonex2lem2  30070  clwwlknonex2  30071  3wlkdlem4  30124  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  eupth2lem2  30181  eulerpathpr  30202  1vwmgr  30238  3vfriswmgrlem  30239  3vfriswmgr  30240  3cyclfrgrrn1  30247  vdgn1frgrv2  30258  frgrncvvdeqlem3  30263  frgrncvvdeqlem8  30268  frgrncvvdeqlem9  30269  frgrwopregasn  30278  frgrwopregbsn  30279  frgrwopreglem5ALT  30284  frgr2wwlk1  30291  frgr2wwlkeqm  30293  fusgr2wsp2nb  30296  2clwwlk2clwwlklem  30308  extwwlkfabel  30315  nvvop  30571  isnvlem  30572  sspval  30685  nmorepnf  30730  phpar  30786  siilem2  30814  bnsscmcl  30830  ubthlem1  30832  shaddcl  31179  shmulcl  31180  hsn0elch  31210  hhssablo  31225  hhssnvt  31227  hhsssh  31231  shscl  31280  shintcl  31292  chintcl  31294  shincl  31343  chincl  31461  h1datomi  31543  chscllem2  31600  sumspansn  31611  spansncvi  31614  5oalem2  31617  5oalem3  31618  pjini  31661  pjjsi  31662  eigposi  31798  nmoprepnf  31829  nmfnrepnf  31842  dmadjrnb  31868  lnophmlem1  31978  lnophm  31981  nmcopex  31991  lnconi  31995  nmbdfnlb  32012  nmcfnex  32015  imaelshi  32020  rnbra  32069  leopg  32084  pjbdlni  32111  pjhmop  32112  hmopidmch  32115  pjclem4  32161  pj3si  32169  strlem1  32212  atssma  32340  atcv0eq  32341  atcv1  32342  atomli  32344  atcvatlem  32347  cdj3lem2a  32398  cdj3lem3a  32401  xppreima  32602  fmptcof2  32614  aciunf1lem  32619  funcnv4mpt  32626  1stpreimas  32662  f1od2  32677  fpwrelmapffslem  32688  xrofsup  32723  fzspl  32745  fzsplit3  32749  nnindf  32777  fprodex01  32783  fsumiunle  32787  indfval  32812  indf1ofs  32822  gsumhashmul  33027  fzto1st  33058  fxpsubm  33127  fxpsubg  33128  fxpsubrg  33129  isslmd  33157  slmdlema  33158  elrgspnlem2  33196  elrgspnlem4  33198  subsdrg  33250  qusker  33299  0nellinds  33320  unitprodclb  33339  nsgmgclem  33361  nsgmgc  33362  nsgqusf1olem2  33364  elrspunidl  33378  prmidlval  33387  prmidlc  33398  opprlidlabs  33435  dfufd2lem  33499  lindsunlem  33599  brfldext  33620  brfinext  33627  finexttrb  33639  extdg1id  33640  fldextrspunlsplem  33647  constrconj  33714  constrfin  33715  trisecnconstr  33761  smatrcl  33765  submateq  33778  lmatfval  33783  lmatcl  33785  qtophaus  33805  locfinreflem  33809  locfinref  33810  zartopn  33844  zarcmplem  33850  rhmpreimacnlem  33853  xpinpreima  33875  xpinpreima2  33876  cnre2csqlem  33879  tpr2rico  33881  prsdm  33883  prsrn  33884  ordtrest2NEWlem  33891  ordtrest2NEW  33892  zrhcntr  33948  qqhval2  33951  isrrext  33969  ismntoplly  33994  esumcvg  34055  sigaval  34080  issiga  34081  0elsiga  34083  sigaclcu  34086  issgon  34092  prsiga  34100  sigaclci  34101  difelsiga  34102  unelsiga  34103  ispisys2  34122  inelpisys  34123  unelldsys  34127  sigapildsyslem  34130  sigapildsys  34131  ldgenpisyslem1  34132  ldgenpisys  34135  isros  34137  unelros  34140  difelros  34141  fiunelros  34143  inelsros  34147  diffiunisros  34148  rossros  34149  measvuni  34183  measiun  34187  voliune  34198  volfiniune  34199  brfae  34217  ismbfm  34220  mbfmcnvima  34225  mbfmcst  34229  1stmbfm  34230  2ndmbfm  34231  imambfm  34232  sitgval  34302  issibf  34303  sibfima  34308  sitgfval  34311  sitgclg  34312  eulerpartlemelr  34327  eulerpartlemsf  34329  eulerpartleme  34333  eulerpartlemt0  34339  eulerpartlemt  34341  eulerpartgbij  34342  eulerpartlemr  34344  eulerpartlemmf  34345  eulerpartlemgvv  34346  eulerpartlemgs2  34350  eulerpartlemn  34351  eulerpart  34352  cndprobprob  34408  rrvsum  34424  orvcelel  34440  ballotlemodife  34468  ballotlemsdom  34482  ballotlemrv  34490  ballotlemrv1  34491  ballotlemrv2  34492  ballotlem1ri  34505  fsum2dsub  34577  reprinfz1  34592  reprpmtf1o  34596  reprdifc  34597  breprexplema  34600  hgt750lema  34627  hgt750leme  34628  bnj149  34844  bnj222  34852  bnj1112  34952  bnj1148  34965  fineqvrep  35072  gblacfnacd  35077  vonf1owev  35083  loop1cycl  35112  subfacp1lem3  35157  subfacp1lem6  35160  erdszelem10  35175  kur14  35191  cvxsconn  35218  cnllysconn  35220  resconn  35221  iscvm  35234  cvmliftlem5  35264  cvmliftlem15  35273  cvmlift2lem1  35277  cvmlift2lem12  35289  cvmlift2lem13  35290  sat1el2xp  35354  fmlasuc  35361  gonan0  35367  gonar  35370  satefvfmla0  35393  msubrn  35504  msubco  35506  ismfs  35524  mvtinf  35530  mclsax  35544  mppspstlem  35546  elmpps  35548  nnuni  35702  dfdm5  35748  dfrn5  35749  elima4  35751  rdgprc0  35769  pprodss4v  35860  elfuns  35891  fnimage  35905  imageval  35906  fwddifval  36138  fwddifnval  36139  fwddifnp1  36141  elhf2g  36152  hfun  36154  hfninf  36162  filnetlem4  36357  onsucconn  36414  onsucsuccmp  36420  limsucncmp  36422  onint1  36425  fveleq  36427  findreccl  36429  nndivsub  36433  weiunse  36444  bj-seex  36898  bj-adjg1  37019  bj-mooreset  37078  bj-ismoored0  37082  bj-ismoored  37083  bj-inftyexpitaudisj  37181  bj-inftyexpidisj  37186  bj-isvec  37263  bj-isclm  37267  csbmpo123  37307  topdifinffinlem  37323  topdifinffin  37324  csbfinxpg  37364  phpreu  37586  finixpnum  37587  lindsenlbs  37597  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem22  37624  poimirlem23  37625  poimirlem24  37626  poimirlem25  37627  poimirlem26  37628  poimirlem28  37630  poimirlem29  37631  poimirlem30  37632  poimirlem31  37633  poimirlem32  37634  poimir  37635  mblfinlem3  37641  ex-ovoliunnfl  37645  voliunnfl  37646  volsupnfl  37647  mbfresfi  37648  itgabsnc  37671  ftc1anclem6  37680  ftc1anclem7  37681  ftc1anclem8  37682  ftc1anc  37683  dvasin  37686  sdclem2  37724  fdc  37727  incsequz  37730  neificl  37735  mettrifi  37739  cntotbnd  37778  cnpwstotbnd  37779  ismtyima  37785  ismtyhmeolem  37786  heiborlem2  37794  heiborlem3  37795  heiborlem4  37796  heiborlem5  37797  heiborlem6  37798  heiborlem10  37802  isrngo  37879  isdivrngo  37932  drngoi  37933  idlval  37995  isidlc  37997  idladdcl  38001  idllmulcl  38002  idlrmulcl  38003  0idl  38007  pridlval  38015  smprngopr  38034  prnc  38049  ispridlc  38052  pridlc  38053  eqrelf  38232  iss2  38314  elcoeleqvrels  38574  elfunsALTV  38672  eldisjs  38702  eleldisjs  38708  fsumshftd  38933  riotaclbgBAD  38935  renegclALT  38944  lshpinN  38970  isopos  39161  oposlem  39163  glbconN  39358  glbconNOLD  39359  lnnat  39409  2at0mat0  39507  islvol2aN  39574  dalawlem13  39865  pclfinclN  39932  lhpoc2N  39997  ltrncnvatb  40120  cdleme11h  40248  cdlemefr32sn2aw  40386  cdlemefs32sn1aw  40396  cdleme32fvaw  40421  cdlemg1fvawlemN  40555  dicelvalN  41160  dih1dimatlem  41311  dihlatat  41319  dihjatcclem4  41403  islpolN  41465  lpolsatN  41470  lpolpolsatN  41471  mapdordlem1a  41616  mapdordlem1  41618  mapdhcl  41709  iscsrg  41946  fzsplitnd  41958  lcmineqlem12  42016  intlewftc  42037  dvrelogpow2b  42044  aks4d1p1p3  42045  aks4d1p1p2  42046  aks4d1p1p4  42047  dvle2  42048  aks4d1p8  42063  aks4d1p9  42064  isprimroot  42069  primrootsunit1  42073  primrootscoprmpow  42075  aks6d1c1p1  42083  aks6d1c1p2  42085  aks6d1c1p3  42086  evl1gprodd  42093  hashscontpow  42098  aks6d1c3  42099  aks6d1c2  42106  sticksstones1  42122  sticksstones10  42131  sticksstones11  42132  sticksstones12a  42133  aks6d1c6lem1  42146  unitscyglem5  42175  retire  42295  reelznn0nn  42437  fsuppind  42566  fsuppssindlem2  42568  fsuppssind  42569  isnacs3  42686  nacsfix  42688  mzpclval  42701  mzpcl1  42705  mzpcl2  42706  mzpcl34  42707  mzpexpmpt  42721  mzpsubst  42724  diophin  42748  diophun  42749  2rexfrabdioph  42772  3rexfrabdioph  42773  4rexfrabdioph  42774  6rexfrabdioph  42775  7rexfrabdioph  42776  rabdiophlem2  42778  diophren  42789  fphpd  42792  fphpdo  42793  fiphp3d  42795  pellexlem1  42805  pell14qrexpclnn0  42842  pellqrex  42855  rmspecnonsq  42883  monotuz  42917  monotoddzzfi  42918  monotoddzz  42919  oddcomabszz  42920  modabsdifz  42962  rmxdioph  42992  expdiophlem2  42998  limsuc2  43017  dfac11  43038  kelac1  43039  dfac21  43042  lsmfgcl  43050  islnm  43053  lnmlssfg  43056  lmhmfgima  43060  pwslnm  43070  unxpwdom3  43071  pwfi2f1o  43072  islnr  43087  hbtlem2  43100  cnsrexpcl  43141  flcidc  43146  mendlmod  43165  proot1ex  43172  oaordnr  43272  omnord1  43281  oenord1  43292  cantnfresb  43300  onmcl  43307  tfsnfin  43328  nadd2rabtr  43360  nadd1rabtr  43364  nadd1rabex  43366  nadd1suc  43368  pwelg  43536  fipjust  43541  elnonrel  43561  elinlem  43574  elcnvlem  43577  ss2iundf  43635  dfhe3  43751  dffrege115  43954  rfovcnvf1od  43980  ntrneiel2  44062  clsneiel2  44085  neicvgel2  44096  grur1cld  44208  dvgrat  44288  cvgdvgrat  44289  radcnvrat  44290  binomcxplemdvsum  44331  binomcxplemnotnn0  44332  orbitcl  44934  modelaxreplem1  44955  modelaxreplem2  44956  modelaxrep  44958  fnchoice  45010  fiiuncl  45046  disjf1  45164  disjinfi  45173  choicefi  45181  axccdom  45203  fmptf  45220  fmptff  45250  monoords  45282  supminfrnmpt  45428  supxrleubrnmptf  45434  supminfxr  45447  supminfxr2  45452  supminfxrrnmpt  45454  monoordxrv  45464  monoordxr  45465  monoord2xrv  45466  monoord2xr  45467  caucvgbf  45472  cvgcaule  45474  fsummulc1f  45556  fsumnncl  45557  fsumf1of  45559  fsumreclf  45561  fsumlessf  45562  fsumsermpt  45564  fmul01  45565  fmulcl  45566  fmuldfeqlem1  45567  fmuldfeq  45568  fmul01lt1lem1  45569  fmul01lt1lem2  45570  fprodexp  45579  fprodabs2  45580  mccllem  45582  mccl  45583  fprodcnlem  45584  fprodcn  45585  climmulf  45589  climsuse  45593  climrecf  45594  climaddf  45600  climf  45607  sumnnodd  45615  clim2f  45621  0ellimcdiv  45634  climsubmpt  45645  climreclf  45649  climf2  45651  fnlimcnv  45652  climeldmeqmpt  45653  clim2f2  45655  climfveqmpt  45656  fnlimfvre  45659  fnlimabslt  45664  climfveqmpt3  45667  climbddf  45672  climeldmeqmpt3  45674  climinf2mpt  45699  climinfmpt  45700  limsupequzmptf  45716  lmbr3  45732  liminfreuzlem  45787  coseq0  45849  cncfshift  45859  cncfperiod  45864  fprodcncf  45885  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvmptmulf  45922  dvnmptdivc  45923  dvnmul  45928  dvmptfprod  45930  iblspltprt  45958  itgspltprt  45964  stoweidlem2  45987  stoweidlem3  45988  stoweidlem4  45989  stoweidlem6  45991  stoweidlem8  45993  stoweidlem17  46002  stoweidlem19  46004  stoweidlem20  46005  stoweidlem21  46006  stoweidlem23  46008  stoweidlem27  46012  stoweidlem35  46020  stoweidlem42  46027  stoweidlem43  46028  stoweidlem62  46047  stoweid  46048  wallispilem3  46052  wallispi  46055  fourierdlem16  46108  fourierdlem21  46113  fourierdlem41  46133  fourierdlem42  46134  fourierdlem48  46139  fourierdlem49  46140  fourierdlem50  46141  fourierdlem51  46142  fourierdlem54  46145  fourierdlem63  46154  fourierdlem64  46155  fourierdlem65  46156  fourierdlem71  46162  fourierdlem72  46163  fourierdlem73  46164  fourierdlem83  46174  fourierdlem86  46177  fourierdlem89  46180  fourierdlem90  46181  fourierdlem91  46182  fourierdlem96  46187  fourierdlem97  46188  fourierdlem98  46189  fourierdlem99  46190  fourierdlem100  46191  fourierdlem103  46194  fourierdlem104  46195  fourierdlem105  46196  fourierdlem108  46199  fourierdlem109  46200  fourierdlem110  46201  fourierdlem112  46203  fourierdlem113  46204  etransclem24  46243  salunicl  46301  saluncl  46302  saldifcl  46304  sge0f1o  46367  sge0lempt  46395  sge0iunmptlemfi  46398  sge0p1  46399  sge0fodjrnlem  46401  sge0iunmpt  46403  sge0ltfirpmpt2  46411  sge0isummpt2  46417  sge0xaddlem2  46419  sge0xadd  46420  ismea  46436  nnfoctbdjlem  46440  nnfoctbdj  46441  meadjiun  46451  voliunsge0lem  46457  meaiuninclem  46465  meaiuninc3v  46469  hoidmvlelem2  46581  hoidmvlelem3  46582  vonvolmbl2  46648  hoimbl2  46650  vonhoire  46657  vonicclem2  46669  vonn0ioo2  46675  vonn0icc2  46677  salpreimagelt  46692  salpreimalegt  46694  salpreimagtge  46710  salpreimaltle  46711  issmf  46713  salpreimagtlt  46715  smfpreimalt  46716  smfpreimaltf  46721  issmfle  46730  smfpreimale  46739  issmfgt  46741  smfpreimagt  46747  issmfgelem  46754  issmfge  46755  smflimlem4  46759  smflim  46762  smfpreimage  46767  smfresal  46773  smfpimbor1lem1  46783  smfpimbor1lem2  46784  smflim2  46791  smflimmpt  46795  smflimsuplem1  46805  smflimsuplem2  46806  smflimsuplem3  46807  smflimsuplem5  46809  smflimsuplem7  46811  smflimsup  46813  smfliminf  46816  ormkglobd  46860  cjnpoly  46877  eu2ndop1stv  47113  dmfcoafv  47163  ffnaov  47187  faovcl  47188  funressndmafv2rn  47211  dfatdmfcoafv2  47242  mod2addne  47352  smonoord  47359  iccpartiltu  47410  iccpartigtl  47411  sprsymrelf1lem  47479  prproropf1olem2  47492  fmtno4prmfac193  47561  proththdlem  47601  proththd  47602  iseven  47616  isodd  47617  dfodd2  47624  evenm1odd  47627  evenp1odd  47628  enege  47633  onego  47634  epee  47693  perfectALTV  47711  bgoldbtbndlem2  47794  bgoldbtbndlem3  47795  bgoldbtbndlem4  47796  bgoldbtbnd  47797  clnbupgrel  47822  edgusgrclnbfin  47830  grimuhgr  47875  uhgrimedgi  47878  uhgrimprop  47880  isuspgrim0  47882  isuspgrimlem  47883  grimedg  47923  grtriproplem  47927  grtrif1o  47930  isgrtri  47931  grtriclwlk3  47933  cycl3grtrilem  47934  cycl3grtri  47935  grimgrtri  47937  usgrgrtrirex  47938  isubgr3stgrlem7  47960  grlimprclnbgrvtx  47987  grlimgredgex  47988  grlimgrtri  47991  usgrexmpl1tri  48013  gpgvtxel2  48036  gpgvtx0  48041  gpgvtx1  48042  gpgedgvtx0  48049  gpgedgvtx1  48050  gpgedgiov  48053  gpgedg2ov  48054  gpgedg2iv  48055  gpgnbgrvtx0  48062  gpgnbgrvtx1  48063  gpg3kgrtriex  48077  gpgprismgr4cycllem3  48085  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem2lem1  48102  pgnbgreunbgrlem2lem2  48103  pgnbgreunbgrlem2lem3  48104  pgnbgreunbgrlem4  48107  pgnbgreunbgrlem5lem1  48108  pgnbgreunbgrlem5lem2  48109  pgnbgreunbgrlem5lem3  48110  pgnbgreunbgr  48113  grlimedgnedg  48119  uzlidlring  48223  cbvmpox2  48324  lmod1  48481  nnolog2flm1  48579  dignn0flhalflem1  48604  catprsc  49002  nelsubc3lem  49059  fucofulem2  49300  fucofvalne  49314  isthincd2lem2  49424  euendfunc  49515  cnelsubclem  49592