Theorem eleq1d 2824

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

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

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

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

This theorem is referenced by:  eleq1  2827  eleq12d  2833  eqeltrd  2839  eqneltrd  2859  rspcimdv  3550  reuind  3694  sbcel2  4347  sbccsb2  4366  disjiun  5061  breq1  5076  breq2  5077  axrep6g  5213  inex1g  5248  intex  5273  pwexg  5308  reusv2lem4  5331  reusv2  5333  reusv3  5335  rabxfrd  5347  prexOLD  5373  opelopabsb  5473  csbmpt12  5500  pofun  5545  seex  5578  seinxp  5703  opabid2  5772  opeliunxp2  5781  elrn2g  5833  opeldmd  5849  opeldm  5850  elreldm  5878  elsnres  5974  iss  5988  unielrel  6226  onunel  6418  funopg  6520  brprcneu  6818  brprcneuALT  6819  tz6.12f  6853  ndmfvrcl  6861  ssimaex  6913  dmfco  6924  fvmpti  6935  fvmpt3  6941  fvmptf  6958  fvmptss2  6963  respreima  7008  fvn0ssdmfun  7016  fvelrn  7018  ffnfvf  7062  ffvresb  7068  fmptco  7072  fmptcof  7073  fsn  7078  fsn2g  7081  fressnfv  7104  fvrnressn  7105  fnex  7162  funfvima  7175  funfvima3  7181  f1mpt  7206  fliftfuns  7259  isoselem  7286  isowe2  7295  riotaclb  7355  ovrspc2v  7383  ffnov  7483  fovcld  7484  ovmpos  7505  ov2gf  7506  ovg  7522  funimassov  7534  oprssdm  7538  ndmovrcl  7543  caovclg  7549  elovmpo  7602  ofmpteq  7644  sorpsscmpl  7678  uniexg  7684  unexbOLD  7692  abnexg  7700  difsnexi  7705  onint  7734  limsuc  7790  tfisi  7800  peano5  7834  xpexr  7859  xpexcnv  7861  fnexALT  7894  focdmex  7899  f1stres  7956  f2ndres  7957  xp1st  7964  xp2nd  7965  unielxp  7970  opiota  8002  fmpox  8010  offval22  8028  frxp  8067  fnse  8074  frxp2  8085  sexp2  8087  frxp3  8092  sexp3  8094  opeliunxp2f  8151  dftpos4  8186  fvmpocurryd  8212  undefnel2  8218  onnseq  8275  smoel  8291  smo11  8295  tfrlem8  8314  tfrlem9  8315  tfrlem15  8322  tfr2b  8326  tz7.44-2  8337  tz7.44-3  8338  oacl  8461  omcl  8462  oecl  8463  oaord1  8477  omordi  8492  oen0  8513  oeeui  8529  nnacl  8538  nnmcl  8539  nnecl  8540  nnmordi  8558  nnaordex  8565  omsmolem  8584  naddcllem  8603  naddov2  8606  naddf  8608  naddssim  8612  naddelim  8613  naddasslem1  8621  naddasslem2  8622  naddsuc2  8628  erexb  8660  elecex  8685  qliftfuns  8742  ixpsnval  8839  elixp2  8840  resixp  8872  undifixp  8873  mptelixpg  8874  resixpfo  8875  elixpsn  8876  fundmen  8969  fopwdom  9014  disjen  9063  xpf1o  9068  unfi  9096  cnvfi  9101  fnfi  9103  f1oenfirn  9105  f1domfi  9106  unblem2  9194  imafiOLD  9217  pwfi  9220  fiint  9228  iunfi  9244  tfsnfin2  9264  isfsupp  9269  fsuppun  9291  ffsuppbi  9302  elfi2  9318  wdom2d  9486  ixpiunwdom  9496  dfom3  9560  cantnfvalf  9578  cantnflt  9585  cantnflem1  9602  r1fin  9689  tz9.12lem3  9705  ranksnb  9743  ranklim  9760  r1pw  9761  r1pwALT  9762  r1pwcl  9763  rankuni2b  9769  djuexb  9825  cardmin2  9915  infxpenc2lem1  9933  dfac8alem  9943  dfac8clem  9946  ac5num  9950  acni2  9960  acnlem  9962  alephon  9983  alephfplem3  10020  alephfplem4  10021  dfac4  10036  dfac5lem1  10037  dfac5lem5  10041  dfac2a  10044  dfac2b  10045  dfacacn  10056  dfac12lem2  10059  dfac12r  10061  dfac12k  10062  cofsmo  10183  cfsmolem  10184  isfin1a  10206  fin1ai  10207  isfin3  10210  infpssrlem3  10219  fin23lem7  10230  fin23lem11  10231  enfin2i  10235  isf34lem4  10291  fin1a2lem7  10320  hsmexlem9  10339  hsmexlem4  10343  hsmex  10346  axcc2lem  10350  axcc3  10352  axdc3lem2  10365  axcclem  10371  zornn0g  10419  ttukeylem3  10425  ttukeylem6  10428  ttukey2g  10430  brdom7disj  10445  brdom6disj  10446  fnct  10451  konigthlem  10483  axregndlem2  10518  axinfnd  10521  axacndlem5  10526  axacnd  10527  fpwwe2lem4  10549  fpwwe2lem12  10557  fpwwe  10561  pwfseqlem1  10573  pwfseqlem3  10575  pwfseqlem4a  10576  pwfseqlem4  10577  wununi  10621  wunpw  10622  wunpr  10624  wunr1om  10634  tskpw  10668  tskr1om  10682  inar1  10690  grupw  10710  grupr  10712  gruurn  10713  gruiun  10714  ingru  10730  grur1a  10734  grothomex  10744  grothac  10745  addnidpi  10816  indpi  10822  adderpq  10871  mulerpq  10872  addclprlem2  10932  mulclprlem  10934  distrlem4pr  10941  prlem934  10948  ltexprlem3  10953  ltexprlem4  10954  ltexprlem7  10957  ltexpri  10958  prlem936  10962  reclem2pr  10963  reclem3pr  10964  addclsr  10998  mulclsr  10999  supsrlem  11026  supsr  11027  axaddf  11060  axmulf  11061  axaddrcl  11067  axmulrcl  11069  renegcl  11449  negreb  11451  negn0  11571  negf1o  11572  ltord1  11668  leord1  11669  eqord1  11670  ltord2  11671  leord2  11672  eqord2  11673  negfi  12097  infm3  12107  cju  12147  indfval  12158  peano5nni  12169  peano2nn  12178  dfnn2  12179  nn1m1nn  12187  nnaddcl  12189  nnmulcl  12190  nnsub  12213  nndivtr  12216  un0addcl  12462  un0mulcl  12463  elnnnn0  12472  nn0sub  12479  fcdmnn0fsuppg  12489  elz  12518  nnnegz  12519  elz2  12534  znegclb  12556  zaddcl  12559  nzadd  12567  zmulcl  12568  zneo  12604  nneo  12605  zeo  12607  peano5uzi  12610  zindd  12622  uzp1  12817  uzaddcl  12846  ublbneg  12875  eqreznegel  12876  supminf  12877  zsupss  12879  qmulz  12893  qnegcl  12908  irradd  12915  irrmul  12916  xnn0xaddcl  13179  fzrev2  13534  injresinjlem  13737  negmod0  13829  om2uzuzi  13903  uzindi  13936  fsuppmapnn0ub  13949  mptnn0fsuppr  13953  seqexw  13971  seqcl2  13974  seqcl  13976  seqf  13977  monoord  13986  monoord2  13987  sermono  13988  seqsplit  13989  seqcaopr2  13992  seqid3  14000  seqhomo  14003  expcllem  14026  expcl2lem  14027  m1expcl2  14039  faccl  14237  facdiv  14241  facndiv  14242  bccmpl  14263  bccl  14276  hashclb  14312  hasheq0  14317  hashfn  14329  seqcoll  14418  opfi1uzind  14465  ccatalpha  14548  reuccatpfxs1lem  14700  reuccatpfxs1  14701  repswccat  14740  repswrevw  14741  2cshw  14767  2cshwcshw  14779  cshimadifsn  14783  cshco  14790  swrd2lsw  14906  wwlktovf  14910  wwlktovf1  14911  wwlktovfo  14912  wrd2f1tovbij  14914  shftlem  15022  shftf  15033  cjval  15056  cjth  15057  remim  15071  cnpart  15194  uzin2  15299  caubnd2  15312  sqreulem  15314  clim  15448  clim2  15458  lo1o12  15487  climrlim2  15501  lo1resb  15518  o1resb  15520  lo1eq  15522  climmpt2  15527  climshftlem  15528  rlimcld2  15532  climcn1  15546  climcn2  15547  o1dif  15584  iserex  15611  climub  15616  climserle  15617  isercoll  15622  climcau  15625  caurcvg2  15632  caucvgb  15634  summolem3  15668  summolem2a  15669  zsum  15672  fsum  15674  sumss2  15680  fsumcvg2  15681  fsumclf  15692  fsumsplitf  15696  fsumsplit1  15699  sumpr  15702  sumtp  15703  fsumm1  15705  fsum1p  15707  isummulc2  15716  fsum2dlem  15724  fsumcom2  15728  fsumshftm  15735  fsum0diag2  15737  fsumge1  15752  fsum00  15753  fsumabs  15756  telfsumo  15757  telfsumo2  15758  fsumparts  15761  fsumrlim  15766  fsumo1  15767  o1fsum  15768  fsumiun  15776  binomlem  15786  isumshft  15796  isum1p  15798  isumrpcl  15800  climcndslem1  15806  climcndslem2  15807  climcnds  15808  infcvgaux2i  15815  cvgrat  15840  mertens  15843  clim2prod  15845  prodfn0  15851  prodfrec  15852  prodfdiv  15853  ntrivcvgfvn0  15856  prodmolem3  15890  prodmolem2a  15891  zprod  15894  fprod  15898  prodss  15904  fprodser  15906  fprodm1  15924  fprod1p  15925  fprodm1s  15927  fprodp1s  15928  fprodabs  15931  fprodn0  15936  fprod2dlem  15937  fprodcnv  15940  fprodcom2  15941  fproddivf  15944  fprodsplitf  15945  fprodsplit1f  15947  bpolycl  16009  fprodefsum  16052  rpnnen2lem11  16183  mod2eq1n2dvds  16308  mulsucdiv2z  16314  zob  16320  nn0o1gt2  16342  nno  16343  nn0o  16344  divalglem7  16360  bitsf1  16407  sadcp1  16416  smupp1  16441  qnumdencl  16701  iserodd  16798  pcqcl  16819  pcxnn0cl  16823  pcxcl  16824  pcgcd1  16840  dvdsprmpweqle  16849  pcmpt  16855  pcmpt2  16856  pcmptdvds  16857  infpnlem2  16874  infpn2  16876  1arith  16890  elgz  16894  mul4sq  16917  4sqlem13  16920  4sqlem17  16924  4sqlem18  16925  4sqlem19  16926  vdwlem1  16944  vdwlem2  16945  vdwnn  16961  ramtcl2  16974  ramcl  16992  prmonn2  17002  prmodvdslcmf  17010  isstruct2  17111  wunress  17211  firest  17387  imasaddfnlem  17484  imasvscafn  17493  xpsfrnel2  17520  mreintcl  17549  ismred2  17557  mreexexlemd  17602  mreexexlem3d  17604  mreexexlem4d  17605  iscatd2  17639  catpropd  17667  subsubc  17812  isfunc  17823  inclfusubc  17902  fncnvimaeqv  18078  joindef  18332  joinval  18333  meetdef  18346  meetval  18347  oduclatb  18465  acsdrsel  18501  isacs4lem  18502  isacs5lem  18503  acsdrscl  18504  mgmsscl  18605  mgmpropd  18611  mgm1  18618  gsumvalx  18636  issubmgm  18662  issubmgm2  18663  mgmhmima  18675  sgrppropd  18691  mndpropd  18719  issubm  18763  0subm  18777  insubm  18778  mhmimalem  18784  gsumwsubmcl  18797  gsumwspan  18806  symggrplem  18844  sursubmefmnd  18856  injsubmefmnd  18857  smndex1basss  18868  mulgsubcl  19056  issubg  19094  issubg2  19109  issubg4  19113  0subg  19119  isnsg  19122  isnsg2  19123  nsgbi  19124  isnsg3  19127  elnmz  19130  nmzbi  19131  nmzsubg  19132  eqgval  19144  eqgid  19147  cycsubgcl  19173  ghmrn  19196  ghmnsgima  19207  gass  19268  oppgsubg  19330  f1omvdconj  19413  symgfisg  19435  psgneldm  19470  0subgALT  19535  odhash3  19543  sylow2blem2  19588  lsmsubm  19620  lsmsubg  19621  efgsf  19696  efgsdm  19697  efgs1b  19703  efgredlema  19707  eqgabl  19801  ablnsg  19814  cyggenod2  19852  gsumzaddlem  19888  gsummhm2  19906  gsum2dlem2  19938  gsum2d2lem  19940  gsumcom2  19942  dprdfeq0  19991  dprdsubg  19993  dprd2da  20011  ablfacrp  20035  pgpfac1lem3  20046  pgpfaclem1  20050  ablfaclem3  20056  ablfac2  20058  cycsubggenodd  20078  isrng  20127  issrg  20161  srgfcl  20169  rglcom4d  20184  srgbinomlem4  20202  isring  20210  iscrng  20213  dvdsr  20334  irredrmul  20399  isrngim  20417  isrim0  20454  issubrng  20520  subrngringnsg  20526  issubrng2  20531  rhmimasubrnglem  20538  issubrg  20544  issubrg2  20565  subrgpropd  20581  isdrngd  20738  isdrngdOLD  20740  issdrg  20761  sdrgacs  20774  issrngd  20828  islmod  20855  lmodlema  20856  islmodd  20857  lmodprop2d  20915  rmodislmodlem  20920  rmodislmod  20921  lssset  20924  islssd  20926  lsscl  20933  lsslss  20952  lsspropd  21008  lmhmima  21038  lbsind  21071  lsmcl  21074  islvec  21095  lmhmlvec  21101  lspsolvlem  21136  lspsolv  21137  lvecpropd  21161  rnglidlmcl  21210  rnglidl0  21223  rnglidlmmgm  21239  rngqiprngimf1lem  21288  rngqiprngimf1  21294  ring2idlqus  21303  xrsdsreclblem  21389  xrsdsreclb  21390  cnsubrglem  21393  prmirred  21450  pzriprnglem4  21460  pzriprnglem8  21464  pzriprngALT  21471  znunithash  21540  cofipsgn  21569  zrhpsgnelbas  21570  rzgrp  21599  isphl  21604  phllmhm  21608  ipcl  21609  isphld  21630  phlpropd  21631  phlssphl  21635  cssincl  21664  pjdm  21683  dsmmval  21710  dsmmbas2  21713  dsmmelbas  21715  frlmbas  21731  frlmup1  21774  lindfind  21792  lindsind  21793  f1lindf  21798  islindf4  21814  psrbag  21893  psrbaglefi  21902  mplsubglem  21974  mpllsslem  21975  ltbwe  22021  psrbagsn  22040  subrgasclcl  22044  mplind  22047  mpfind  22092  psdmul  22155  coe1mul2lem2  22255  gsumply1eq  22296  evl1vsd  22331  mpfpf1  22338  pf1mpf  22339  pf1ind  22342  matecl  22409  m1detdiag  22581  mdetralt  22592  mdetralt2  22593  mdetunilem2  22597  mdetunilem9  22604  m2detleiblem3  22613  m2detleiblem4  22614  smadiadetlem0  22645  cpmatacl  22700  chpscmat  22826  uniopn  22881  inopn  22883  fiinopn  22885  istps  22918  fctop  22988  iscld  23011  isopn2  23016  mretopd  23076  iscldtop  23079  perfi  23139  tgrest  23143  restcld  23156  ordtbaslem  23172  ordtrest2lem  23187  ordtrest2  23188  iscn  23219  cnpval  23220  iscnp  23221  tgcn  23236  subbascn  23238  ssidcn  23239  lmbrf  23244  cnpnei  23248  cnima  23249  iscncl  23253  cnconst2  23267  cnrest2  23270  cnpresti  23272  cnprest  23273  cnindis  23276  lmres  23284  lmcnp  23288  iscnrm  23307  t1sncld  23310  cnrmi  23344  cncmp  23376  cmpsublem  23383  fiuncmp  23388  unconn  23413  conncompid  23415  conncompconn  23416  conncompss  23417  1stcfb  23429  2ndcrest  23438  2ndcctbss  23439  2ndcdisj  23440  1stccnp  23446  islly  23452  isnlly  23453  subislly  23465  restnlly  23466  restlly  23467  islly2  23468  hausllycmp  23478  cldllycmp  23479  dislly  23481  isptfin  23500  islocfin  23501  ptfinfin  23503  finlocfin  23504  dissnlocfin  23513  locfindis  23514  comppfsc  23516  kgenval  23519  elkgen  23520  kgeni  23521  cmpkgen  23535  1stckgenlem  23537  kgencn2  23541  ptpjpre1  23555  elpt  23556  elptr  23557  ptbasin  23561  xkobval  23570  xkoval  23571  xkoopn  23573  txbasval  23590  tx1cn  23593  tx2cn  23594  dfac14  23602  xkoccn  23603  txcnp  23604  ptcnplem  23605  txcnmpt  23608  txindislem  23617  txdis1cn  23619  txlly  23620  txnlly  23621  pthaus  23622  ptrescn  23623  hauseqlcld  23630  txlm  23632  tx2ndc  23635  txkgen  23636  xkoptsub  23638  xkopt  23639  xkoco1cn  23641  xkoco2cn  23642  xkococnlem  23643  xkococn  23644  cnmpt11  23647  cnmpt12  23651  cnmpt21  23655  cnmpt22  23658  cnmptkp  23664  cnmptk1p  23669  xkoinjcn  23671  txconn  23673  qtopval2  23680  elqtop  23681  idqtop  23690  qtopcld  23697  qtopeu  23700  qtoprest  23701  qtopomap  23702  qtopcmap  23703  ishmeo  23743  hmeoopn  23750  hmeocld  23751  ordthmeolem  23785  ptcmpfi  23797  elmptrab  23811  fgcl  23862  trfil2  23871  cfinfil  23877  uzrest  23881  ufilss  23889  trufil  23894  cfinufil  23912  ufinffr  23913  ufildr  23915  rnelfm  23937  flfcntr  24027  ptcmplem2  24037  ptcmplem3  24038  ptcmplem4  24039  ptcmplem5  24040  cnextfvval  24049  tmdcn2  24073  tmdmulg  24076  tmdgsum2  24080  symgtgp  24090  opnsubg  24092  clssubg  24093  tgpconncompeqg  24096  ghmcnp  24099  tgphaus  24101  tgpt0  24103  qustgpopn  24104  qustgplem  24105  tsmsgsum  24123  tsmssubm  24127  tsmsres  24128  tsmsf1o  24129  tsmsxplem1  24137  tsmsxplem2  24138  tsmsxp  24139  istrg  24148  istdrg  24150  istdrg2  24162  istlm  24169  istvc  24176  ustval  24187  ustincl  24192  ustdiag  24193  ustinvel  24194  ustexhalf  24195  ust0  24204  ucnima  24264  fmucndlem  24274  prdsdsf  24351  prdsxmet  24353  imasf1oxmet  24359  imasf1omet  24360  prdsxmslem2  24513  metustsym  24539  isnlm  24659  qtopbaslem  24742  xrtgioo  24791  reperflem  24803  fsumcn  24856  expcn  24858  xrhmeo  24932  cnllycmp  24942  bndth  24944  isclm  25050  lmhmclm  25073  lmmcvg  25247  fmcfil  25258  iscfil3  25259  iscau2  25263  iscau4  25265  iscmet3lem1  25277  iscmet3  25279  cfilres  25282  caussi  25283  equivcfil  25285  flimcfil  25300  bcthlem1  25310  isbn  25324  srabn  25346  ishl2  25356  cmslssbn  25358  cmscsscms  25359  minveclem3b  25414  ivthlem1  25437  ivthlem2  25438  ivthlem3  25439  ivth2  25441  ivthle  25442  ivthle2  25443  ivthicc  25444  ovolficcss  25455  ovolunlem1a  25482  ovolunlem1  25483  ovolfiniun  25487  ovoliunlem1  25488  ovoliunlem3  25490  ovoliun  25491  ovoliun2  25492  shft2rab  25494  ovolshftlem1  25495  sca2rab  25498  ovolscalem1  25499  mblsplit  25518  finiunmbl  25530  volun  25531  volfiniun  25533  voliunlem1  25536  voliunlem3  25538  iunmbl  25539  voliun  25540  volsup  25542  ioombl  25551  ioorcl  25563  vitalilem1  25594  vitalilem2  25595  vitalilem3  25596  vitalilem4  25597  vitali  25599  ismbf1  25610  mbfdm  25612  ismbf  25614  ismbfcn  25615  mbfima  25616  mbfimaicc  25617  ismbfcn2  25624  ismbfd  25625  ismbf2d  25626  mbfeqalem1  25627  mbfmax  25635  mbfposr  25638  mbfposb  25639  ismbf3d  25640  mbfimaopnlem  25641  mbfimaopn2  25643  cncombf  25644  isi1f  25660  i1fd  25667  itg1mulc  25690  mbfi1fseqlem4  25704  itg2lcl  25713  isibl  25751  iblitg  25754  iblcnlem1  25774  iblcnlem  25775  iblrelem  25777  iblpos  25779  itgeqa  25800  itgfsum  25813  itgabs  25821  limcvallem  25857  ellimc  25859  ellimc2  25863  limcmpt  25869  cnmptlimc  25876  dvbsss  25888  cpnfval  25918  elcpn  25920  dvmptfsum  25961  dvle  25993  dvfsumle  26007  dvfsumge  26008  dvfsumabs  26009  dvfsumrlimf  26011  dvfsumlem1  26012  dvfsumlem2  26013  dvfsumlem3  26014  dvfsumlem4  26015  dvfsumrlimge0  26016  dvfsumrlim  26017  dvfsumrlim2  26018  dvfsum2  26020  itgsubstlem  26034  itgsubst  26035  mdegcl  26053  deg1nn0clb  26074  isuc1p  26125  plyeq0lem  26194  plyco  26225  plycj  26261  plycjOLD  26263  dvply2g  26270  dvnply2  26272  plydivlem4  26281  fta1lem  26292  fta1  26293  elqaalem1  26304  elqaalem2  26305  elqaalem3  26306  elqaa  26307  ulmcau  26379  radcnv0  26400  radcnvlt1  26402  radcnvle  26404  pserdvlem2  26412  coseq1  26508  efeq1  26511  sinord  26517  efif1olem2  26526  efif1olem4  26528  lognegb  26573  logcj  26589  argimgt0  26595  logtayl  26643  2irrexpq  26714  root1eq1  26738  logrec  26746  2irrexpqALT  26783  angrteqvd  26789  angpieqvdlem  26811  atans  26913  atans2  26914  dmarea  26940  areambl  26941  rlimcnp  26948  rlimcnp2  26949  xrlimcnp  26951  harmonicbnd  26986  harmonicbnd2  26987  lgamcvglem  27022  wilthlem2  27051  wilth  27053  efnnfsumcl  27085  vmacl  27100  efvmacl  27102  efchtdvds  27141  sqff1o  27164  fsumdvdscom  27167  musumsum  27174  fsumdvdsmul  27177  fsumvma  27195  perfect  27213  dchrelbasd  27221  lgsval  27283  lgsval2lem  27289  lgsdir2lem4  27310  lgsdir2  27312  lgsqrlem1  27328  lgsdchr  27337  m1lgs  27370  2lgs  27389  mul2sq  27401  2sqlem6  27405  2sqblem  27413  2sq2  27415  rplogsumlem2  27467  dchrisumlema  27470  dchrisumlem2  27472  dchrisumlem3  27473  dchrvmasumlem2  27480  dchrvmasumlem3  27481  dchrisum0flblem2  27491  dchrisum0flb  27492  dchrisum0fno1  27493  ostthlem1  27609  nodmon  27633  noextendseq  27650  nodense  27675  madefi  27924  addsproplem1  27980  addsproplem3  27982  addsprop  27987  addsf  27993  addbdaylem  28028  negsproplem1  28039  negsproplem3  28041  negsprop  28046  negbdaylem  28067  mulsproplemcbv  28126  mulsproplem1  28127  mulsproplem10  28136  mulsprop  28141  addonbday  28290  noseqp1  28302  noseqind  28303  peano5n0s  28330  dfn0s2  28343  n0addscl  28355  n0mulscl  28356  n0bday  28363  onsfi  28367  n0s0m1  28373  n0subs  28374  n0p1nns  28382  dfnns2  28383  nn1m1nns  28385  oldfib  28388  zaddscl  28405  zmulscld  28408  elzn0s  28409  peano5uzs  28415  expscllem  28441  z12addscl  28488  z12shalf  28491  z12negsclb  28492  z12zsodd  28493  z12bdaylem  28495  z12bday  28496  bdayfin  28498  mirval  28742  perpneq  28801  isperp2  28802  isperp2d  28803  foot  28809  islnopp  28826  islnoppd  28827  outpasch  28842  hlpasch  28843  ishpg  28846  colopp  28856  colhp  28857  lmif  28872  islmib  28874  lmiinv  28879  trgcopy  28891  trgcopyeu  28893  acopyeu  28921  inaghl  28932  tgasa1  28945  f1otrgitv  28957  f1otrg  28958  isfusgr  29406  opfusgr  29411  fusgrfisbase  29416  fusgrfisstep  29417  nbupgrel  29433  nbumgrvtx  29434  nbusgreledg  29441  edgnbusgreu  29455  nb3grprlem1  29468  uvtxusgrel  29491  cusgredg  29512  cplgr2vpr  29521  cusgrexg  29532  usgredgsscusgredg  29547  fusgrn0degnn0  29587  rusgrnumwrdl2  29674  rgrx0ndm  29681  wlkcomp  29718  wlkdlem2  29769  clwlkcomp  29866  iswwlks  29923  wwlknllvtx  29933  0enwwlksnge1  29951  wlkiswwlks2lem5  29960  wwlksm1edg  29968  wwlksnred  29979  wwlksnext  29980  wwlksnextbi  29981  wwlksnredwwlkn  29982  wwlksnextfun  29985  wwlksnextinj  29986  wwlksnextsurj  29987  wwlksnextbij  29989  wwlksnfi  29993  wwlksnextproplem2  29997  wwlksnextprop  29999  2wlkdlem4  30015  rusgrnumwwlkl1  30058  rusgrnumwwlks  30064  isclwwlk  30073  clwwlk1loop  30077  clwwlkccatlem  30078  clwlkclwwlklem2a1  30081  clwlkclwwlklem2a4  30086  clwlkclwwlklem2a  30087  clwlkclwwlklem2  30089  clwlkclwwlklem3  30090  clwlkclwwlk  30091  clwlkclwwlk2  30092  clwwisshclwwslemlem  30102  clwwisshclwwslem  30103  clwwisshclwws  30104  clwwlknlbonbgr1  30128  clwwlkinwwlk  30129  clwwlkn1  30130  loopclwwlkn1b  30131  clwwlkn1loopb  30132  clwwlkn2  30133  clwwlkel  30135  clwwlkf  30136  clwwlkwwlksb  30143  clwwlkext2edg  30145  wwlksext2clwwlk  30146  wwlksubclwwlk  30147  eleclclwwlknlem2  30150  umgr2cwwk2dif  30153  s2elclwwlknon2  30193  clwwlknonwwlknonb  30195  clwwlknonex2lem2  30197  clwwlknonex2  30198  3wlkdlem4  30251  upgr3v3e3cycl  30269  upgr4cycl4dv4e  30274  eupth2lem2  30308  eulerpathpr  30329  1vwmgr  30365  3vfriswmgrlem  30366  3vfriswmgr  30367  3cyclfrgrrn1  30374  vdgn1frgrv2  30385  frgrncvvdeqlem3  30390  frgrncvvdeqlem8  30395  frgrncvvdeqlem9  30396  frgrwopregasn  30405  frgrwopregbsn  30406  frgrwopreglem5ALT  30411  frgr2wwlk1  30418  frgr2wwlkeqm  30420  fusgr2wsp2nb  30423  2clwwlk2clwwlklem  30435  extwwlkfabel  30442  nvvop  30699  isnvlem  30700  sspval  30813  nmorepnf  30858  phpar  30914  siilem2  30942  bnsscmcl  30958  ubthlem1  30960  shaddcl  31307  shmulcl  31308  hsn0elch  31338  hhssablo  31353  hhssnvt  31355  hhsssh  31359  shscl  31408  shintcl  31420  chintcl  31422  shincl  31471  chincl  31589  h1datomi  31671  chscllem2  31728  sumspansn  31739  spansncvi  31742  5oalem2  31745  5oalem3  31746  pjini  31789  pjjsi  31790  eigposi  31926  nmoprepnf  31957  nmfnrepnf  31970  dmadjrnb  31996  lnophmlem1  32106  lnophm  32109  nmcopex  32119  lnconi  32123  nmbdfnlb  32140  nmcfnex  32143  imaelshi  32148  rnbra  32197  leopg  32212  pjbdlni  32239  pjhmop  32240  hmopidmch  32243  pjclem4  32289  pj3si  32297  strlem1  32340  atssma  32468  atcv0eq  32469  atcv1  32470  atomli  32472  atcvatlem  32475  cdj3lem2a  32526  cdj3lem3a  32529  xppreima  32738  fmptcof2  32750  aciunf1lem  32755  funcnv4mpt  32761  1stpreimas  32799  f1od2  32812  fpwrelmapffslem  32825  xrofsup  32860  fzspl  32882  fzsplit3  32886  nnindf  32913  fprodex01  32918  fsumiunle  32922  indf1ofs  32946  gsumhashmul  33149  fzto1st  33185  fxpsubm  33254  fxpsubg  33255  fxpsubrg  33256  isslmd  33284  slmdlema  33285  elrgspnlem2  33325  elrgspnlem4  33327  subsdrg  33383  qusker  33433  0nellinds  33454  unitprodclb  33473  nsgmgclem  33495  nsgmgc  33496  nsgqusf1olem2  33498  elrspunidl  33512  prmidlval  33521  prmidlc  33532  opprlidlabs  33569  dfufd2lem  33641  psrbasfsupp  33704  selvply1rhmlemb  33712  mplidomlem  33720  lindsunlem  33817  brfldext  33838  brfinext  33845  finextfldext  33857  finexttrb  33858  extdg1id  33859  fldextrspunlsplem  33866  constrconj  33938  constrfin  33939  trisecnconstr  33985  smatrcl  33989  submateq  34002  lmatfval  34007  lmatcl  34009  qtophaus  34029  locfinreflem  34033  locfinref  34034  zartopn  34068  zarcmplem  34074  rhmpreimacnlem  34077  xpinpreima  34099  xpinpreima2  34100  cnre2csqlem  34103  tpr2rico  34105  prsdm  34107  prsrn  34108  ordtrest2NEWlem  34115  ordtrest2NEW  34116  zrhcntr  34172  qqhval2  34175  isrrext  34193  ismntoplly  34218  esumcvg  34279  sigaval  34304  issiga  34305  0elsiga  34307  sigaclcu  34310  issgon  34316  prsiga  34324  sigaclci  34325  difelsiga  34326  unelsiga  34327  ispisys2  34346  inelpisys  34347  unelldsys  34351  sigapildsyslem  34354  sigapildsys  34355  ldgenpisyslem1  34356  ldgenpisys  34359  isros  34361  unelros  34364  difelros  34365  fiunelros  34367  inelsros  34371  diffiunisros  34372  rossros  34373  measvuni  34407  measiun  34411  voliune  34422  volfiniune  34423  brfae  34441  ismbfm  34444  mbfmcnvima  34448  mbfmcst  34452  1stmbfm  34453  2ndmbfm  34454  imambfm  34455  sitgval  34525  issibf  34526  sibfima  34531  sitgfval  34534  sitgclg  34535  eulerpartlemelr  34550  eulerpartlemsf  34552  eulerpartleme  34556  eulerpartlemt0  34562  eulerpartlemt  34564  eulerpartgbij  34565  eulerpartlemr  34567  eulerpartlemmf  34568  eulerpartlemgvv  34569  eulerpartlemgs2  34573  eulerpartlemn  34574  eulerpart  34575  cndprobprob  34631  rrvsum  34647  orvcelel  34663  ballotlemodife  34691  ballotlemsdom  34705  ballotlemrv  34713  ballotlemrv1  34714  ballotlemrv2  34715  ballotlem1ri  34728  fsum2dsub  34800  reprinfz1  34815  reprpmtf1o  34819  reprdifc  34820  breprexplema  34823  hgt750lema  34850  hgt750leme  34851  bnj149  35066  bnj222  35074  bnj1112  35174  bnj1148  35187  fissorduni  35280  fineqvrep  35304  fineqvnttrclse  35314  fineqvinfep  35315  gblacfnacd  35339  vonf1owev  35345  loop1cycl  35374  subfacp1lem3  35419  subfacp1lem6  35422  erdszelem10  35437  kur14  35453  cvxsconn  35480  cnllysconn  35482  resconn  35483  iscvm  35496  cvmliftlem5  35526  cvmliftlem15  35535  cvmlift2lem1  35539  cvmlift2lem12  35551  cvmlift2lem13  35552  sat1el2xp  35616  fmlasuc  35623  gonan0  35629  gonar  35632  satefvfmla0  35655  msubrn  35766  msubco  35768  ismfs  35786  mvtinf  35792  mclsax  35806  mppspstlem  35808  elmpps  35810  nnuni  35964  dfdm5  36010  dfrn5  36011  elima4  36013  rdgprc0  36028  pprodss4v  36119  elfuns  36150  fnimage  36164  imageval  36165  fwddifval  36399  fwddifnval  36400  fwddifnp1  36402  elhf2g  36413  hfun  36415  hfninf  36423  filnetlem4  36618  onsucconn  36675  onsucsuccmp  36681  limsucncmp  36683  onint1  36686  fveleq  36688  findreccl  36690  nndivsub  36694  weiunse  36705  mh-inf3f1  36778  mh-infprim2bi  36784  mh-infprim3bi  36785  bj-seex  37284  bj-adjg1  37405  bj-mooreset  37469  bj-ismoored0  37473  bj-ismoored  37474  bj-inftyexpitaudisj  37574  bj-inftyexpidisj  37579  bj-isvec  37656  bj-isclm  37660  csbmpo123  37702  topdifinffinlem  37718  topdifinffin  37719  csbfinxpg  37759  phpreu  37980  finixpnum  37981  lindsenlbs  37991  poimirlem16  38012  poimirlem17  38013  poimirlem19  38015  poimirlem20  38016  poimirlem22  38018  poimirlem23  38019  poimirlem24  38020  poimirlem25  38021  poimirlem26  38022  poimirlem28  38024  poimirlem29  38025  poimirlem30  38026  poimirlem31  38027  poimirlem32  38028  poimir  38029  mblfinlem3  38035  ex-ovoliunnfl  38039  voliunnfl  38040  volsupnfl  38041  mbfresfi  38042  itgabsnc  38065  ftc1anclem6  38074  ftc1anclem7  38075  ftc1anclem8  38076  ftc1anc  38077  dvasin  38080  sdclem2  38118  fdc  38121  incsequz  38124  neificl  38129  mettrifi  38133  cntotbnd  38172  cnpwstotbnd  38173  ismtyima  38179  ismtyhmeolem  38180  heiborlem2  38188  heiborlem3  38189  heiborlem4  38190  heiborlem5  38191  heiborlem6  38192  heiborlem10  38196  isrngo  38273  isdivrngo  38326  drngoi  38327  idlval  38389  isidlc  38391  idladdcl  38395  idllmulcl  38396  idlrmulcl  38397  0idl  38401  pridlval  38409  smprngopr  38428  prnc  38443  ispridlc  38446  pridlc  38447  eqrelf  38634  iss2  38720  elcoeleqvrels  39055  elfunsALTV  39153  eldisjs  39195  eleldisjs  39204  fsumshftd  39453  riotaclbgBAD  39455  renegclALT  39464  lshpinN  39490  isopos  39681  oposlem  39683  glbconN  39878  lnnat  39928  2at0mat0  40026  islvol2aN  40093  dalawlem13  40384  pclfinclN  40451  lhpoc2N  40516  ltrncnvatb  40639  cdleme11h  40767  cdlemefr32sn2aw  40905  cdlemefs32sn1aw  40915  cdleme32fvaw  40940  cdlemg1fvawlemN  41074  dicelvalN  41679  dih1dimatlem  41830  dihlatat  41838  dihjatcclem4  41922  islpolN  41984  lpolsatN  41989  lpolpolsatN  41990  mapdordlem1a  42135  mapdordlem1  42137  mapdhcl  42228  iscsrg  42465  fzsplitnd  42476  lcmineqlem12  42534  intlewftc  42555  dvrelogpow2b  42562  aks4d1p1p3  42563  aks4d1p1p2  42564  aks4d1p1p4  42565  dvle2  42566  aks4d1p8  42581  aks4d1p9  42582  isprimroot  42587  primrootsunit1  42591  primrootscoprmpow  42593  aks6d1c1p1  42601  aks6d1c1p2  42603  aks6d1c1p3  42604  evl1gprodd  42611  hashscontpow  42616  aks6d1c3  42617  aks6d1c2  42624  sticksstones1  42640  sticksstones10  42649  sticksstones11  42650  sticksstones12a  42651  aks6d1c6lem1  42664  unitscyglem5  42693  retire  42805  reelznn0nn  42960  fsuppind  43049  fsuppssindlem2  43051  fsuppssind  43052  isnacs3  43168  nacsfix  43170  mzpclval  43183  mzpcl1  43187  mzpcl2  43188  mzpcl34  43189  mzpexpmpt  43203  mzpsubst  43206  diophin  43230  diophun  43231  2rexfrabdioph  43250  3rexfrabdioph  43251  4rexfrabdioph  43252  6rexfrabdioph  43253  7rexfrabdioph  43254  rabdiophlem2  43256  diophren  43267  fphpd  43270  fphpdo  43271  fiphp3d  43273  pellexlem1  43283  pell14qrexpclnn0  43320  pellqrex  43333  rmspecnonsq  43361  monotuz  43395  monotoddzzfi  43396  monotoddzz  43397  oddcomabszz  43398  modabsdifz  43440  rmxdioph  43470  expdiophlem2  43476  limsuc2  43495  dfac11  43516  kelac1  43517  dfac21  43520  lsmfgcl  43528  islnm  43531  lnmlssfg  43534  lmhmfgima  43538  pwslnm  43548  unxpwdom3  43549  pwfi2f1o  43550  islnr  43565  hbtlem2  43578  cnsrexpcl  43619  flcidc  43624  mendlmod  43643  proot1ex  43650  oaordnr  43750  omnord1  43759  oenord1  43770  cantnfresb  43778  onmcl  43785  tfsnfin  43806  nadd2rabtr  43838  nadd1rabtr  43842  nadd1rabex  43844  nadd1suc  43846  pwelg  44013  fipjust  44018  elnonrel  44038  elinlem  44051  elcnvlem  44054  ss2iundf  44112  dfhe3  44228  dffrege115  44431  rfovcnvf1od  44457  ntrneiel2  44539  clsneiel2  44562  neicvgel2  44573  grur1cld  44685  dvgrat  44765  cvgdvgrat  44766  radcnvrat  44767  binomcxplemdvsum  44808  binomcxplemnotnn0  44809  orbitcl  45410  modelaxreplem1  45431  modelaxreplem2  45432  modelaxrep  45434  fnchoice  45486  fiiuncl  45522  disjf1  45638  disjinfi  45647  choicefi  45654  axccdom  45675  fmptf  45691  fmptff  45721  monoords  45753  supminfrnmpt  45896  supxrleubrnmptf  45902  supminfxr  45915  supminfxr2  45920  supminfxrrnmpt  45922  monoordxrv  45932  monoordxr  45933  monoord2xrv  45934  monoord2xr  45935  caucvgbf  45940  cvgcaule  45942  fsummulc1f  46024  fsumnncl  46025  fsumf1of  46027  fsumreclf  46029  fsumlessf  46030  fsumsermpt  46032  fmul01  46033  fmulcl  46034  fmuldfeqlem1  46035  fmuldfeq  46036  fmul01lt1lem1  46037  fmul01lt1lem2  46038  fprodexp  46047  fprodabs2  46048  mccllem  46050  mccl  46051  fprodcnlem  46052  fprodcn  46053  climmulf  46057  climsuse  46061  climrecf  46062  climaddf  46068  climf  46075  sumnnodd  46083  clim2f  46087  0ellimcdiv  46100  climsubmpt  46111  climreclf  46115  climf2  46117  fnlimcnv  46118  climeldmeqmpt  46119  clim2f2  46121  climfveqmpt  46122  fnlimfvre  46125  fnlimabslt  46130  climfveqmpt3  46133  climbddf  46138  climeldmeqmpt3  46140  climinf2mpt  46165  climinfmpt  46166  limsupequzmptf  46182  lmbr3  46198  liminfreuzlem  46253  coseq0  46315  cncfshift  46325  cncfperiod  46330  fprodcncf  46351  ioodvbdlimc1lem2  46383  ioodvbdlimc2lem  46385  dvmptmulf  46388  dvnmptdivc  46389  dvnmul  46394  dvmptfprod  46396  iblspltprt  46424  itgspltprt  46430  stoweidlem2  46453  stoweidlem3  46454  stoweidlem4  46455  stoweidlem6  46457  stoweidlem8  46459  stoweidlem17  46468  stoweidlem19  46470  stoweidlem20  46471  stoweidlem21  46472  stoweidlem23  46474  stoweidlem27  46478  stoweidlem35  46486  stoweidlem42  46493  stoweidlem43  46494  stoweidlem62  46513  stoweid  46514  wallispilem3  46518  wallispi  46521  fourierdlem16  46574  fourierdlem21  46579  fourierdlem41  46599  fourierdlem42  46600  fourierdlem48  46605  fourierdlem49  46606  fourierdlem50  46607  fourierdlem51  46608  fourierdlem54  46611  fourierdlem63  46620  fourierdlem64  46621  fourierdlem65  46622  fourierdlem71  46628  fourierdlem72  46629  fourierdlem73  46630  fourierdlem83  46640  fourierdlem86  46643  fourierdlem89  46646  fourierdlem90  46647  fourierdlem91  46648  fourierdlem96  46653  fourierdlem97  46654  fourierdlem98  46655  fourierdlem99  46656  fourierdlem100  46657  fourierdlem103  46660  fourierdlem104  46661  fourierdlem105  46662  fourierdlem108  46665  fourierdlem109  46666  fourierdlem110  46667  fourierdlem112  46669  fourierdlem113  46670  etransclem24  46709  salunicl  46767  saluncl  46768  saldifcl  46770  sge0f1o  46833  sge0lempt  46861  sge0iunmptlemfi  46864  sge0p1  46865  sge0fodjrnlem  46867  sge0iunmpt  46869  sge0ltfirpmpt2  46877  sge0isummpt2  46883  sge0xaddlem2  46885  sge0xadd  46886  ismea  46902  nnfoctbdjlem  46906  nnfoctbdj  46907  meadjiun  46917  voliunsge0lem  46923  meaiuninclem  46931  meaiuninc3v  46935  hoidmvlelem2  47047  hoidmvlelem3  47048  vonvolmbl2  47114  hoimbl2  47116  vonhoire  47123  vonicclem2  47135  vonn0ioo2  47141  vonn0icc2  47143  salpreimagelt  47158  salpreimalegt  47160  salpreimagtge  47176  salpreimaltle  47177  issmf  47179  salpreimagtlt  47181  smfpreimalt  47182  smfpreimaltf  47187  issmfle  47196  smfpreimale  47205  issmfgt  47207  smfpreimagt  47213  issmfgelem  47220  issmfge  47221  smflimlem4  47225  smflim  47228  smfpreimage  47233  smfresal  47239  smfpimbor1lem1  47249  smfpimbor1lem2  47250  smflim2  47257  smflimmpt  47261  smflimsuplem1  47271  smflimsuplem2  47272  smflimsuplem3  47273  smflimsuplem5  47275  smflimsuplem7  47277  smflimsup  47279  smfliminf  47282  ormkglobd  47328  cjnpoly  47360  eu2ndop1stv  47596  dmfcoafv  47646  ffnaov  47670  faovcl  47671  funressndmafv2rn  47694  dfatdmfcoafv2  47725  mod2addne  47841  smonoord  47848  iccpartiltu  47905  iccpartigtl  47906  sprsymrelf1lem  47974  prproropf1olem2  47987  fmtno4prmfac193  48059  proththdlem  48099  proththd  48100  iseven  48127  isodd  48128  dfodd2  48135  evenm1odd  48138  evenp1odd  48139  enege  48144  onego  48145  epee  48204  perfectALTV  48222  bgoldbtbndlem2  48305  bgoldbtbndlem3  48306  bgoldbtbndlem4  48307  bgoldbtbnd  48308  clnbupgrel  48333  edgusgrclnbfin  48341  grimuhgr  48386  uhgrimedgi  48389  uhgrimprop  48391  isuspgrim0  48393  isuspgrimlem  48394  grimedg  48434  grtriproplem  48438  grtrif1o  48441  isgrtri  48442  grtriclwlk3  48444  cycl3grtrilem  48445  cycl3grtri  48446  grimgrtri  48448  usgrgrtrirex  48449  isubgr3stgrlem7  48471  grlimprclnbgrvtx  48498  grlimgredgex  48499  grlimgrtri  48502  usgrexmpl1tri  48524  gpgvtxel2  48547  gpgvtx0  48552  gpgvtx1  48553  gpgedgvtx0  48560  gpgedgvtx1  48561  gpgedgiov  48564  gpgedg2ov  48565  gpgedg2iv  48566  gpgnbgrvtx0  48573  gpgnbgrvtx1  48574  gpg3kgrtriex  48588  gpgprismgr4cycllem3  48596  pgnbgreunbgrlem1  48612  pgnbgreunbgrlem2lem1  48613  pgnbgreunbgrlem2lem2  48614  pgnbgreunbgrlem2lem3  48615  pgnbgreunbgrlem4  48618  pgnbgreunbgrlem5lem1  48619  pgnbgreunbgrlem5lem2  48620  pgnbgreunbgrlem5lem3  48621  pgnbgreunbgr  48624  grlimedgnedg  48630  uzlidlring  48734  cbvmpox2  48835  lmod1  48991  nnolog2flm1  49089  dignn0flhalflem1  49114  catprsc  49511  nelsubc3lem  49568  fucofulem2  49809  fucofvalne  49823  isthincd2lem2  49933  euendfunc  50024  cnelsubclem  50101