Theorem eleq1d 2829

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.) Allow shortening of eleq1 2832. (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 2751	. . . 4 ⊢ (𝜑 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
3	2	anbi1d 630	. . 3 ⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
4	3	exbidv 1920	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
5		dfclel 2820	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶))
6		dfclel 2820	. 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eleq1  2832  eleq12d  2838  eqeltrd  2844  eqneltrd  2864  rspcimdv  3625  reuind  3775  sbcel2  4441  sbccsb2  4460  disjiun  5154  breq1  5169  breq2  5170  axrep6g  5311  inex1g  5337  intex  5362  pwexg  5396  reusv2lem4  5419  reusv2  5421  reusv3  5423  rabxfrd  5435  prex  5452  opelopabsb  5549  csbmpt12  5576  pofun  5626  seex  5659  seinxp  5783  opabid2  5852  opeliunxp2  5863  elrn2g  5915  opeldmd  5931  opeldm  5932  elreldm  5960  elsnres  6050  iss  6064  elimasngOLD  6120  unielrel  6305  onunel  6500  funopg  6612  funimaexgOLD  6665  brprcneu  6910  brprcneuALT  6911  tz6.12f  6946  ndmfvrcl  6956  ssimaex  7007  dmfco  7018  fvmpti  7028  fvmpt3  7033  fvmptf  7050  fvmptss2  7055  respreima  7099  fvn0ssdmfun  7108  fvelrn  7110  ffnfvf  7154  ffvresb  7159  fmptco  7163  fmptcof  7164  fsn  7169  fsn2g  7172  fressnfv  7194  fvrnressn  7195  fvn0fvelrnOLD  7197  fnex  7254  funfvima  7267  funfvima3  7273  f1mpt  7298  fliftfuns  7350  isoselem  7377  isowe2  7386  riotaclb  7446  ovrspc2v  7474  ffnov  7576  fovcld  7577  ovmpos  7598  ov2gf  7599  ovg  7615  funimassov  7627  oprssdm  7631  ndmovrcl  7636  caovclg  7642  elovmpo  7695  ofmpteq  7736  sorpsscmpl  7769  uniexg  7775  unexbOLD  7783  abnexg  7791  difsnexi  7796  onint  7826  limsuc  7886  tfisi  7896  peano5  7932  xpexr  7958  xpexcnv  7960  fnexALT  7991  focdmex  7996  f1stres  8054  f2ndres  8055  xp1st  8062  xp2nd  8063  unielxp  8068  opiota  8100  fmpox  8108  offval22  8129  frxp  8167  fnse  8174  frxp2  8185  sexp2  8187  frxp3  8192  sexp3  8194  opeliunxp2f  8251  dftpos4  8286  fvmpocurryd  8312  undefnel2  8318  onnseq  8400  smoel  8416  smo11  8420  tfrlem8  8440  tfrlem9  8441  tfrlem15  8448  tfr2b  8452  tz7.44-2  8463  tz7.44-3  8464  oacl  8591  omcl  8592  oecl  8593  oaord1  8607  omordi  8622  oen0  8642  oeeui  8658  nnacl  8667  nnmcl  8668  nnecl  8669  nnmordi  8687  nnaordex  8694  omsmolem  8713  naddcllem  8732  naddov2  8735  naddf  8737  naddssim  8741  naddelim  8742  naddasslem1  8750  naddasslem2  8751  naddsuc2  8757  erexb  8788  qliftfuns  8862  ixpsnval  8958  elixp2  8959  resixp  8991  undifixp  8992  mptelixpg  8993  resixpfo  8994  elixpsn  8995  fundmen  9096  fopwdom  9146  disjen  9200  xpf1o  9205  unfi  9238  cnvfi  9243  fnfi  9244  f1oenfirn  9246  f1domfi  9247  unblem2  9357  imafiOLD  9382  pwfi  9385  xpfiOLD  9387  fiint  9394  fiintOLD  9395  iunfi  9411  pwfiOLD  9417  isfsupp  9435  fsuppun  9456  ffsuppbi  9467  elfi2  9483  wdom2d  9649  ixpiunwdom  9659  dfom3  9716  cantnfvalf  9734  cantnflt  9741  cantnflem1  9758  r1fin  9842  tz9.12lem3  9858  ranksnb  9896  ranklim  9913  r1pw  9914  r1pwALT  9915  r1pwcl  9916  rankuni2b  9922  djuexb  9978  cardmin2  10068  infxpenc2lem1  10088  dfac8alem  10098  dfac8clem  10101  ac5num  10105  acni2  10115  acnlem  10117  alephon  10138  alephfplem3  10175  alephfplem4  10176  dfac4  10191  dfac5lem1  10192  dfac5lem5  10196  dfac2a  10199  dfac2b  10200  dfacacn  10211  dfac12lem2  10214  dfac12r  10216  dfac12k  10217  cofsmo  10338  cfsmolem  10339  isfin1a  10361  fin1ai  10362  isfin3  10365  infpssrlem3  10374  fin23lem7  10385  fin23lem11  10386  enfin2i  10390  isf34lem4  10446  fin1a2lem7  10475  hsmexlem9  10494  hsmexlem4  10498  hsmex  10501  axcc2lem  10505  axcc3  10507  axdc3lem2  10520  axcclem  10526  zornn0g  10574  ttukeylem3  10580  ttukeylem6  10583  ttukey2g  10585  brdom7disj  10600  brdom6disj  10601  fnct  10606  konigthlem  10637  axregndlem2  10672  axinfnd  10675  axacndlem5  10680  axacnd  10681  fpwwe2lem4  10703  fpwwe2lem12  10711  fpwwe  10715  pwfseqlem1  10727  pwfseqlem3  10729  pwfseqlem4a  10730  pwfseqlem4  10731  wununi  10775  wunpw  10776  wunpr  10778  wunr1om  10788  tskpw  10822  tskr1om  10836  inar1  10844  grupw  10864  grupr  10866  gruurn  10867  gruiun  10868  ingru  10884  grur1a  10888  grothomex  10898  grothac  10899  addnidpi  10970  indpi  10976  adderpq  11025  mulerpq  11026  addclprlem2  11086  mulclprlem  11088  distrlem4pr  11095  prlem934  11102  ltexprlem3  11107  ltexprlem4  11108  ltexprlem7  11111  ltexpri  11112  prlem936  11116  reclem2pr  11117  reclem3pr  11118  addclsr  11152  mulclsr  11153  supsrlem  11180  supsr  11181  axaddf  11214  axmulf  11215  axaddrcl  11221  axmulrcl  11223  renegcl  11599  negreb  11601  negn0  11719  negf1o  11720  ltord1  11816  leord1  11817  eqord1  11818  ltord2  11819  leord2  11820  eqord2  11821  negfi  12244  infm3  12254  cju  12289  peano5nni  12296  peano2nn  12305  dfnn2  12306  nn1m1nn  12314  nnaddcl  12316  nnmulcl  12317  nnsub  12337  nndivtr  12340  un0addcl  12586  un0mulcl  12587  elnnnn0  12596  nn0sub  12603  fcdmnn0fsuppg  12612  elz  12641  nnnegz  12642  elz2  12657  znegclb  12680  zaddcl  12683  nzadd  12691  zmulcl  12692  zneo  12726  nneo  12727  zeo  12729  peano5uzi  12732  zindd  12744  eluzsubOLD  12939  uzp1  12944  uzaddcl  12969  ublbneg  12998  eqreznegel  12999  supminf  13000  zsupss  13002  qmulz  13016  qnegcl  13031  irradd  13038  irrmul  13039  xnn0xaddcl  13297  fzrev2  13648  injresinjlem  13837  negmod0  13929  om2uzuzi  14000  uzindi  14033  fsuppmapnn0ub  14046  mptnn0fsuppr  14050  seqexw  14068  seqcl2  14071  seqcl  14073  seqf  14074  monoord  14083  monoord2  14084  sermono  14085  seqsplit  14086  seqcaopr2  14089  seqid3  14097  seqhomo  14100  expcllem  14123  expcl2lem  14124  m1expcl2  14136  faccl  14332  facdiv  14336  facndiv  14337  bccmpl  14358  bccl  14371  hashclb  14407  hasheq0  14412  hashfn  14424  seqcoll  14513  opfi1uzind  14560  ccatalpha  14641  reuccatpfxs1lem  14794  reuccatpfxs1  14795  repswccat  14834  repswrevw  14835  2cshw  14861  2cshwcshw  14874  cshimadifsn  14878  cshco  14885  swrd2lsw  15001  wwlktovf  15005  wwlktovf1  15006  wwlktovfo  15007  wrd2f1tovbij  15009  shftlem  15117  shftf  15128  cjval  15151  cjth  15152  remim  15166  cnpart  15289  uzin2  15393  caubnd2  15406  sqreulem  15408  clim  15540  clim2  15550  lo1o12  15579  climrlim2  15593  lo1resb  15610  o1resb  15612  lo1eq  15614  climmpt2  15619  climshftlem  15620  rlimcld2  15624  climcn1  15638  climcn2  15639  o1dif  15676  iserex  15705  climub  15710  climserle  15711  isercoll  15716  climcau  15719  caurcvg2  15726  caucvgb  15728  summolem3  15762  summolem2a  15763  zsum  15766  fsum  15768  sumss2  15774  fsumcvg2  15775  fsumclf  15786  fsumsplitf  15790  fsumsplit1  15793  sumpr  15796  sumtp  15797  fsumm1  15799  fsum1p  15801  isummulc2  15810  fsum2dlem  15818  fsumcom2  15822  fsumshftm  15829  fsum0diag2  15831  fsumge1  15845  fsum00  15846  fsumabs  15849  telfsumo  15850  telfsumo2  15851  fsumparts  15854  fsumrlim  15859  fsumo1  15860  o1fsum  15861  fsumiun  15869  binomlem  15877  isumshft  15887  isum1p  15889  isumrpcl  15891  climcndslem1  15897  climcndslem2  15898  climcnds  15899  infcvgaux2i  15906  cvgrat  15931  mertens  15934  clim2prod  15936  prodfn0  15942  prodfrec  15943  prodfdiv  15944  ntrivcvgfvn0  15947  prodmolem3  15981  prodmolem2a  15982  zprod  15985  fprod  15989  prodss  15995  fprodser  15997  fprodm1  16015  fprod1p  16016  fprodm1s  16018  fprodp1s  16019  fprodabs  16022  fprodn0  16027  fprod2dlem  16028  fprodcnv  16031  fprodcom2  16032  fproddivf  16035  fprodsplitf  16036  fprodsplit1f  16038  bpolycl  16100  fprodefsum  16143  rpnnen2lem11  16272  mod2eq1n2dvds  16395  mulsucdiv2z  16401  zob  16407  nn0o1gt2  16429  nno  16430  nn0o  16431  divalglem7  16447  bitsf1  16492  sadcp1  16501  smupp1  16526  qnumdencl  16786  iserodd  16882  pcqcl  16903  pcxnn0cl  16907  pcxcl  16908  pcgcd1  16924  dvdsprmpweqle  16933  pcmpt  16939  pcmpt2  16940  pcmptdvds  16941  infpnlem2  16958  infpn2  16960  1arith  16974  elgz  16978  mul4sq  17001  4sqlem13  17004  4sqlem17  17008  4sqlem18  17009  4sqlem19  17010  vdwlem1  17028  vdwlem2  17029  vdwnn  17045  ramtcl2  17058  ramcl  17076  prmonn2  17086  prmodvdslcmf  17094  isstruct2  17196  wunress  17309  wunressOLD  17310  firest  17492  imasaddfnlem  17588  imasvscafn  17597  xpsfrnel2  17624  mreintcl  17653  ismred2  17661  mreexexlemd  17702  mreexexlem3d  17704  mreexexlem4d  17705  iscatd2  17739  catpropd  17767  subsubc  17917  isfunc  17928  inclfusubc  18008  fncnvimaeqv  18188  joindef  18446  joinval  18447  meetdef  18460  meetval  18461  oduclatb  18577  acsdrsel  18613  isacs4lem  18614  isacs5lem  18615  acsdrscl  18616  mgmsscl  18683  mgmpropd  18689  mgm1  18696  gsumvalx  18714  issubmgm  18740  issubmgm2  18741  mgmhmima  18753  sgrppropd  18769  mndpropd  18797  issubm  18838  0subm  18852  insubm  18853  mhmimalem  18859  gsumwsubmcl  18872  gsumwspan  18881  symggrplem  18919  sursubmefmnd  18931  injsubmefmnd  18932  smndex1basss  18940  mulgsubcl  19128  issubg  19166  issubg2  19181  issubg4  19185  0subg  19191  0subgOLD  19192  isnsg  19195  isnsg2  19196  nsgbi  19197  isnsg3  19200  elnmz  19203  nmzbi  19204  nmzsubg  19205  eqgval  19217  eqgid  19220  cycsubgcl  19246  ghmrn  19269  ghmnsgima  19280  gass  19341  oppgsubg  19406  f1omvdconj  19488  symgfisg  19510  psgneldm  19545  0subgALT  19610  odhash3  19618  sylow2blem2  19663  lsmsubm  19695  lsmsubg  19696  efgsf  19771  efgsdm  19772  efgs1b  19778  efgredlema  19782  eqgabl  19876  ablnsg  19889  cyggenod2  19927  gsumzaddlem  19963  gsummhm2  19981  gsum2dlem2  20013  gsum2d2lem  20015  gsumcom2  20017  dprdfeq0  20066  dprdsubg  20068  dprd2da  20086  ablfacrp  20110  pgpfac1lem3  20121  pgpfaclem1  20125  ablfaclem3  20131  ablfac2  20133  cycsubggenodd  20153  isrng  20181  issrg  20215  srgfcl  20223  rglcom4d  20238  srgbinomlem4  20256  isring  20264  iscrng  20267  dvdsr  20388  irredrmul  20453  isrngim  20471  isrim0OLD  20507  isrim0  20509  issubrng  20573  subrngringnsg  20579  issubrng2  20584  rhmimasubrnglem  20591  issubrg  20599  issubrg2  20620  subrgpropd  20636  isdrngd  20787  isdrngdOLD  20789  issdrg  20811  sdrgacs  20824  issrngd  20878  islmod  20884  lmodlema  20885  islmodd  20886  lmodprop2d  20944  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  lssset  20954  islssd  20956  lsscl  20963  lsslss  20982  lsspropd  21039  lmhmima  21069  lbsind  21102  lsmcl  21105  islvec  21126  lmhmlvec  21132  lspsolvlem  21167  lspsolv  21168  lvecpropd  21192  rnglidlmcl  21249  rnglidl0  21262  rnglidlmmgm  21278  rngqiprngimf1lem  21327  rngqiprngimf1  21333  ring2idlqus  21342  xrsdsreclblem  21453  xrsdsreclb  21454  cnsubrglem  21457  prmirred  21508  pzriprnglem4  21518  pzriprnglem8  21522  pzriprngALT  21529  znunithash  21606  cofipsgn  21634  zrhpsgnelbas  21635  rzgrp  21664  isphl  21669  phllmhm  21673  ipcl  21674  isphld  21695  phlpropd  21696  phlssphl  21700  cssincl  21729  pjdm  21750  dsmmval  21777  dsmmbas2  21780  dsmmelbas  21782  frlmbas  21798  frlmup1  21841  lindfind  21859  lindsind  21860  f1lindf  21865  islindf4  21881  psrbag  21960  psrbaglefi  21969  mplsubglem  22042  mpllsslem  22043  ltbwe  22085  psrbagsn  22110  subrgasclcl  22114  mplind  22117  mpfind  22154  psdmul  22193  coe1mul2lem2  22292  gsumply1eq  22334  evl1vsd  22369  mpfpf1  22376  pf1mpf  22377  pf1ind  22380  matecl  22452  m1detdiag  22624  mdetralt  22635  mdetralt2  22636  mdetunilem2  22640  mdetunilem9  22647  m2detleiblem3  22656  m2detleiblem4  22657  smadiadetlem0  22688  cpmatacl  22743  chpscmat  22869  uniopn  22924  inopn  22926  fiinopn  22928  istps  22961  fctop  23032  iscld  23056  isopn2  23061  mretopd  23121  iscldtop  23124  perfi  23184  tgrest  23188  restcld  23201  ordtbaslem  23217  ordtrest2lem  23232  ordtrest2  23233  iscn  23264  cnpval  23265  iscnp  23266  tgcn  23281  subbascn  23283  ssidcn  23284  lmbrf  23289  cnpnei  23293  cnima  23294  iscncl  23298  cnconst2  23312  cnrest2  23315  cnpresti  23317  cnprest  23318  cnindis  23321  lmres  23329  lmcnp  23333  iscnrm  23352  t1sncld  23355  cnrmi  23389  cncmp  23421  cmpsublem  23428  fiuncmp  23433  unconn  23458  conncompid  23460  conncompconn  23461  conncompss  23462  1stcfb  23474  2ndcrest  23483  2ndcctbss  23484  2ndcdisj  23485  1stccnp  23491  islly  23497  isnlly  23498  subislly  23510  restnlly  23511  restlly  23512  islly2  23513  hausllycmp  23523  cldllycmp  23524  dislly  23526  isptfin  23545  islocfin  23546  ptfinfin  23548  finlocfin  23549  dissnlocfin  23558  locfindis  23559  comppfsc  23561  kgenval  23564  elkgen  23565  kgeni  23566  cmpkgen  23580  1stckgenlem  23582  kgencn2  23586  ptpjpre1  23600  elpt  23601  elptr  23602  ptbasin  23606  xkobval  23615  xkoval  23616  xkoopn  23618  txbasval  23635  tx1cn  23638  tx2cn  23639  dfac14  23647  xkoccn  23648  txcnp  23649  ptcnplem  23650  txcnmpt  23653  txindislem  23662  txdis1cn  23664  txlly  23665  txnlly  23666  pthaus  23667  ptrescn  23668  hauseqlcld  23675  txlm  23677  tx2ndc  23680  txkgen  23681  xkoptsub  23683  xkopt  23684  xkoco1cn  23686  xkoco2cn  23687  xkococnlem  23688  xkococn  23689  cnmpt11  23692  cnmpt12  23696  cnmpt21  23700  cnmpt22  23703  cnmptkp  23709  cnmptk1p  23714  xkoinjcn  23716  txconn  23718  qtopval2  23725  elqtop  23726  idqtop  23735  qtopcld  23742  qtopeu  23745  qtoprest  23746  qtopomap  23747  qtopcmap  23748  ishmeo  23788  hmeoopn  23795  hmeocld  23796  ordthmeolem  23830  ptcmpfi  23842  elmptrab  23856  fgcl  23907  trfil2  23916  cfinfil  23922  uzrest  23926  ufilss  23934  trufil  23939  cfinufil  23957  ufinffr  23958  ufildr  23960  rnelfm  23982  flfcntr  24072  ptcmplem2  24082  ptcmplem3  24083  ptcmplem4  24084  ptcmplem5  24085  cnextfvval  24094  tmdcn2  24118  tmdmulg  24121  tmdgsum2  24125  symgtgp  24135  opnsubg  24137  clssubg  24138  tgpconncompeqg  24141  ghmcnp  24144  tgphaus  24146  tgpt0  24148  qustgpopn  24149  qustgplem  24150  tsmsgsum  24168  tsmssubm  24172  tsmsres  24173  tsmsf1o  24174  tsmsxplem1  24182  tsmsxplem2  24183  tsmsxp  24184  istrg  24193  istdrg  24195  istdrg2  24207  istlm  24214  istvc  24221  ustval  24232  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  ust0  24249  ucnima  24311  fmucndlem  24321  prdsdsf  24398  prdsxmet  24400  imasf1oxmet  24406  imasf1omet  24407  prdsxmslem2  24563  metustsym  24589  isnlm  24717  qtopbaslem  24800  xrtgioo  24847  reperflem  24859  fsumcn  24913  expcn  24915  expcnOLD  24917  xrhmeo  24996  cnllycmp  25007  bndth  25009  isclm  25116  lmhmclm  25139  lmmcvg  25314  fmcfil  25325  iscfil3  25326  iscau2  25330  iscau4  25332  iscmet3lem1  25344  iscmet3  25346  cfilres  25349  caussi  25350  equivcfil  25352  flimcfil  25367  bcthlem1  25377  isbn  25391  srabn  25413  ishl2  25423  cmslssbn  25425  cmscsscms  25426  minveclem3b  25481  ivthlem1  25505  ivthlem2  25506  ivthlem3  25507  ivth2  25509  ivthle  25510  ivthle2  25511  ivthicc  25512  ovolficcss  25523  ovolunlem1a  25550  ovolunlem1  25551  ovolfiniun  25555  ovoliunlem1  25556  ovoliunlem3  25558  ovoliun  25559  ovoliun2  25560  shft2rab  25562  ovolshftlem1  25563  sca2rab  25566  ovolscalem1  25567  mblsplit  25586  finiunmbl  25598  volun  25599  volfiniun  25601  voliunlem1  25604  voliunlem3  25606  iunmbl  25607  voliun  25608  volsup  25610  ioombl  25619  ioorcl  25631  vitalilem1  25662  vitalilem2  25663  vitalilem3  25664  vitalilem4  25665  vitali  25667  ismbf1  25678  mbfdm  25680  ismbf  25682  ismbfcn  25683  mbfima  25684  mbfimaicc  25685  ismbfcn2  25692  ismbfd  25693  ismbf2d  25694  mbfeqalem1  25695  mbfmax  25703  mbfposr  25706  mbfposb  25707  ismbf3d  25708  mbfimaopnlem  25709  mbfimaopn2  25711  cncombf  25712  isi1f  25728  i1fd  25735  itg1mulc  25759  mbfi1fseqlem4  25773  itg2lcl  25782  isibl  25820  iblitg  25823  iblcnlem1  25843  iblcnlem  25844  iblrelem  25846  iblpos  25848  itgeqa  25869  itgfsum  25882  itgabs  25890  limcvallem  25926  ellimc  25928  ellimc2  25932  limcmpt  25938  cnmptlimc  25945  dvbsss  25957  cpnfval  25988  elcpn  25990  dvmptfsum  26033  dvle  26066  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  dvfsumrlimf  26085  dvfsumlem1  26086  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsumrlimge0  26091  dvfsumrlim  26092  dvfsumrlim2  26093  dvfsum2  26095  itgsubstlem  26109  itgsubst  26110  mdegcl  26128  deg1nn0clb  26149  isuc1p  26200  plyeq0lem  26269  plyco  26300  plycj  26337  dvply2g  26344  dvnply2  26347  plydivlem4  26356  fta1lem  26367  fta1  26368  elqaalem1  26379  elqaalem2  26380  elqaalem3  26381  elqaa  26382  ulmcau  26456  radcnv0  26477  radcnvlt1  26479  radcnvle  26481  pserdvlem2  26490  coseq1  26585  efeq1  26588  sinord  26594  efif1olem2  26603  efif1olem4  26605  lognegb  26650  logcj  26666  argimgt0  26672  logtayl  26720  2irrexpq  26791  root1eq1  26816  logrec  26824  2irrexpqALT  26861  angrteqvd  26867  angpieqvdlem  26889  atans  26991  atans2  26992  dmarea  27018  areambl  27019  rlimcnp  27026  rlimcnp2  27027  xrlimcnp  27029  harmonicbnd  27065  harmonicbnd2  27066  lgamcvglem  27101  wilthlem2  27130  wilth  27132  efnnfsumcl  27164  vmacl  27179  efvmacl  27181  efchtdvds  27220  sqff1o  27243  fsumdvdscom  27246  musumsum  27253  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  fsumvma  27275  perfect  27293  dchrelbasd  27301  lgsval  27363  lgsval2lem  27369  lgsdir2lem4  27390  lgsdir2  27392  lgsqrlem1  27408  lgsdchr  27417  m1lgs  27450  2lgs  27469  mul2sq  27481  2sqlem6  27485  2sqblem  27493  2sq2  27495  rplogsumlem2  27547  dchrisumlema  27550  dchrisumlem2  27552  dchrisumlem3  27553  dchrvmasumlem2  27560  dchrvmasumlem3  27561  dchrisum0flblem2  27571  dchrisum0flb  27572  dchrisum0fno1  27573  ostthlem1  27689  nodmon  27713  noextendseq  27730  nodense  27755  madefi  27968  addsproplem1  28020  addsproplem3  28022  addsprop  28027  addsf  28033  addsbdaylem  28067  negsproplem1  28078  negsproplem3  28080  negsprop  28085  negsbdaylem  28106  mulsproplemcbv  28159  mulsproplem1  28160  mulsproplem10  28169  mulsprop  28174  noseqp1  28315  noseqind  28316  peano5n0s  28342  dfn0s2  28354  n0addscl  28365  n0mulscl  28366  n0sbday  28372  n0s0m1  28377  n0subs  28378  n0p1nns  28379  dfnns2  28380  zaddscl  28398  zmulscld  28401  elzn0s  28402  peano5uzs  28408  expscl  28431  pw2bday  28436  zs12bday  28442  mirval  28681  perpneq  28740  isperp2  28741  isperp2d  28742  foot  28748  islnopp  28765  islnoppd  28766  outpasch  28781  hlpasch  28782  ishpg  28785  colopp  28795  colhp  28796  lmif  28811  islmib  28813  lmiinv  28818  trgcopy  28830  trgcopyeu  28832  acopyeu  28860  inaghl  28871  tgasa1  28884  f1otrgitv  28896  f1otrg  28897  isfusgr  29353  opfusgr  29358  fusgrfisbase  29363  fusgrfisstep  29364  nbupgrel  29380  nbumgrvtx  29381  nbusgreledg  29388  edgnbusgreu  29402  nb3grprlem1  29415  uvtxusgrel  29438  cusgredg  29459  cplgr2vpr  29468  cusgrexg  29479  usgredgsscusgredg  29495  fusgrn0degnn0  29535  rusgrnumwrdl2  29622  rgrx0ndm  29629  wlkcomp  29667  wlkdlem2  29719  clwlkcomp  29815  iswwlks  29869  wwlknllvtx  29879  0enwwlksnge1  29897  wlkiswwlks2lem5  29906  wwlksm1edg  29914  wwlksnred  29925  wwlksnext  29926  wwlksnextbi  29927  wwlksnredwwlkn  29928  wwlksnextfun  29931  wwlksnextinj  29932  wwlksnextsurj  29933  wwlksnextbij  29935  wwlksnfi  29939  wwlksnextproplem2  29943  wwlksnextprop  29945  2wlkdlem4  29961  rusgrnumwwlkl1  30001  rusgrnumwwlks  30007  isclwwlk  30016  clwwlk1loop  30020  clwwlkccatlem  30021  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlklem3  30033  clwlkclwwlk  30034  clwlkclwwlk2  30035  clwwisshclwwslemlem  30045  clwwisshclwwslem  30046  clwwisshclwws  30047  clwwlknlbonbgr1  30071  clwwlkinwwlk  30072  clwwlkn1  30073  loopclwwlkn1b  30074  clwwlkn1loopb  30075  clwwlkn2  30076  clwwlkel  30078  clwwlkf  30079  clwwlkwwlksb  30086  clwwlkext2edg  30088  wwlksext2clwwlk  30089  wwlksubclwwlk  30090  eleclclwwlknlem2  30093  umgr2cwwk2dif  30096  s2elclwwlknon2  30136  clwwlknonwwlknonb  30138  clwwlknonex2lem2  30140  clwwlknonex2  30141  3wlkdlem4  30194  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eupth2lem2  30251  eulerpathpr  30272  1vwmgr  30308  3vfriswmgrlem  30309  3vfriswmgr  30310  3cyclfrgrrn1  30317  vdgn1frgrv2  30328  frgrncvvdeqlem3  30333  frgrncvvdeqlem8  30338  frgrncvvdeqlem9  30339  frgrwopregasn  30348  frgrwopregbsn  30349  frgrwopreglem5ALT  30354  frgr2wwlk1  30361  frgr2wwlkeqm  30363  fusgr2wsp2nb  30366  2clwwlk2clwwlklem  30378  extwwlkfabel  30385  nvvop  30641  isnvlem  30642  sspval  30755  nmorepnf  30800  phpar  30856  siilem2  30884  bnsscmcl  30900  ubthlem1  30902  shaddcl  31249  shmulcl  31250  hsn0elch  31280  hhssablo  31295  hhssnvt  31297  hhsssh  31301  shscl  31350  shintcl  31362  chintcl  31364  shincl  31413  chincl  31531  h1datomi  31613  chscllem2  31670  sumspansn  31681  spansncvi  31684  5oalem2  31687  5oalem3  31688  pjini  31731  pjjsi  31732  eigposi  31868  nmoprepnf  31899  nmfnrepnf  31912  dmadjrnb  31938  lnophmlem1  32048  lnophm  32051  nmcopex  32061  lnconi  32065  nmbdfnlb  32082  nmcfnex  32085  imaelshi  32090  rnbra  32139  leopg  32154  pjbdlni  32181  pjhmop  32182  hmopidmch  32185  pjclem4  32231  pj3si  32239  strlem1  32282  atssma  32410  atcv0eq  32411  atcv1  32412  atomli  32414  atcvatlem  32417  cdj3lem2a  32468  cdj3lem3a  32471  xppreima  32664  fmptcof2  32675  aciunf1lem  32680  funcnv4mpt  32687  1stpreimas  32717  f1od2  32735  fpwrelmapffslem  32746  xrofsup  32774  fzspl  32795  fzsplit3  32799  nnindf  32823  fprodex01  32829  fsumiunle  32833  gsumhashmul  33040  fzto1st  33096  isslmd  33181  slmdlema  33182  qusker  33342  0nellinds  33363  unitprodclb  33382  nsgmgclem  33404  nsgmgc  33405  nsgqusf1olem2  33407  elrspunidl  33421  prmidlval  33430  prmidlc  33441  opprlidlabs  33478  dfufd2lem  33542  lindsunlem  33637  brfldext  33660  brfinext  33666  finexttrb  33675  extdg1id  33676  constrconj  33735  constrfin  33736  smatrcl  33742  submateq  33755  lmatfval  33760  lmatcl  33762  qtophaus  33782  locfinreflem  33786  locfinref  33787  zartopn  33821  zarcmplem  33827  rhmpreimacnlem  33830  xpinpreima  33852  xpinpreima2  33853  cnre2csqlem  33856  tpr2rico  33858  prsdm  33860  prsrn  33861  ordtrest2NEWlem  33868  ordtrest2NEW  33869  qqhval2  33928  isrrext  33946  ismntoplly  33971  indfval  33980  indf1ofs  33990  esumcvg  34050  sigaval  34075  issiga  34076  0elsiga  34078  sigaclcu  34081  issgon  34087  prsiga  34095  sigaclci  34096  difelsiga  34097  unelsiga  34098  ispisys2  34117  inelpisys  34118  unelldsys  34122  sigapildsyslem  34125  sigapildsys  34126  ldgenpisyslem1  34127  ldgenpisys  34130  isros  34132  unelros  34135  difelros  34136  fiunelros  34138  inelsros  34142  diffiunisros  34143  rossros  34144  measvuni  34178  measiun  34182  voliune  34193  volfiniune  34194  brfae  34212  ismbfm  34215  mbfmcnvima  34220  mbfmcst  34224  1stmbfm  34225  2ndmbfm  34226  imambfm  34227  sitgval  34297  issibf  34298  sibfima  34303  sitgfval  34306  sitgclg  34307  eulerpartlemelr  34322  eulerpartlemsf  34324  eulerpartleme  34328  eulerpartlemt0  34334  eulerpartlemt  34336  eulerpartgbij  34337  eulerpartlemr  34339  eulerpartlemmf  34340  eulerpartlemgvv  34341  eulerpartlemgs2  34345  eulerpartlemn  34346  eulerpart  34347  cndprobprob  34403  rrvsum  34419  orvcelel  34434  ballotlemodife  34462  ballotlemsdom  34476  ballotlemrv  34484  ballotlemrv1  34485  ballotlemrv2  34486  ballotlem1ri  34499  fsum2dsub  34584  reprinfz1  34599  reprpmtf1o  34603  reprdifc  34604  breprexplema  34607  hgt750lema  34634  hgt750leme  34635  bnj149  34851  bnj222  34859  bnj1112  34959  bnj1148  34972  fineqvrep  35071  gblacfnacd  35075  loop1cycl  35105  subfacp1lem3  35150  subfacp1lem6  35153  erdszelem10  35168  kur14  35184  cvxsconn  35211  cnllysconn  35213  resconn  35214  iscvm  35227  cvmliftlem5  35257  cvmliftlem15  35266  cvmlift2lem1  35270  cvmlift2lem12  35282  cvmlift2lem13  35283  sat1el2xp  35347  fmlasuc  35354  gonan0  35360  gonar  35363  satefvfmla0  35386  msubrn  35497  msubco  35499  ismfs  35517  mvtinf  35523  mclsax  35537  mppspstlem  35539  elmpps  35541  nnuni  35689  dfdm5  35736  dfrn5  35737  elima4  35739  rdgprc0  35757  pprodss4v  35848  elfuns  35879  fnimage  35893  imageval  35894  fwddifval  36126  fwddifnval  36127  fwddifnp1  36129  elhf2g  36140  hfun  36142  hfninf  36150  filnetlem4  36347  onsucconn  36404  onsucsuccmp  36410  limsucncmp  36412  onint1  36415  fveleq  36417  findreccl  36419  nndivsub  36423  weiunse  36434  bj-seex  36888  bj-adjg1  37009  bj-mooreset  37068  bj-ismoored0  37072  bj-ismoored  37073  bj-inftyexpitaudisj  37171  bj-inftyexpidisj  37176  bj-isvec  37253  bj-isclm  37257  csbmpo123  37297  topdifinffinlem  37313  topdifinffin  37314  csbfinxpg  37354  phpreu  37564  finixpnum  37565  lindsenlbs  37575  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem28  37608  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  poimir  37613  mblfinlem3  37619  ex-ovoliunnfl  37623  voliunnfl  37624  volsupnfl  37625  mbfresfi  37626  itgabsnc  37649  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  dvasin  37664  sdclem2  37702  fdc  37705  incsequz  37708  neificl  37713  mettrifi  37717  cntotbnd  37756  cnpwstotbnd  37757  ismtyima  37763  ismtyhmeolem  37764  heiborlem2  37772  heiborlem3  37773  heiborlem4  37774  heiborlem5  37775  heiborlem6  37776  heiborlem10  37780  isrngo  37857  isdivrngo  37910  drngoi  37911  idlval  37973  isidlc  37975  idladdcl  37979  idllmulcl  37980  idlrmulcl  37981  0idl  37985  pridlval  37993  smprngopr  38012  prnc  38027  ispridlc  38030  pridlc  38031  eqrelf  38211  ecex2  38284  imaexALTV  38286  iss2  38300  elcoeleqvrels  38551  elfunsALTV  38648  eldisjs  38678  eleldisjs  38684  fsumshftd  38908  riotaclbgBAD  38910  renegclALT  38919  lshpinN  38945  isopos  39136  oposlem  39138  glbconN  39333  glbconNOLD  39334  lnnat  39384  2at0mat0  39482  islvol2aN  39549  dalawlem13  39840  pclfinclN  39907  lhpoc2N  39972  ltrncnvatb  40095  cdleme11h  40223  cdlemefr32sn2aw  40361  cdlemefs32sn1aw  40371  cdleme32fvaw  40396  cdlemg1fvawlemN  40530  dicelvalN  41135  dih1dimatlem  41286  dihlatat  41294  dihjatcclem4  41378  islpolN  41440  lpolsatN  41445  lpolpolsatN  41446  mapdordlem1a  41591  mapdordlem1  41593  mapdhcl  41684  iscsrg  41925  fzsplitnd  41939  lcmineqlem12  41997  intlewftc  42018  dvrelogpow2b  42025  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  dvle2  42029  aks4d1p8  42044  aks4d1p9  42045  isprimroot  42050  primrootsunit1  42054  primrootscoprmpow  42056  aks6d1c1p1  42064  aks6d1c1p2  42066  aks6d1c1p3  42067  evl1gprodd  42074  hashscontpow  42079  aks6d1c3  42080  aks6d1c2  42087  sticksstones1  42103  sticksstones10  42112  sticksstones11  42113  sticksstones12a  42114  aks6d1c6lem1  42127  unitscyglem5  42156  metakunt26  42187  metakunt29  42190  metakunt30  42191  metakunt32  42193  retire  42308  reelznn0nn  42425  fsuppind  42545  fsuppssindlem2  42547  fsuppssind  42548  isnacs3  42666  nacsfix  42668  mzpclval  42681  mzpcl1  42685  mzpcl2  42686  mzpcl34  42687  mzpexpmpt  42701  mzpsubst  42704  diophin  42728  diophun  42729  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  rabdiophlem2  42758  diophren  42769  fphpd  42772  fphpdo  42773  fiphp3d  42775  pellexlem1  42785  pell14qrexpclnn0  42822  pellqrex  42835  rmspecnonsq  42863  monotuz  42898  monotoddzzfi  42899  monotoddzz  42900  oddcomabszz  42901  modabsdifz  42943  rmxdioph  42973  expdiophlem2  42979  limsuc2  42998  dfac11  43019  kelac1  43020  dfac21  43023  lsmfgcl  43031  islnm  43034  lnmlssfg  43037  lmhmfgima  43041  pwslnm  43051  unxpwdom3  43052  pwfi2f1o  43053  islnr  43068  hbtlem2  43081  cnsrexpcl  43122  flcidc  43131  mendlmod  43150  proot1ex  43157  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  44201  dvgrat  44281  cvgdvgrat  44282  radcnvrat  44283  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  fnchoice  44929  fiiuncl  44967  disjf1  45090  disjinfi  45099  choicefi  45107  axccdom  45129  fmptf  45147  fmptff  45179  monoords  45212  supminfrnmpt  45360  supxrleubrnmptf  45366  supminfxr  45379  supminfxr2  45384  supminfxrrnmpt  45386  monoordxrv  45397  monoordxr  45398  monoord2xrv  45399  monoord2xr  45400  caucvgbf  45405  cvgcaule  45407  fsummulc1f  45492  fsumnncl  45493  fsumf1of  45495  fsumreclf  45497  fsumlessf  45498  fsumsermpt  45500  fmul01  45501  fmulcl  45502  fmuldfeqlem1  45503  fmuldfeq  45504  fmul01lt1lem1  45505  fmul01lt1lem2  45506  fprodexp  45515  fprodabs2  45516  mccllem  45518  mccl  45519  fprodcnlem  45520  fprodcn  45521  climmulf  45525  climsuse  45529  climrecf  45530  climaddf  45536  climf  45543  sumnnodd  45551  clim2f  45557  0ellimcdiv  45570  climsubmpt  45581  climreclf  45585  climf2  45587  fnlimcnv  45588  climeldmeqmpt  45589  clim2f2  45591  climfveqmpt  45592  fnlimfvre  45595  fnlimabslt  45600  climfveqmpt3  45603  climbddf  45608  climeldmeqmpt3  45610  climinf2mpt  45635  climinfmpt  45636  limsupequzmptf  45652  lmbr3  45668  liminfreuzlem  45723  coseq0  45785  cncfshift  45795  cncfperiod  45800  fprodcncf  45821  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvmptmulf  45858  dvnmptdivc  45859  dvnmul  45864  dvmptfprod  45866  iblspltprt  45894  itgspltprt  45900  stoweidlem2  45923  stoweidlem3  45924  stoweidlem4  45925  stoweidlem6  45927  stoweidlem8  45929  stoweidlem17  45938  stoweidlem19  45940  stoweidlem20  45941  stoweidlem21  45942  stoweidlem23  45944  stoweidlem27  45948  stoweidlem35  45956  stoweidlem42  45963  stoweidlem43  45964  stoweidlem62  45983  stoweid  45984  wallispilem3  45988  wallispi  45991  fourierdlem16  46044  fourierdlem21  46049  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem51  46078  fourierdlem54  46081  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem71  46098  fourierdlem72  46099  fourierdlem73  46100  fourierdlem83  46110  fourierdlem86  46113  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem100  46127  fourierdlem103  46130  fourierdlem104  46131  fourierdlem105  46132  fourierdlem108  46135  fourierdlem109  46136  fourierdlem110  46137  fourierdlem112  46139  fourierdlem113  46140  etransclem24  46179  salunicl  46237  saluncl  46238  saldifcl  46240  sge0f1o  46303  sge0lempt  46331  sge0iunmptlemfi  46334  sge0p1  46335  sge0fodjrnlem  46337  sge0iunmpt  46339  sge0ltfirpmpt2  46347  sge0isummpt2  46353  sge0xaddlem2  46355  sge0xadd  46356  ismea  46372  nnfoctbdjlem  46376  nnfoctbdj  46377  meadjiun  46387  voliunsge0lem  46393  meaiuninclem  46401  meaiuninc3v  46405  hoidmvlelem2  46517  hoidmvlelem3  46518  vonvolmbl2  46584  hoimbl2  46586  vonhoire  46593  vonicclem2  46605  vonn0ioo2  46611  vonn0icc2  46613  salpreimagelt  46628  salpreimalegt  46630  salpreimagtge  46646  salpreimaltle  46647  issmf  46649  salpreimagtlt  46651  smfpreimalt  46652  smfpreimaltf  46657  issmfle  46666  smfpreimale  46675  issmfgt  46677  smfpreimagt  46683  issmfgelem  46690  issmfge  46691  smflimlem4  46695  smflim  46698  smfpreimage  46703  smfresal  46709  smfpimbor1lem1  46719  smfpimbor1lem2  46720  smflim2  46727  smflimmpt  46731  smflimsuplem1  46741  smflimsuplem2  46742  smflimsuplem3  46743  smflimsuplem5  46745  smflimsuplem7  46747  smflimsup  46749  smfliminf  46752  eu2ndop1stv  47040  dmfcoafv  47090  ffnaov  47114  faovcl  47115  funressndmafv2rn  47138  dfatdmfcoafv2  47169  smonoord  47245  iccpartiltu  47296  iccpartigtl  47297  sprsymrelf1lem  47365  prproropf1olem2  47378  fmtno4prmfac193  47447  proththdlem  47487  proththd  47488  iseven  47502  isodd  47503  dfodd2  47510  evenm1odd  47513  evenp1odd  47514  enege  47519  onego  47520  epee  47579  perfectALTV  47597  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  clnbupgrel  47707  edgusgrclnbfin  47714  isuspgrim0  47756  uspgrimprop  47757  isuspgrimlem  47758  grimuhgr  47762  grimedg  47787  grtriproplem  47790  grtrif1o  47793  isgrtri  47794  grtriclwlk3  47796  grimgrtri  47798  usgrgrtrirex  47799  grlimgrtri  47820  usgrexmpl1tri  47840  uzlidlring  47958  cbvmpox2  48060  lmod1  48221  nnolog2flm1  48324  dignn0flhalflem1  48349  catprsc  48680  isthincd2lem2  48703