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  3575  reuind  3721  sbcel2  4377  sbccsb2  4396  disjiun  5090  breq1  5105  breq2  5106  axrep6g  5240  inex1g  5269  intex  5294  pwexg  5328  reusv2lem4  5351  reusv2  5353  reusv3  5355  rabxfrd  5367  prex  5387  opelopabsb  5485  csbmpt12  5512  pofun  5557  seex  5590  seinxp  5715  opabid2  5782  opeliunxp2  5792  elrn2g  5844  opeldmd  5860  opeldm  5861  elreldm  5888  elsnres  5981  iss  5995  unielrel  6235  onunel  6427  funopg  6534  brprcneu  6830  brprcneuALT  6831  tz6.12f  6866  ndmfvrcl  6876  ssimaex  6928  dmfco  6939  fvmpti  6949  fvmpt3  6954  fvmptf  6971  fvmptss2  6976  respreima  7020  fvn0ssdmfun  7028  fvelrn  7030  ffnfvf  7074  ffvresb  7079  fmptco  7083  fmptcof  7084  fsn  7089  fsn2g  7092  fressnfv  7114  fvrnressn  7115  fvn0fvelrnOLD  7117  fnex  7173  funfvima  7186  funfvima3  7192  f1mpt  7218  fliftfuns  7271  isoselem  7298  isowe2  7307  riotaclb  7367  ovrspc2v  7395  ffnov  7495  fovcld  7496  ovmpos  7517  ov2gf  7518  ovg  7534  funimassov  7546  oprssdm  7550  ndmovrcl  7555  caovclg  7561  elovmpo  7614  ofmpteq  7656  sorpsscmpl  7690  uniexg  7696  unexbOLD  7704  abnexg  7712  difsnexi  7717  onint  7746  limsuc  7805  tfisi  7815  peano5  7849  xpexr  7874  xpexcnv  7876  fnexALT  7909  focdmex  7914  f1stres  7971  f2ndres  7972  xp1st  7979  xp2nd  7980  unielxp  7985  opiota  8017  fmpox  8025  offval22  8044  frxp  8082  fnse  8089  frxp2  8100  sexp2  8102  frxp3  8107  sexp3  8109  opeliunxp2f  8166  dftpos4  8201  fvmpocurryd  8227  undefnel2  8233  onnseq  8290  smoel  8306  smo11  8310  tfrlem8  8329  tfrlem9  8330  tfrlem15  8337  tfr2b  8341  tz7.44-2  8352  tz7.44-3  8353  oacl  8476  omcl  8477  oecl  8478  oaord1  8492  omordi  8507  oen0  8527  oeeui  8543  nnacl  8552  nnmcl  8553  nnecl  8554  nnmordi  8572  nnaordex  8579  omsmolem  8598  naddcllem  8617  naddov2  8620  naddf  8622  naddssim  8626  naddelim  8627  naddasslem1  8635  naddasslem2  8636  naddsuc2  8642  erexb  8673  elecex  8698  qliftfuns  8754  ixpsnval  8850  elixp2  8851  resixp  8883  undifixp  8884  mptelixpg  8885  resixpfo  8886  elixpsn  8887  fundmen  8979  fopwdom  9026  disjen  9075  xpf1o  9080  unfi  9112  cnvfi  9117  fnfi  9119  f1oenfirn  9121  f1domfi  9122  unblem2  9216  imafiOLD  9241  pwfi  9244  xpfiOLD  9246  fiint  9253  fiintOLD  9254  iunfi  9270  isfsupp  9292  fsuppun  9314  ffsuppbi  9325  elfi2  9341  wdom2d  9509  ixpiunwdom  9519  dfom3  9576  cantnfvalf  9594  cantnflt  9601  cantnflem1  9618  r1fin  9702  tz9.12lem3  9718  ranksnb  9756  ranklim  9773  r1pw  9774  r1pwALT  9775  r1pwcl  9776  rankuni2b  9782  djuexb  9838  cardmin2  9928  infxpenc2lem1  9948  dfac8alem  9958  dfac8clem  9961  ac5num  9965  acni2  9975  acnlem  9977  alephon  9998  alephfplem3  10035  alephfplem4  10036  dfac4  10051  dfac5lem1  10052  dfac5lem5  10056  dfac2a  10059  dfac2b  10060  dfacacn  10071  dfac12lem2  10074  dfac12r  10076  dfac12k  10077  cofsmo  10198  cfsmolem  10199  isfin1a  10221  fin1ai  10222  isfin3  10225  infpssrlem3  10234  fin23lem7  10245  fin23lem11  10246  enfin2i  10250  isf34lem4  10306  fin1a2lem7  10335  hsmexlem9  10354  hsmexlem4  10358  hsmex  10361  axcc2lem  10365  axcc3  10367  axdc3lem2  10380  axcclem  10386  zornn0g  10434  ttukeylem3  10440  ttukeylem6  10443  ttukey2g  10445  brdom7disj  10460  brdom6disj  10461  fnct  10466  konigthlem  10497  axregndlem2  10532  axinfnd  10535  axacndlem5  10540  axacnd  10541  fpwwe2lem4  10563  fpwwe2lem12  10571  fpwwe  10575  pwfseqlem1  10587  pwfseqlem3  10589  pwfseqlem4a  10590  pwfseqlem4  10591  wununi  10635  wunpw  10636  wunpr  10638  wunr1om  10648  tskpw  10682  tskr1om  10696  inar1  10704  grupw  10724  grupr  10726  gruurn  10727  gruiun  10728  ingru  10744  grur1a  10748  grothomex  10758  grothac  10759  addnidpi  10830  indpi  10836  adderpq  10885  mulerpq  10886  addclprlem2  10946  mulclprlem  10948  distrlem4pr  10955  prlem934  10962  ltexprlem3  10967  ltexprlem4  10968  ltexprlem7  10971  ltexpri  10972  prlem936  10976  reclem2pr  10977  reclem3pr  10978  addclsr  11012  mulclsr  11013  supsrlem  11040  supsr  11041  axaddf  11074  axmulf  11075  axaddrcl  11081  axmulrcl  11083  renegcl  11461  negreb  11463  negn0  11583  negf1o  11584  ltord1  11680  leord1  11681  eqord1  11682  ltord2  11683  leord2  11684  eqord2  11685  negfi  12108  infm3  12118  cju  12158  peano5nni  12165  peano2nn  12174  dfnn2  12175  nn1m1nn  12183  nnaddcl  12185  nnmulcl  12186  nnsub  12206  nndivtr  12209  un0addcl  12451  un0mulcl  12452  elnnnn0  12461  nn0sub  12468  fcdmnn0fsuppg  12478  elz  12507  nnnegz  12508  elz2  12523  znegclb  12546  zaddcl  12549  nzadd  12557  zmulcl  12558  zneo  12593  nneo  12594  zeo  12596  peano5uzi  12599  zindd  12611  eluzsubOLD  12805  uzp1  12810  uzaddcl  12839  ublbneg  12868  eqreznegel  12869  supminf  12870  zsupss  12872  qmulz  12886  qnegcl  12901  irradd  12908  irrmul  12909  xnn0xaddcl  13171  fzrev2  13525  injresinjlem  13724  negmod0  13816  om2uzuzi  13890  uzindi  13923  fsuppmapnn0ub  13936  mptnn0fsuppr  13940  seqexw  13958  seqcl2  13961  seqcl  13963  seqf  13964  monoord  13973  monoord2  13974  sermono  13975  seqsplit  13976  seqcaopr2  13979  seqid3  13987  seqhomo  13990  expcllem  14013  expcl2lem  14014  m1expcl2  14026  faccl  14224  facdiv  14228  facndiv  14229  bccmpl  14250  bccl  14263  hashclb  14299  hasheq0  14304  hashfn  14316  seqcoll  14405  opfi1uzind  14452  ccatalpha  14534  reuccatpfxs1lem  14687  reuccatpfxs1  14688  repswccat  14727  repswrevw  14728  2cshw  14754  2cshwcshw  14767  cshimadifsn  14771  cshco  14778  swrd2lsw  14894  wwlktovf  14898  wwlktovf1  14899  wwlktovfo  14900  wrd2f1tovbij  14902  shftlem  15010  shftf  15021  cjval  15044  cjth  15045  remim  15059  cnpart  15182  uzin2  15287  caubnd2  15300  sqreulem  15302  clim  15436  clim2  15446  lo1o12  15475  climrlim2  15489  lo1resb  15506  o1resb  15508  lo1eq  15510  climmpt2  15515  climshftlem  15516  rlimcld2  15520  climcn1  15534  climcn2  15535  o1dif  15572  iserex  15599  climub  15604  climserle  15605  isercoll  15610  climcau  15613  caurcvg2  15620  caucvgb  15622  summolem3  15656  summolem2a  15657  zsum  15660  fsum  15662  sumss2  15668  fsumcvg2  15669  fsumclf  15680  fsumsplitf  15684  fsumsplit1  15687  sumpr  15690  sumtp  15691  fsumm1  15693  fsum1p  15695  isummulc2  15704  fsum2dlem  15712  fsumcom2  15716  fsumshftm  15723  fsum0diag2  15725  fsumge1  15739  fsum00  15740  fsumabs  15743  telfsumo  15744  telfsumo2  15745  fsumparts  15748  fsumrlim  15753  fsumo1  15754  o1fsum  15755  fsumiun  15763  binomlem  15771  isumshft  15781  isum1p  15783  isumrpcl  15785  climcndslem1  15791  climcndslem2  15792  climcnds  15793  infcvgaux2i  15800  cvgrat  15825  mertens  15828  clim2prod  15830  prodfn0  15836  prodfrec  15837  prodfdiv  15838  ntrivcvgfvn0  15841  prodmolem3  15875  prodmolem2a  15876  zprod  15879  fprod  15883  prodss  15889  fprodser  15891  fprodm1  15909  fprod1p  15910  fprodm1s  15912  fprodp1s  15913  fprodabs  15916  fprodn0  15921  fprod2dlem  15922  fprodcnv  15925  fprodcom2  15926  fproddivf  15929  fprodsplitf  15930  fprodsplit1f  15932  bpolycl  15994  fprodefsum  16037  rpnnen2lem11  16168  mod2eq1n2dvds  16293  mulsucdiv2z  16299  zob  16305  nn0o1gt2  16327  nno  16328  nn0o  16329  divalglem7  16345  bitsf1  16392  sadcp1  16401  smupp1  16426  qnumdencl  16685  iserodd  16782  pcqcl  16803  pcxnn0cl  16807  pcxcl  16808  pcgcd1  16824  dvdsprmpweqle  16833  pcmpt  16839  pcmpt2  16840  pcmptdvds  16841  infpnlem2  16858  infpn2  16860  1arith  16874  elgz  16878  mul4sq  16901  4sqlem13  16904  4sqlem17  16908  4sqlem18  16909  4sqlem19  16910  vdwlem1  16928  vdwlem2  16929  vdwnn  16945  ramtcl2  16958  ramcl  16976  prmonn2  16986  prmodvdslcmf  16994  isstruct2  17095  wunress  17195  firest  17371  imasaddfnlem  17467  imasvscafn  17476  xpsfrnel2  17503  mreintcl  17532  ismred2  17540  mreexexlemd  17581  mreexexlem3d  17583  mreexexlem4d  17584  iscatd2  17618  catpropd  17646  subsubc  17791  isfunc  17802  inclfusubc  17881  fncnvimaeqv  18057  joindef  18311  joinval  18312  meetdef  18325  meetval  18326  oduclatb  18442  acsdrsel  18478  isacs4lem  18479  isacs5lem  18480  acsdrscl  18481  mgmsscl  18548  mgmpropd  18554  mgm1  18561  gsumvalx  18579  issubmgm  18605  issubmgm2  18606  mgmhmima  18618  sgrppropd  18634  mndpropd  18662  issubm  18706  0subm  18720  insubm  18721  mhmimalem  18727  gsumwsubmcl  18740  gsumwspan  18749  symggrplem  18787  sursubmefmnd  18799  injsubmefmnd  18800  smndex1basss  18808  mulgsubcl  18996  issubg  19034  issubg2  19049  issubg4  19053  0subg  19059  0subgOLD  19060  isnsg  19063  isnsg2  19064  nsgbi  19065  isnsg3  19068  elnmz  19071  nmzbi  19072  nmzsubg  19073  eqgval  19085  eqgid  19088  cycsubgcl  19114  ghmrn  19137  ghmnsgima  19148  gass  19209  oppgsubg  19271  f1omvdconj  19352  symgfisg  19374  psgneldm  19409  0subgALT  19474  odhash3  19482  sylow2blem2  19527  lsmsubm  19559  lsmsubg  19560  efgsf  19635  efgsdm  19636  efgs1b  19642  efgredlema  19646  eqgabl  19740  ablnsg  19753  cyggenod2  19791  gsumzaddlem  19827  gsummhm2  19845  gsum2dlem2  19877  gsum2d2lem  19879  gsumcom2  19881  dprdfeq0  19930  dprdsubg  19932  dprd2da  19950  ablfacrp  19974  pgpfac1lem3  19985  pgpfaclem1  19989  ablfaclem3  19995  ablfac2  19997  cycsubggenodd  20017  isrng  20039  issrg  20073  srgfcl  20081  rglcom4d  20096  srgbinomlem4  20114  isring  20122  iscrng  20125  dvdsr  20247  irredrmul  20312  isrngim  20330  isrim0OLD  20366  isrim0  20368  issubrng  20432  subrngringnsg  20438  issubrng2  20443  rhmimasubrnglem  20450  issubrg  20456  issubrg2  20477  subrgpropd  20493  isdrngd  20650  isdrngdOLD  20652  issdrg  20673  sdrgacs  20686  issrngd  20740  islmod  20746  lmodlema  20747  islmodd  20748  lmodprop2d  20806  rmodislmodlem  20811  rmodislmod  20812  lssset  20815  islssd  20817  lsscl  20824  lsslss  20843  lsspropd  20900  lmhmima  20930  lbsind  20963  lsmcl  20966  islvec  20987  lmhmlvec  20993  lspsolvlem  21028  lspsolv  21029  lvecpropd  21053  rnglidlmcl  21102  rnglidl0  21115  rnglidlmmgm  21131  rngqiprngimf1lem  21180  rngqiprngimf1  21186  ring2idlqus  21195  xrsdsreclblem  21305  xrsdsreclb  21306  cnsubrglem  21309  prmirred  21360  pzriprnglem4  21370  pzriprnglem8  21374  pzriprngALT  21381  znunithash  21450  cofipsgn  21478  zrhpsgnelbas  21479  rzgrp  21508  isphl  21513  phllmhm  21517  ipcl  21518  isphld  21539  phlpropd  21540  phlssphl  21544  cssincl  21573  pjdm  21592  dsmmval  21619  dsmmbas2  21622  dsmmelbas  21624  frlmbas  21640  frlmup1  21683  lindfind  21701  lindsind  21702  f1lindf  21707  islindf4  21723  psrbag  21802  psrbaglefi  21811  mplsubglem  21884  mpllsslem  21885  ltbwe  21927  psrbagsn  21946  subrgasclcl  21950  mplind  21953  mpfind  21990  psdmul  22029  coe1mul2lem2  22130  gsumply1eq  22172  evl1vsd  22207  mpfpf1  22214  pf1mpf  22215  pf1ind  22218  matecl  22288  m1detdiag  22460  mdetralt  22471  mdetralt2  22472  mdetunilem2  22476  mdetunilem9  22483  m2detleiblem3  22492  m2detleiblem4  22493  smadiadetlem0  22524  cpmatacl  22579  chpscmat  22705  uniopn  22760  inopn  22762  fiinopn  22764  istps  22797  fctop  22867  iscld  22890  isopn2  22895  mretopd  22955  iscldtop  22958  perfi  23018  tgrest  23022  restcld  23035  ordtbaslem  23051  ordtrest2lem  23066  ordtrest2  23067  iscn  23098  cnpval  23099  iscnp  23100  tgcn  23115  subbascn  23117  ssidcn  23118  lmbrf  23123  cnpnei  23127  cnima  23128  iscncl  23132  cnconst2  23146  cnrest2  23149  cnpresti  23151  cnprest  23152  cnindis  23155  lmres  23163  lmcnp  23167  iscnrm  23186  t1sncld  23189  cnrmi  23223  cncmp  23255  cmpsublem  23262  fiuncmp  23267  unconn  23292  conncompid  23294  conncompconn  23295  conncompss  23296  1stcfb  23308  2ndcrest  23317  2ndcctbss  23318  2ndcdisj  23319  1stccnp  23325  islly  23331  isnlly  23332  subislly  23344  restnlly  23345  restlly  23346  islly2  23347  hausllycmp  23357  cldllycmp  23358  dislly  23360  isptfin  23379  islocfin  23380  ptfinfin  23382  finlocfin  23383  dissnlocfin  23392  locfindis  23393  comppfsc  23395  kgenval  23398  elkgen  23399  kgeni  23400  cmpkgen  23414  1stckgenlem  23416  kgencn2  23420  ptpjpre1  23434  elpt  23435  elptr  23436  ptbasin  23440  xkobval  23449  xkoval  23450  xkoopn  23452  txbasval  23469  tx1cn  23472  tx2cn  23473  dfac14  23481  xkoccn  23482  txcnp  23483  ptcnplem  23484  txcnmpt  23487  txindislem  23496  txdis1cn  23498  txlly  23499  txnlly  23500  pthaus  23501  ptrescn  23502  hauseqlcld  23509  txlm  23511  tx2ndc  23514  txkgen  23515  xkoptsub  23517  xkopt  23518  xkoco1cn  23520  xkoco2cn  23521  xkococnlem  23522  xkococn  23523  cnmpt11  23526  cnmpt12  23530  cnmpt21  23534  cnmpt22  23537  cnmptkp  23543  cnmptk1p  23548  xkoinjcn  23550  txconn  23552  qtopval2  23559  elqtop  23560  idqtop  23569  qtopcld  23576  qtopeu  23579  qtoprest  23580  qtopomap  23581  qtopcmap  23582  ishmeo  23622  hmeoopn  23629  hmeocld  23630  ordthmeolem  23664  ptcmpfi  23676  elmptrab  23690  fgcl  23741  trfil2  23750  cfinfil  23756  uzrest  23760  ufilss  23768  trufil  23773  cfinufil  23791  ufinffr  23792  ufildr  23794  rnelfm  23816  flfcntr  23906  ptcmplem2  23916  ptcmplem3  23917  ptcmplem4  23918  ptcmplem5  23919  cnextfvval  23928  tmdcn2  23952  tmdmulg  23955  tmdgsum2  23959  symgtgp  23969  opnsubg  23971  clssubg  23972  tgpconncompeqg  23975  ghmcnp  23978  tgphaus  23980  tgpt0  23982  qustgpopn  23983  qustgplem  23984  tsmsgsum  24002  tsmssubm  24006  tsmsres  24007  tsmsf1o  24008  tsmsxplem1  24016  tsmsxplem2  24017  tsmsxp  24018  istrg  24027  istdrg  24029  istdrg2  24041  istlm  24048  istvc  24055  ustval  24066  ustincl  24071  ustdiag  24072  ustinvel  24073  ustexhalf  24074  ust0  24083  ucnima  24144  fmucndlem  24154  prdsdsf  24231  prdsxmet  24233  imasf1oxmet  24239  imasf1omet  24240  prdsxmslem2  24393  metustsym  24419  isnlm  24539  qtopbaslem  24622  xrtgioo  24671  reperflem  24683  fsumcn  24737  expcn  24739  expcnOLD  24741  xrhmeo  24820  cnllycmp  24831  bndth  24833  isclm  24940  lmhmclm  24963  lmmcvg  25137  fmcfil  25148  iscfil3  25149  iscau2  25153  iscau4  25155  iscmet3lem1  25167  iscmet3  25169  cfilres  25172  caussi  25173  equivcfil  25175  flimcfil  25190  bcthlem1  25200  isbn  25214  srabn  25236  ishl2  25246  cmslssbn  25248  cmscsscms  25249  minveclem3b  25304  ivthlem1  25328  ivthlem2  25329  ivthlem3  25330  ivth2  25332  ivthle  25333  ivthle2  25334  ivthicc  25335  ovolficcss  25346  ovolunlem1a  25373  ovolunlem1  25374  ovolfiniun  25378  ovoliunlem1  25379  ovoliunlem3  25381  ovoliun  25382  ovoliun2  25383  shft2rab  25385  ovolshftlem1  25386  sca2rab  25389  ovolscalem1  25390  mblsplit  25409  finiunmbl  25421  volun  25422  volfiniun  25424  voliunlem1  25427  voliunlem3  25429  iunmbl  25430  voliun  25431  volsup  25433  ioombl  25442  ioorcl  25454  vitalilem1  25485  vitalilem2  25486  vitalilem3  25487  vitalilem4  25488  vitali  25490  ismbf1  25501  mbfdm  25503  ismbf  25505  ismbfcn  25506  mbfima  25507  mbfimaicc  25508  ismbfcn2  25515  ismbfd  25516  ismbf2d  25517  mbfeqalem1  25518  mbfmax  25526  mbfposr  25529  mbfposb  25530  ismbf3d  25531  mbfimaopnlem  25532  mbfimaopn2  25534  cncombf  25535  isi1f  25551  i1fd  25558  itg1mulc  25581  mbfi1fseqlem4  25595  itg2lcl  25604  isibl  25642  iblitg  25645  iblcnlem1  25665  iblcnlem  25666  iblrelem  25668  iblpos  25670  itgeqa  25691  itgfsum  25704  itgabs  25712  limcvallem  25748  ellimc  25750  ellimc2  25754  limcmpt  25760  cnmptlimc  25767  dvbsss  25779  cpnfval  25810  elcpn  25812  dvmptfsum  25855  dvle  25888  dvfsumle  25902  dvfsumleOLD  25903  dvfsumge  25904  dvfsumabs  25905  dvfsumrlimf  25907  dvfsumlem1  25908  dvfsumlem2  25909  dvfsumlem2OLD  25910  dvfsumlem3  25911  dvfsumlem4  25912  dvfsumrlimge0  25913  dvfsumrlim  25914  dvfsumrlim2  25915  dvfsum2  25917  itgsubstlem  25931  itgsubst  25932  mdegcl  25950  deg1nn0clb  25971  isuc1p  26022  plyeq0lem  26091  plyco  26122  plycj  26159  plycjOLD  26161  dvply2g  26168  dvnply2  26171  plydivlem4  26180  fta1lem  26191  fta1  26192  elqaalem1  26203  elqaalem2  26204  elqaalem3  26205  elqaa  26206  ulmcau  26280  radcnv0  26301  radcnvlt1  26303  radcnvle  26305  pserdvlem2  26314  coseq1  26410  efeq1  26413  sinord  26419  efif1olem2  26428  efif1olem4  26430  lognegb  26475  logcj  26491  argimgt0  26497  logtayl  26545  2irrexpq  26616  root1eq1  26641  logrec  26649  2irrexpqALT  26686  angrteqvd  26692  angpieqvdlem  26714  atans  26816  atans2  26817  dmarea  26843  areambl  26844  rlimcnp  26851  rlimcnp2  26852  xrlimcnp  26854  harmonicbnd  26890  harmonicbnd2  26891  lgamcvglem  26926  wilthlem2  26955  wilth  26957  efnnfsumcl  26989  vmacl  27004  efvmacl  27006  efchtdvds  27045  sqff1o  27068  fsumdvdscom  27071  musumsum  27078  fsumdvdsmul  27081  fsumdvdsmulOLD  27083  fsumvma  27100  perfect  27118  dchrelbasd  27126  lgsval  27188  lgsval2lem  27194  lgsdir2lem4  27215  lgsdir2  27217  lgsqrlem1  27233  lgsdchr  27242  m1lgs  27275  2lgs  27294  mul2sq  27306  2sqlem6  27310  2sqblem  27318  2sq2  27320  rplogsumlem2  27372  dchrisumlema  27375  dchrisumlem2  27377  dchrisumlem3  27378  dchrvmasumlem2  27385  dchrvmasumlem3  27386  dchrisum0flblem2  27396  dchrisum0flb  27397  dchrisum0fno1  27398  ostthlem1  27514  nodmon  27538  noextendseq  27555  nodense  27580  madefi  27800  addsproplem1  27852  addsproplem3  27854  addsprop  27859  addsf  27865  addsbdaylem  27899  negsproplem1  27910  negsproplem3  27912  negsprop  27917  negsbdaylem  27938  mulsproplemcbv  27994  mulsproplem1  27995  mulsproplem10  28004  mulsprop  28009  noseqp1  28161  noseqind  28162  peano5n0s  28188  dfn0s2  28200  n0addscl  28212  n0mulscl  28213  n0sbday  28220  onsfi  28223  n0s0m1  28228  n0subs  28229  n0p1nns  28236  dfnns2  28237  nn1m1nns  28239  zaddscl  28258  zmulscld  28261  elzn0s  28262  peano5uzs  28268  expscllem  28292  zs12negsclb  28317  zs12bday  28319  mirval  28558  perpneq  28617  isperp2  28618  isperp2d  28619  foot  28625  islnopp  28642  islnoppd  28643  outpasch  28658  hlpasch  28659  ishpg  28662  colopp  28672  colhp  28673  lmif  28688  islmib  28690  lmiinv  28695  trgcopy  28707  trgcopyeu  28709  acopyeu  28737  inaghl  28748  tgasa1  28761  f1otrgitv  28773  f1otrg  28774  isfusgr  29221  opfusgr  29226  fusgrfisbase  29231  fusgrfisstep  29232  nbupgrel  29248  nbumgrvtx  29249  nbusgreledg  29256  edgnbusgreu  29270  nb3grprlem1  29283  uvtxusgrel  29306  cusgredg  29327  cplgr2vpr  29336  cusgrexg  29347  usgredgsscusgredg  29363  fusgrn0degnn0  29403  rusgrnumwrdl2  29490  rgrx0ndm  29497  wlkcomp  29534  wlkdlem2  29585  clwlkcomp  29682  iswwlks  29739  wwlknllvtx  29749  0enwwlksnge1  29767  wlkiswwlks2lem5  29776  wwlksm1edg  29784  wwlksnred  29795  wwlksnext  29796  wwlksnextbi  29797  wwlksnredwwlkn  29798  wwlksnextfun  29801  wwlksnextinj  29802  wwlksnextsurj  29803  wwlksnextbij  29805  wwlksnfi  29809  wwlksnextproplem2  29813  wwlksnextprop  29815  2wlkdlem4  29831  rusgrnumwwlkl1  29871  rusgrnumwwlks  29877  isclwwlk  29886  clwwlk1loop  29890  clwwlkccatlem  29891  clwlkclwwlklem2a1  29894  clwlkclwwlklem2a4  29899  clwlkclwwlklem2a  29900  clwlkclwwlklem2  29902  clwlkclwwlklem3  29903  clwlkclwwlk  29904  clwlkclwwlk2  29905  clwwisshclwwslemlem  29915  clwwisshclwwslem  29916  clwwisshclwws  29917  clwwlknlbonbgr1  29941  clwwlkinwwlk  29942  clwwlkn1  29943  loopclwwlkn1b  29944  clwwlkn1loopb  29945  clwwlkn2  29946  clwwlkel  29948  clwwlkf  29949  clwwlkwwlksb  29956  clwwlkext2edg  29958  wwlksext2clwwlk  29959  wwlksubclwwlk  29960  eleclclwwlknlem2  29963  umgr2cwwk2dif  29966  s2elclwwlknon2  30006  clwwlknonwwlknonb  30008  clwwlknonex2lem2  30010  clwwlknonex2  30011  3wlkdlem4  30064  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  eupth2lem2  30121  eulerpathpr  30142  1vwmgr  30178  3vfriswmgrlem  30179  3vfriswmgr  30180  3cyclfrgrrn1  30187  vdgn1frgrv2  30198  frgrncvvdeqlem3  30203  frgrncvvdeqlem8  30208  frgrncvvdeqlem9  30209  frgrwopregasn  30218  frgrwopregbsn  30219  frgrwopreglem5ALT  30224  frgr2wwlk1  30231  frgr2wwlkeqm  30233  fusgr2wsp2nb  30236  2clwwlk2clwwlklem  30248  extwwlkfabel  30255  nvvop  30511  isnvlem  30512  sspval  30625  nmorepnf  30670  phpar  30726  siilem2  30754  bnsscmcl  30770  ubthlem1  30772  shaddcl  31119  shmulcl  31120  hsn0elch  31150  hhssablo  31165  hhssnvt  31167  hhsssh  31171  shscl  31220  shintcl  31232  chintcl  31234  shincl  31283  chincl  31401  h1datomi  31483  chscllem2  31540  sumspansn  31551  spansncvi  31554  5oalem2  31557  5oalem3  31558  pjini  31601  pjjsi  31602  eigposi  31738  nmoprepnf  31769  nmfnrepnf  31782  dmadjrnb  31808  lnophmlem1  31918  lnophm  31921  nmcopex  31931  lnconi  31935  nmbdfnlb  31952  nmcfnex  31955  imaelshi  31960  rnbra  32009  leopg  32024  pjbdlni  32051  pjhmop  32052  hmopidmch  32055  pjclem4  32101  pj3si  32109  strlem1  32152  atssma  32280  atcv0eq  32281  atcv1  32282  atomli  32284  atcvatlem  32287  cdj3lem2a  32338  cdj3lem3a  32341  xppreima  32542  fmptcof2  32554  aciunf1lem  32559  funcnv4mpt  32566  1stpreimas  32602  f1od2  32617  fpwrelmapffslem  32628  xrofsup  32663  fzspl  32685  fzsplit3  32689  nnindf  32717  fprodex01  32723  fsumiunle  32727  indfval  32752  indf1ofs  32762  gsumhashmul  32974  fzto1st  33033  fxpsubm  33102  isslmd  33128  slmdlema  33129  elrgspnlem2  33167  elrgspnlem4  33169  subsdrg  33221  qusker  33293  0nellinds  33314  unitprodclb  33333  nsgmgclem  33355  nsgmgc  33356  nsgqusf1olem2  33358  elrspunidl  33372  prmidlval  33381  prmidlc  33392  opprlidlabs  33429  dfufd2lem  33493  lindsunlem  33593  brfldext  33614  brfinext  33621  finexttrb  33633  extdg1id  33634  fldextrspunlsplem  33641  constrconj  33708  constrfin  33709  trisecnconstr  33755  smatrcl  33759  submateq  33772  lmatfval  33777  lmatcl  33779  qtophaus  33799  locfinreflem  33803  locfinref  33804  zartopn  33838  zarcmplem  33844  rhmpreimacnlem  33847  xpinpreima  33869  xpinpreima2  33870  cnre2csqlem  33873  tpr2rico  33875  prsdm  33877  prsrn  33878  ordtrest2NEWlem  33885  ordtrest2NEW  33886  zrhcntr  33942  qqhval2  33945  isrrext  33963  ismntoplly  33988  esumcvg  34049  sigaval  34074  issiga  34075  0elsiga  34077  sigaclcu  34080  issgon  34086  prsiga  34094  sigaclci  34095  difelsiga  34096  unelsiga  34097  ispisys2  34116  inelpisys  34117  unelldsys  34121  sigapildsyslem  34124  sigapildsys  34125  ldgenpisyslem1  34126  ldgenpisys  34129  isros  34131  unelros  34134  difelros  34135  fiunelros  34137  inelsros  34141  diffiunisros  34142  rossros  34143  measvuni  34177  measiun  34181  voliune  34192  volfiniune  34193  brfae  34211  ismbfm  34214  mbfmcnvima  34219  mbfmcst  34223  1stmbfm  34224  2ndmbfm  34225  imambfm  34226  sitgval  34296  issibf  34297  sibfima  34302  sitgfval  34305  sitgclg  34306  eulerpartlemelr  34321  eulerpartlemsf  34323  eulerpartleme  34327  eulerpartlemt0  34333  eulerpartlemt  34335  eulerpartgbij  34336  eulerpartlemr  34338  eulerpartlemmf  34339  eulerpartlemgvv  34340  eulerpartlemgs2  34344  eulerpartlemn  34345  eulerpart  34346  cndprobprob  34402  rrvsum  34418  orvcelel  34434  ballotlemodife  34462  ballotlemsdom  34476  ballotlemrv  34484  ballotlemrv1  34485  ballotlemrv2  34486  ballotlem1ri  34499  fsum2dsub  34571  reprinfz1  34586  reprpmtf1o  34590  reprdifc  34591  breprexplema  34594  hgt750lema  34621  hgt750leme  34622  bnj149  34838  bnj222  34846  bnj1112  34946  bnj1148  34959  fineqvrep  35058  gblacfnacd  35062  vonf1owev  35068  loop1cycl  35097  subfacp1lem3  35142  subfacp1lem6  35145  erdszelem10  35160  kur14  35176  cvxsconn  35203  cnllysconn  35205  resconn  35206  iscvm  35219  cvmliftlem5  35249  cvmliftlem15  35258  cvmlift2lem1  35262  cvmlift2lem12  35274  cvmlift2lem13  35275  sat1el2xp  35339  fmlasuc  35346  gonan0  35352  gonar  35355  satefvfmla0  35378  msubrn  35489  msubco  35491  ismfs  35509  mvtinf  35515  mclsax  35529  mppspstlem  35531  elmpps  35533  nnuni  35687  dfdm5  35733  dfrn5  35734  elima4  35736  rdgprc0  35754  pprodss4v  35845  elfuns  35876  fnimage  35890  imageval  35891  fwddifval  36123  fwddifnval  36124  fwddifnp1  36126  elhf2g  36137  hfun  36139  hfninf  36147  filnetlem4  36342  onsucconn  36399  onsucsuccmp  36405  limsucncmp  36407  onint1  36410  fveleq  36412  findreccl  36414  nndivsub  36418  weiunse  36429  bj-seex  36883  bj-adjg1  37004  bj-mooreset  37063  bj-ismoored0  37067  bj-ismoored  37068  bj-inftyexpitaudisj  37166  bj-inftyexpidisj  37171  bj-isvec  37248  bj-isclm  37252  csbmpo123  37292  topdifinffinlem  37308  topdifinffin  37309  csbfinxpg  37349  phpreu  37571  finixpnum  37572  lindsenlbs  37582  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem22  37609  poimirlem23  37610  poimirlem24  37611  poimirlem25  37612  poimirlem26  37613  poimirlem28  37615  poimirlem29  37616  poimirlem30  37617  poimirlem31  37618  poimirlem32  37619  poimir  37620  mblfinlem3  37626  ex-ovoliunnfl  37630  voliunnfl  37631  volsupnfl  37632  mbfresfi  37633  itgabsnc  37656  ftc1anclem6  37665  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  dvasin  37671  sdclem2  37709  fdc  37712  incsequz  37715  neificl  37720  mettrifi  37724  cntotbnd  37763  cnpwstotbnd  37764  ismtyima  37770  ismtyhmeolem  37771  heiborlem2  37779  heiborlem3  37780  heiborlem4  37781  heiborlem5  37782  heiborlem6  37783  heiborlem10  37787  isrngo  37864  isdivrngo  37917  drngoi  37918  idlval  37980  isidlc  37982  idladdcl  37986  idllmulcl  37987  idlrmulcl  37988  0idl  37992  pridlval  38000  smprngopr  38019  prnc  38034  ispridlc  38037  pridlc  38038  eqrelf  38217  iss2  38299  elcoeleqvrels  38559  elfunsALTV  38657  eldisjs  38687  eleldisjs  38693  fsumshftd  38918  riotaclbgBAD  38920  renegclALT  38929  lshpinN  38955  isopos  39146  oposlem  39148  glbconN  39343  glbconNOLD  39344  lnnat  39394  2at0mat0  39492  islvol2aN  39559  dalawlem13  39850  pclfinclN  39917  lhpoc2N  39982  ltrncnvatb  40105  cdleme11h  40233  cdlemefr32sn2aw  40371  cdlemefs32sn1aw  40381  cdleme32fvaw  40406  cdlemg1fvawlemN  40540  dicelvalN  41145  dih1dimatlem  41296  dihlatat  41304  dihjatcclem4  41388  islpolN  41450  lpolsatN  41455  lpolpolsatN  41456  mapdordlem1a  41601  mapdordlem1  41603  mapdhcl  41694  iscsrg  41931  fzsplitnd  41943  lcmineqlem12  42001  intlewftc  42022  dvrelogpow2b  42029  aks4d1p1p3  42030  aks4d1p1p2  42031  aks4d1p1p4  42032  dvle2  42033  aks4d1p8  42048  aks4d1p9  42049  isprimroot  42054  primrootsunit1  42058  primrootscoprmpow  42060  aks6d1c1p1  42068  aks6d1c1p2  42070  aks6d1c1p3  42071  evl1gprodd  42078  hashscontpow  42083  aks6d1c3  42084  aks6d1c2  42091  sticksstones1  42107  sticksstones10  42116  sticksstones11  42117  sticksstones12a  42118  aks6d1c6lem1  42131  unitscyglem5  42160  retire  42280  reelznn0nn  42422  fsuppind  42551  fsuppssindlem2  42553  fsuppssind  42554  isnacs3  42671  nacsfix  42673  mzpclval  42686  mzpcl1  42690  mzpcl2  42691  mzpcl34  42692  mzpexpmpt  42706  mzpsubst  42709  diophin  42733  diophun  42734  2rexfrabdioph  42757  3rexfrabdioph  42758  4rexfrabdioph  42759  6rexfrabdioph  42760  7rexfrabdioph  42761  rabdiophlem2  42763  diophren  42774  fphpd  42777  fphpdo  42778  fiphp3d  42780  pellexlem1  42790  pell14qrexpclnn0  42827  pellqrex  42840  rmspecnonsq  42868  monotuz  42903  monotoddzzfi  42904  monotoddzz  42905  oddcomabszz  42906  modabsdifz  42948  rmxdioph  42978  expdiophlem2  42984  limsuc2  43003  dfac11  43024  kelac1  43025  dfac21  43028  lsmfgcl  43036  islnm  43039  lnmlssfg  43042  lmhmfgima  43046  pwslnm  43056  unxpwdom3  43057  pwfi2f1o  43058  islnr  43073  hbtlem2  43086  cnsrexpcl  43127  flcidc  43132  mendlmod  43151  proot1ex  43158  oaordnr  43258  omnord1  43267  oenord1  43278  cantnfresb  43286  onmcl  43293  tfsnfin  43314  nadd2rabtr  43346  nadd1rabtr  43350  nadd1rabex  43352  nadd1suc  43354  pwelg  43522  fipjust  43527  elnonrel  43547  elinlem  43560  elcnvlem  43563  ss2iundf  43621  dfhe3  43737  dffrege115  43940  rfovcnvf1od  43966  ntrneiel2  44048  clsneiel2  44071  neicvgel2  44082  grur1cld  44194  dvgrat  44274  cvgdvgrat  44275  radcnvrat  44276  binomcxplemdvsum  44317  binomcxplemnotnn0  44318  orbitcl  44920  modelaxreplem1  44941  modelaxreplem2  44942  modelaxrep  44944  fnchoice  44996  fiiuncl  45032  disjf1  45150  disjinfi  45159  choicefi  45167  axccdom  45189  fmptf  45206  fmptff  45236  monoords  45268  supminfrnmpt  45414  supxrleubrnmptf  45420  supminfxr  45433  supminfxr2  45438  supminfxrrnmpt  45440  monoordxrv  45450  monoordxr  45451  monoord2xrv  45452  monoord2xr  45453  caucvgbf  45458  cvgcaule  45460  fsummulc1f  45542  fsumnncl  45543  fsumf1of  45545  fsumreclf  45547  fsumlessf  45548  fsumsermpt  45550  fmul01  45551  fmulcl  45552  fmuldfeqlem1  45553  fmuldfeq  45554  fmul01lt1lem1  45555  fmul01lt1lem2  45556  fprodexp  45565  fprodabs2  45566  mccllem  45568  mccl  45569  fprodcnlem  45570  fprodcn  45571  climmulf  45575  climsuse  45579  climrecf  45580  climaddf  45586  climf  45593  sumnnodd  45601  clim2f  45607  0ellimcdiv  45620  climsubmpt  45631  climreclf  45635  climf2  45637  fnlimcnv  45638  climeldmeqmpt  45639  clim2f2  45641  climfveqmpt  45642  fnlimfvre  45645  fnlimabslt  45650  climfveqmpt3  45653  climbddf  45658  climeldmeqmpt3  45660  climinf2mpt  45685  climinfmpt  45686  limsupequzmptf  45702  lmbr3  45718  liminfreuzlem  45773  coseq0  45835  cncfshift  45845  cncfperiod  45850  fprodcncf  45871  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvmptmulf  45908  dvnmptdivc  45909  dvnmul  45914  dvmptfprod  45916  iblspltprt  45944  itgspltprt  45950  stoweidlem2  45973  stoweidlem3  45974  stoweidlem4  45975  stoweidlem6  45977  stoweidlem8  45979  stoweidlem17  45988  stoweidlem19  45990  stoweidlem20  45991  stoweidlem21  45992  stoweidlem23  45994  stoweidlem27  45998  stoweidlem35  46006  stoweidlem42  46013  stoweidlem43  46014  stoweidlem62  46033  stoweid  46034  wallispilem3  46038  wallispi  46041  fourierdlem16  46094  fourierdlem21  46099  fourierdlem41  46119  fourierdlem42  46120  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem51  46128  fourierdlem54  46131  fourierdlem63  46140  fourierdlem64  46141  fourierdlem65  46142  fourierdlem71  46148  fourierdlem72  46149  fourierdlem73  46150  fourierdlem83  46160  fourierdlem86  46163  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem96  46173  fourierdlem97  46174  fourierdlem98  46175  fourierdlem99  46176  fourierdlem100  46177  fourierdlem103  46180  fourierdlem104  46181  fourierdlem105  46182  fourierdlem108  46185  fourierdlem109  46186  fourierdlem110  46187  fourierdlem112  46189  fourierdlem113  46190  etransclem24  46229  salunicl  46287  saluncl  46288  saldifcl  46290  sge0f1o  46353  sge0lempt  46381  sge0iunmptlemfi  46384  sge0p1  46385  sge0fodjrnlem  46387  sge0iunmpt  46389  sge0ltfirpmpt2  46397  sge0isummpt2  46403  sge0xaddlem2  46405  sge0xadd  46406  ismea  46422  nnfoctbdjlem  46426  nnfoctbdj  46427  meadjiun  46437  voliunsge0lem  46443  meaiuninclem  46451  meaiuninc3v  46455  hoidmvlelem2  46567  hoidmvlelem3  46568  vonvolmbl2  46634  hoimbl2  46636  vonhoire  46643  vonicclem2  46655  vonn0ioo2  46661  vonn0icc2  46663  salpreimagelt  46678  salpreimalegt  46680  salpreimagtge  46696  salpreimaltle  46697  issmf  46699  salpreimagtlt  46701  smfpreimalt  46702  smfpreimaltf  46707  issmfle  46716  smfpreimale  46725  issmfgt  46727  smfpreimagt  46733  issmfgelem  46740  issmfge  46741  smflimlem4  46745  smflim  46748  smfpreimage  46753  smfresal  46759  smfpimbor1lem1  46769  smfpimbor1lem2  46770  smflim2  46777  smflimmpt  46781  smflimsuplem1  46791  smflimsuplem2  46792  smflimsuplem3  46793  smflimsuplem5  46795  smflimsuplem7  46797  smflimsup  46799  smfliminf  46802  ormkglobd  46846  cjnpoly  46863  eu2ndop1stv  47099  dmfcoafv  47149  ffnaov  47173  faovcl  47174  funressndmafv2rn  47197  dfatdmfcoafv2  47228  mod2addne  47338  smonoord  47345  iccpartiltu  47396  iccpartigtl  47397  sprsymrelf1lem  47465  prproropf1olem2  47478  fmtno4prmfac193  47547  proththdlem  47587  proththd  47588  iseven  47602  isodd  47603  dfodd2  47610  evenm1odd  47613  evenp1odd  47614  enege  47619  onego  47620  epee  47679  perfectALTV  47697  bgoldbtbndlem2  47780  bgoldbtbndlem3  47781  bgoldbtbndlem4  47782  bgoldbtbnd  47783  clnbupgrel  47808  edgusgrclnbfin  47815  grimuhgr  47860  uhgrimedgi  47863  uhgrimprop  47865  isuspgrim0  47867  isuspgrimlem  47868  grimedg  47908  grtriproplem  47911  grtrif1o  47914  isgrtri  47915  grtriclwlk3  47917  cycl3grtrilem  47918  cycl3grtri  47919  grimgrtri  47921  usgrgrtrirex  47922  isubgr3stgrlem7  47944  grlimgrtri  47968  usgrexmpl1tri  47989  gpgvtxel2  48012  gpgvtx0  48017  gpgvtx1  48018  gpgedgvtx0  48025  gpgedgvtx1  48026  gpgedgiov  48029  gpgedg2ov  48030  gpgedg2iv  48031  gpgnbgrvtx0  48038  gpgnbgrvtx1  48039  gpg3kgrtriex  48053  gpgprismgr4cycllem3  48060  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  pgnbgreunbgrlem4  48082  pgnbgreunbgrlem5lem1  48083  pgnbgreunbgrlem5lem2  48084  pgnbgreunbgrlem5lem3  48085  pgnbgreunbgr  48088  uzlidlring  48196  cbvmpox2  48297  lmod1  48454  nnolog2flm1  48552  dignn0flhalflem1  48577  catprsc  48975  nelsubc3lem  49032  fucofulem2  49273  fucofvalne  49287  isthincd2lem2  49397  euendfunc  49488  cnelsubclem  49565