Theorem eleq1d 2845

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  eleq1  2848  eleq12d  2854  eqeltrd  2860  eqneltrd  2880  rspcimdv  3566  reuind  3711  sbcel2  4376  sbccsb2  4395  disjiun  5091  breq1  5106  breq2  5107  axrep6g  5245  inex1g  5282  intex  5308  pwexg  5343  reusv2lem4  5366  reusv2  5368  reusv3  5370  rabxfrd  5382  prexOLD  5408  opelopabsb  5508  csbmpt12  5536  pofun  5581  seex  5614  seinxp  5739  opabid2  5810  opeliunxp2  5819  elrn2g  5876  opeldmd  5892  opeldm  5893  elreldm  5921  elsnres  6016  iss  6033  unielrel  6273  onunel  6467  funopg  6570  brprcneu  6871  brprcneuALT  6872  tz6.12f  6906  ndmfvrcl  6914  ssimaex  6966  dmfco  6977  fvmpti  6988  fvmpt3  6994  fvmptf  7011  fvmptss2  7016  respreima  7061  fvn0ssdmfun  7070  fvelrn  7072  ffnfvf  7116  ffvresb  7122  fmptco  7126  fmptcof  7127  fsn  7132  fsn2g  7135  fressnfv  7160  fvrnressn  7161  fnex  7219  funfvima  7232  funfvima3  7238  f1mpt  7261  fliftfuns  7318  isoselem  7345  isowe2  7354  riotaclb  7414  ovrspc2v  7442  ffnov  7542  fovcld  7543  ovmpos  7564  ov2gf  7565  ovg  7581  funimassov  7594  oprssdm  7598  ndmovrcl  7603  caovclg  7609  elovmpo  7662  ofmpteq  7707  sorpsscmpl  7741  uniexg  7748  abnexg  7761  difsnexi  7766  onint  7795  limsuc  7851  tfisi  7861  peano5  7896  xpexr  7921  xpexcnv  7923  fnexALT  7954  focdmex  7959  f1stres  8016  f2ndres  8017  xp1st  8024  xp2nd  8025  unielxp  8030  opiota  8061  fmpox  8069  offval22  8090  frxp  8129  fnse  8136  frxp2  8147  sexp2  8149  frxp3  8154  sexp3  8156  opeliunxp2f  8213  dftpos4  8248  fvmpocurryd  8274  undefnel2  8281  onnseq  8338  smoel  8354  smo11  8358  tfrlem8  8378  tfrlem9  8379  tfrlem15  8386  tfr2b  8390  tz7.44-2  8401  tz7.44-3  8402  oacl  8529  omcl  8530  oecl  8531  oaord1  8545  omordi  8560  oen0  8581  oeeui  8597  nnacl  8606  nnmcl  8607  nnecl  8608  nnmordi  8626  nnaordex  8633  omsmolem  8652  naddcllem  8671  naddov2  8674  naddf  8677  naddssim  8681  naddelim  8682  naddasslem1  8690  naddasslem2  8691  naddsuc2  8697  erexb  8729  elecex  8754  qliftfuns  8811  ixpsnval  8914  elixp2  8915  resixp  8947  undifixp  8948  mptelixpg  8949  resixpfo  8950  elixpsn  8951  fundmen  9045  fopwdom  9090  disjen  9139  xpf1o  9144  unfi  9172  cnvfi  9177  fnfi  9179  f1oenfirn  9181  f1domfi  9182  unblem2  9270  pwfi  9295  fiint  9303  iunfi  9317  tfsnfin2  9337  isfsupp  9342  fsuppun  9364  ffsuppbi  9375  elfi2  9391  wdom2d  9559  ixpiunwdom  9569  dfom3  9633  cantnfvalf  9651  cantnflt  9658  cantnflem1  9675  r1fin  9762  tz9.12lem3  9778  ranksnb  9816  ranklim  9835  r1pw  9836  r1pwALT  9837  r1pwcl  9838  rankuni2b  9844  elhf2g  9883  hfun  9886  djuexb  9939  cardmin2  10029  infxpenc2lem1  10047  dfac8alem  10057  dfac8clem  10060  ac5num  10064  acni2  10074  acnlem  10076  alephon  10097  alephfplem3  10134  alephfplem4  10135  dfac4  10150  dfac5lem1  10151  dfac5lem5  10155  dfac2a  10157  dfac2b  10158  dfacacn  10169  dfac12lem2  10172  dfac12r  10174  dfac12k  10175  cofsmo  10296  cfsmolem  10297  isfin1a  10319  fin1ai  10320  isfin3  10323  infpssrlem3  10332  fin23lem7  10343  fin23lem11  10344  enfin2i  10348  isf34lem4  10404  fin1a2lem7  10433  hsmexlem9  10452  hsmexlem4  10456  hsmex  10459  axcc2lem  10463  axcc3  10465  axdc3lem2  10478  axcclem  10484  zornn0g  10532  ttukeylem3  10538  ttukeylem6  10541  ttukey2g  10543  brdom7disj  10559  brdom6disj  10560  fnct  10569  fnctOLD  10570  konigthlem  10602  axregndlem2  10637  axinfnd  10640  axacndlem5  10645  axacnd  10646  fpwwe2lem4  10668  fpwwe2lem12  10676  fpwwe  10680  pwfseqlem1  10692  pwfseqlem3  10694  pwfseqlem4a  10695  pwfseqlem4  10696  wununi  10740  wunpw  10741  wunpr  10743  wunr1om  10753  tskpw  10787  tskr1om  10801  inar1  10809  grupw  10829  grupr  10831  gruurn  10832  gruiun  10833  ingru  10849  grur1a  10853  grothomex  10863  grothac  10864  addnidpi  10935  indpi  10941  adderpq  10990  mulerpq  10991  addclprlem2  11051  mulclprlem  11053  distrlem4pr  11060  prlem934  11067  ltexprlem3  11072  ltexprlem4  11073  ltexprlem7  11076  ltexpri  11077  prlem936  11081  reclem2pr  11082  reclem3pr  11083  addclsr  11117  mulclsr  11118  supsrlem  11145  supsr  11146  axaddf  11179  axmulf  11180  axaddrcl  11186  axmulrcl  11188  renegcl  11570  negreb  11572  negn0  11692  negf1o  11693  ltord1  11789  leord1  11790  eqord1  11791  ltord2  11792  leord2  11793  eqord2  11794  negfi  12213  infm3  12223  cju  12263  indfval  12274  peano5nni  12285  peano2nn  12294  dfnn2  12295  nn1m1nn  12303  nnaddcl  12305  nnmulcl  12306  nnsub  12329  nndivtr  12332  un0addcl  12586  un0mulcl  12587  elnnnn0  12596  nn0sub  12603  fcdmnn0fsuppg  12613  elz  12642  nnnegz  12643  elz2  12658  znegclb  12680  zaddcl  12683  nzadd  12691  zmulcl  12692  zneo  12729  nneo  12730  zeo  12732  peano5uzi  12735  zindd  12747  uzp1  12949  uzaddcl  12978  ublbneg  13007  eqreznegel  13008  supminf  13009  zsupss  13011  qmulz  13025  qnegcl  13041  irradd  13048  irrmul  13049  xnn0xaddcl  13312  fzrev2  13668  injresinjlem  13871  negmod0  13964  om2uzuzi  14038  uzindi  14071  fsuppmapnn0ub  14084  mptnn0fsuppr  14088  seqexw  14106  seqcl2  14109  seqcl  14111  seqf  14112  monoord  14121  monoord2  14122  sermono  14123  seqsplit  14124  seqcaopr2  14127  seqid3  14135  seqhomo  14138  expcllem  14161  expcl2lem  14162  m1expcl2  14174  faccl  14372  facdiv  14376  facndiv  14377  bccmpl  14398  bccl  14411  hashclb  14447  hasheq0  14452  hashfn  14464  seqcoll  14554  opfi1uzind  14601  ccatalpha  14685  reuccatpfxs1lem  14840  reuccatpfxs1  14841  repswccat  14882  repswrevw  14883  2cshw  14909  2cshwcshw  14921  cshimadifsn  14925  cshco  14932  swrd2lsw  15050  wwlktovf  15054  wwlktovf1  15055  wwlktovfo  15056  wrd2f1tovbij  15058  shftlem  15166  shftf  15177  cjval  15214  cjth  15215  remim  15229  cnpart  15352  uzin2  15457  caubnd2  15470  sqreulem  15472  clim  15606  clim2  15616  lo1o12  15645  climrlim2  15659  lo1resb  15676  o1resb  15678  lo1eq  15680  climmpt2  15685  climshftlem  15686  rlimcld2  15690  climcn1  15704  climcn2  15705  o1dif  15742  iserex  15769  climub  15774  climserle  15775  isercoll  15780  climcau  15783  caurcvg2  15790  caucvgb  15792  summolem3  15825  summolem2a  15826  zsum  15829  fsum  15831  sumss2  15837  fsumcvg2  15838  fsumclf  15849  fsumsplitf  15853  fsumsplit1  15856  sumpr  15859  sumtp  15860  fsumm1  15862  fsum1p  15864  isummulc2  15873  fsum2dlem  15881  fsumcom2  15885  fsumshftm  15892  fsum0diag2  15894  fsumge1  15909  fsum00  15910  fsumabs  15913  telfsumo  15914  telfsumo2  15915  fsumparts  15918  fsumrlim  15923  fsumo1  15924  o1fsum  15925  fsumiun  15933  binomlem  15943  isumshft  15953  isum1p  15955  isumrpcl  15957  climcndslem1  15963  climcndslem2  15964  climcnds  15965  infcvgaux2i  15972  cvgrat  15997  mertens  16000  clim2prod  16002  prodfn0  16008  prodfrec  16009  prodfdiv  16010  ntrivcvgfvn0  16013  prodmolem3  16045  prodmolem2a  16046  zprod  16049  fprod  16053  prodss  16059  fprodser  16061  fprodm1  16079  fprod1p  16080  fprodm1s  16082  fprodp1s  16083  fprodabs  16086  fprodn0  16091  fprod2dlem  16092  fprodcnv  16095  fprodcom2  16096  fproddivf  16099  fprodsplitf  16100  fprodsplit1f  16102  bpolycl  16163  fprodefsum  16206  rpnnen2lem11  16337  mod2eq1n2dvds  16462  mulsucdiv2z  16468  zob  16474  nn0o1gt2  16496  nno  16497  nn0o  16498  divalglem7  16514  bitsf1  16561  sadcp1  16570  smupp1  16595  qnumdencl  16855  iserodd  16952  pcqcl  16973  pcxnn0cl  16977  pcxcl  16978  pcgcd1  16994  dvdsprmpweqle  17003  pcmpt  17009  pcmpt2  17010  pcmptdvds  17011  infpnlem2  17028  infpn2  17030  1arith  17044  elgz  17048  mul4sq  17071  4sqlem13  17074  4sqlem17  17078  4sqlem18  17079  4sqlem19  17080  vdwlem1  17098  vdwlem2  17099  vdwnn  17115  ramtcl2  17128  ramcl  17146  prmonn2  17156  prmodvdslcmf  17164  isstruct2  17266  wunress  17366  firest  17542  imasaddfnlem  17639  imasvscafn  17648  xpsfrnel2  17675  mreintcl  17704  ismred2  17712  mreexexlemd  17757  mreexexlem3d  17759  mreexexlem4d  17760  iscatd2  17794  catpropd  17822  subsubc  17967  isfunc  17978  inclfusubc  18057  fncnvimaeqv  18233  joindef  18487  joinval  18488  meetdef  18501  meetval  18502  oduclatb  18620  acsdrsel  18656  isacs4lem  18657  isacs5lem  18658  acsdrscl  18659  mgmsscl  18760  mgmn0plusgf  18766  mgmpropd  18768  mgm1  18775  gsumvalx  18804  issubmgm  18830  issubmgm2  18831  mgmhmima  18843  sgrppropd  18859  mndpropd  18890  issubm  18937  0subm  18952  insubm  18953  mhmimalem  18959  gsumwsubmcl  18972  gsumwspan  18981  symggrplem  19019  sursubmefmnd  19031  injsubmefmnd  19032  smndex1basss  19043  degenmgm  19076  degenmgm2nfun  19078  degenmgm2  19079  mulgsubcl  19237  issubg  19275  issubg2  19291  issubg4  19295  0subg  19301  isnsg  19304  isnsg2  19305  nsgbi  19306  isnsg3  19309  elnmz  19312  nmzbi  19313  nmzsubg  19314  eqgval  19328  eqgid  19331  cycsubgcl  19360  ghmrn  19382  ghmnsgima  19393  gass  19454  oppgsubg  19516  f1omvdconj  19599  symgfisg  19621  psgneldm  19656  0subgALT  19721  odhash3  19729  sylow2blem2  19774  lsmsubm  19806  lsmsubg  19807  efgsf  19882  efgsdm  19883  efgs1b  19889  efgredlema  19893  eqgabl  19987  ablnsg  20000  cyggenod2  20038  gsumzaddlem  20074  gsummhm2  20092  gsum2dlem2  20124  gsum2d2lem  20126  gsumcom2  20128  dprdfeq0  20177  dprdsubg  20179  dprd2da  20197  ablfacrp  20221  pgpfac1lem3  20232  pgpfaclem1  20236  ablfaclem3  20242  ablfac2  20244  cycsubggenodd  20264  isrng  20315  issrg  20353  srgfcl  20361  rglcom4d  20376  srgbinomlem4  20394  isring  20402  iscrng  20405  dvdsr  20531  irredrmul  20596  isrngim  20614  isrim0  20652  issubrng  20738  subrngringnsg  20744  issubrng2  20749  rhmimasubrnglem  20756  issubrg  20762  issubrg2  20783  subrgpropd  20799  isdrngd  20961  isdrngdOLD  20963  issdrg  20984  sdrgacs  20997  issrngd  21051  islmod  21078  lmodlema  21079  islmodd  21080  lmodprop2d  21138  rmodislmodlem  21143  rmodislmod  21144  lssset  21147  islssd  21149  lsscl  21156  lsslss  21175  lsspropd  21231  lmhmima  21261  lbsind  21294  lsmcl  21297  islvec  21318  lmhmlvec  21324  lspsolvlem  21359  lspsolv  21360  lvecpropd  21384  rnglidlmcl  21434  rnglidl0  21448  rnglidlmmgm  21472  df2idl2crng  21516  rngqiprngimf1lem  21529  rngqiprngimf1  21535  ring2idlqus  21544  prmidlval  21557  prmidlc  21568  prmidlprop  21571  xrsdsreclblem  21658  xrsdsreclb  21659  cnsubrglem  21662  prmirred  21719  pzriprnglem4  21729  pzriprnglem8  21733  pzriprngALT  21740  znunithash  21809  cofipsgn  21838  zrhpsgnelbas  21839  rzgrp  21868  isphl  21873  phllmhm  21877  ipcl  21878  isphld  21899  phlpropd  21900  phlssphl  21904  cssincl  21933  pjdm  21952  dsmmval  21979  dsmmbas2  21982  dsmmelbas  21984  frlmbas  22000  frlmup1  22043  lindfind  22061  lindsind  22062  f1lindf  22067  islindf4  22083  lindsenlbs  22096  psrbag  22164  psrbaglefi  22173  mplsubglem  22245  mpllsslem  22246  ltbwe  22292  psrbagsn  22311  subrgasclcl  22315  mplind  22318  mpfind  22363  psdmul  22426  coe1mul2lem2  22526  gsumply1eq  22566  evl1vsd  22601  mpfpf1  22608  pf1mpf  22609  pf1ind  22612  matecl  22679  m1detdiag  22851  mdetralt  22862  mdetralt2  22863  mdetunilem2  22867  mdetunilem9  22874  m2detleiblem3  22883  m2detleiblem4  22884  smadiadetlem0  22915  cpmatacl  22973  chpscmat  23099  uniopn  23154  inopn  23156  fiinopn  23158  istps  23191  fctop  23261  iscld  23284  isopn2  23289  mretopd  23349  iscldtop  23352  perfi  23412  tgrest  23416  restcld  23429  ordtbaslem  23445  ordtrest2lem  23460  ordtrest2  23461  iscn  23492  cnpval  23493  iscnp  23494  tgcn  23509  subbascn  23511  ssidcn  23512  lmbrf  23517  cnpnei  23521  cnima  23522  iscncl  23526  cnconst2  23540  cnrest2  23543  cnpresti  23545  cnprest  23546  cnindis  23549  lmres  23557  lmcnp  23561  iscnrm  23580  t1sncld  23583  cnrmi  23617  cncmp  23649  cmpsublem  23656  fiuncmp  23661  unconn  23686  conncompid  23688  conncompconn  23689  conncompss  23690  1stcfb  23702  2ndcrest  23711  2ndcctbss  23713  2ndcdisj  23714  1stccnp  23720  islly  23726  isnlly  23727  subislly  23739  restnlly  23740  restlly  23741  islly2  23742  hausllycmp  23752  cldllycmp  23753  dislly  23755  isptfin  23774  islocfin  23775  ptfinfin  23777  finlocfin  23778  dissnlocfin  23787  locfindis  23788  comppfsc  23790  kgenval  23793  elkgen  23794  kgeni  23795  cmpkgen  23809  1stckgenlem  23811  kgencn2  23815  ptpjpre1  23829  elpt  23830  elptr  23831  ptbasin  23835  xkobval  23844  xkoval  23845  xkoopn  23847  txbasval  23864  tx1cn  23867  tx2cn  23868  dfac14  23876  xkoccn  23877  txcnp  23878  ptcnplem  23879  txcnmpt  23882  txindislem  23891  txdis1cn  23893  txlly  23894  txnlly  23895  pthaus  23896  ptrescn  23897  hauseqlcld  23904  txlm  23906  tx2ndc  23909  txkgen  23910  xkoptsub  23912  xkopt  23913  xkoco1cn  23915  xkoco2cn  23916  xkococnlem  23917  xkococn  23918  cnmpt11  23921  cnmpt12  23925  cnmpt21  23929  cnmpt22  23932  cnmptkp  23938  cnmptk1p  23943  xkoinjcn  23945  txconn  23947  qtopval2  23954  elqtop  23955  idqtop  23964  qtopcld  23971  qtopeu  23974  qtoprest  23975  qtopomap  23976  qtopcmap  23977  ishmeo  24017  hmeoopn  24024  hmeocld  24025  ordthmeolem  24059  ptcmpfi  24071  elmptrab  24085  fgcl  24136  trfil2  24145  cfinfil  24151  uzrest  24155  ufilss  24163  trufil  24168  cfinufil  24186  ufinffr  24187  ufildr  24189  rnelfm  24211  flfcntr  24301  ptcmplem2  24311  ptcmplem3  24312  ptcmplem4  24313  ptcmplem5  24314  cnextfvval  24323  tmdcn2  24347  tmdmulg  24350  tmdgsum2  24354  symgtgp  24364  opnsubg  24366  clssubg  24367  tgpconncompeqg  24370  ghmcnp  24373  tgphaus  24375  tgpt0  24377  qustgpopn  24378  qustgplem  24379  tsmsgsum  24397  tsmssubm  24401  tsmsres  24402  tsmsf1o  24403  tsmsxplem1  24411  tsmsxplem2  24412  tsmsxp  24413  istrg  24422  istdrg  24424  istdrg2  24436  istlm  24443  istvc  24450  ustval  24461  ustincl  24466  ustdiag  24467  ustinvel  24468  ustexhalf  24469  ust0  24478  ucnima  24538  fmucndlem  24548  prdsdsf  24625  prdsxmet  24627  imasf1oxmet  24633  imasf1omet  24634  prdsxmslem2  24787  metustsym  24813  isnlm  24933  qtopbaslem  25016  xrtgioo  25065  reperflem  25077  fsumcn  25130  expcn  25132  xrhmeo  25206  cnllycmp  25216  bndth  25218  isclm  25324  lmhmclm  25347  lmmcvg  25521  fmcfil  25532  iscfil3  25533  iscau2  25537  iscau4  25539  iscmet3lem1  25551  iscmet3  25553  cfilres  25556  caussi  25557  equivcfil  25559  flimcfil  25574  bcthlem1  25584  isbn  25598  srabn  25620  ishl2  25630  cmslssbn  25632  cmscsscms  25633  minveclem3b  25688  ivthlem1  25711  ivthlem2  25712  ivthlem3  25713  ivth2  25715  ivthle  25716  ivthle2  25717  ivthicc  25718  ovolficcss  25729  ovolunlem1a  25756  ovolunlem1  25757  ovolfiniun  25761  ovoliunlem1  25762  ovoliunlem3  25764  ovoliun  25765  ovoliun2  25766  shft2rab  25768  ovolshftlem1  25769  sca2rab  25772  ovolscalem1  25773  mblsplit  25792  finiunmbl  25804  volun  25805  volfiniun  25807  voliunlem1  25810  voliunlem3  25812  iunmbl  25813  voliun  25814  volsup  25816  ioombl  25825  ioorcl  25837  vitalilem1  25868  vitalilem2  25869  vitalilem3  25870  vitalilem4  25871  vitali  25873  ismbf1  25884  mbfdm  25886  ismbf  25888  ismbfcn  25889  mbfima  25890  mbfimaicc  25891  ismbfcn2  25898  ismbfd  25899  ismbf2d  25900  mbfeqalem1  25901  mbfmax  25909  mbfposr  25912  mbfposb  25913  ismbf3d  25914  mbfimaopnlem  25915  mbfimaopn2  25917  cncombf  25918  isi1f  25934  i1fd  25941  itg1mulc  25964  mbfi1fseqlem4  25978  itg2lcl  25987  isibl  26025  iblitg  26028  iblcnlem1  26047  iblcnlem  26048  iblrelem  26050  iblpos  26052  itgeqa  26073  itgfsum  26086  itgabs  26094  limcvallem  26130  ellimc  26132  ellimc2  26136  limcmpt  26142  cnmptlimc  26149  dvbsss  26161  cpnfval  26191  elcpn  26193  dvmptfsum  26234  dvle  26266  dvfsumle  26280  dvfsumge  26281  dvfsumabs  26282  dvfsumrlimf  26284  dvfsumlem1  26285  dvfsumlem2  26286  dvfsumlem3  26287  dvfsumlem4  26288  dvfsumrlimge0  26289  dvfsumrlim  26290  dvfsumrlim2  26291  dvfsum2  26293  itgsubstlem  26307  itgsubst  26308  mdegcl  26326  deg1nn0clb  26347  isuc1p  26398  plyeq0lem  26468  plyco  26499  plycj  26535  plycjOLD  26537  dvply2g  26547  dvnply2  26549  plydivlem4  26558  fta1lem  26569  fta1  26570  rnplynfin  26571  elqaalem1  26583  elqaalem2  26584  elqaalem3  26585  elqaa  26586  ulmcau  26663  radcnv0  26684  radcnvlt1  26686  radcnvle  26688  pserdvlem2  26696  coseq1  26794  efeq1  26797  sinord  26803  efif1olem2  26812  efif1olem4  26814  lognegb  26859  logcj  26875  argimgt0  26881  logtayl  26929  2irrexpq  27000  root1eq1  27024  logrec  27032  2irrexpqALT  27069  angrteqvd  27075  angpieqvdlem  27097  atans  27199  atans2  27200  dmarea  27226  areambl  27227  rlimcnp  27234  rlimcnp2  27235  xrlimcnp  27237  harmonicbnd  27272  harmonicbnd2  27273  lgamcvglem  27308  wilthlem2  27337  wilth  27339  efnnfsumcl  27371  vmacl  27386  efvmacl  27388  efchtdvds  27427  sqff1o  27450  fsumdvdscom  27453  musumsum  27460  fsumdvdsmul  27463  fsumvma  27481  perfect  27499  dchrelbasd  27507  lgsval  27569  lgsval2lem  27575  lgsdir2lem4  27596  lgsdir2  27598  lgsqrlem1  27614  lgsdchr  27623  m1lgs  27656  2lgs  27675  mul2sq  27687  2sqlem6  27691  2sqblem  27699  2sq2  27701  rplogsumlem2  27753  dchrisumlema  27756  dchrisumlem2  27758  dchrisumlem3  27759  dchrvmasumlem2  27766  dchrvmasumlem3  27767  dchrisum0flblem2  27777  dchrisum0flb  27778  dchrisum0fno1  27779  ostthlem1  27895  nodmon  27918  noextendseq  27935  nodense  27960  madefi  28210  addsproplem1  28266  addsproplem3  28268  addsprop  28273  addsf  28279  addbdaylem  28314  negsproplem1  28325  negsproplem3  28327  negsprop  28332  negbdaylem  28353  mulsproplemcbv  28412  mulsproplem1  28413  mulsproplem10  28422  mulsprop  28427  addonbday  28576  noseqp1  28588  noseqind  28589  peano5n0s  28616  dfn0s2  28629  n0addscl  28641  n0mulscl  28642  n0bday  28649  onsfi  28653  n0s0m1  28659  n0subs  28660  n0p1nns  28668  dfnns2  28669  nn1m1nns  28671  oldfib  28674  zaddscl  28691  zmulscld  28694  elzn0s  28695  peano5uzs  28701  expscllem  28727  z12addscl  28774  z12shalf  28777  z12negsclb  28778  z12zsodd  28779  z12bdaylem  28781  z12bday  28782  bdayfin  28784  mirval  29038  perpneq  29100  isperp2  29101  isperp2d  29102  foot  29108  islnopp  29126  islnoppd  29127  outpasch  29144  hlpasch  29145  ishpg  29148  colopp  29158  colhp  29159  lmif  29201  islmib  29203  lmiinv  29208  trgcopy  29222  trgcopyeu  29224  acopyeu  29253  inaghl  29275  tgasa1  29314  f1otrgitv  29358  f1otrg  29359  isfusgr  29810  opfusgr  29815  fusgrfisbase  29820  fusgrfisstep  29821  nbupgrel  29837  nbumgrvtx  29838  nbusgreledg  29845  edgnbusgreu  29859  nb3grprlem1  29872  uvtxusgrel  29895  cusgredg  29916  cplgr2vpr  29925  cusgrexg  29936  usgredgsscusgredg  29951  fusgrn0degnn0  29991  rusgrnumwrdl2  30078  rgrx0ndm  30085  wlkcomp  30122  wlkdlem2  30173  clwlkcomp  30277  iswwlks  30336  wwlknllvtx  30346  0enwwlksnge1  30364  wlkiswwlks2lem5  30373  wwlksm1edg  30381  wwlksnred  30392  wwlksnext  30393  wwlksnextbi  30394  wwlksnredwwlkn  30395  wwlksnextfun  30398  wwlksnextinj  30399  wwlksnextsurj  30400  wwlksnextbij  30402  wwlksnfi  30406  wwlksnextproplem2  30410  wwlksnextprop  30412  2wlkdlem4  30428  rusgrnumwwlkl1  30471  rusgrnumwwlks  30477  isclwwlk  30486  clwwlk1loop  30490  clwwlkccatlem  30491  clwlkclwwlklem2a1  30494  clwlkclwwlklem2a4  30499  clwlkclwwlklem2a  30500  clwlkclwwlklem2  30502  clwlkclwwlklem3  30503  clwlkclwwlk  30504  clwlkclwwlk2  30505  clwwisshclwwslemlem  30515  clwwisshclwwslem  30516  clwwisshclwws  30517  clwwlknlbonbgr1  30541  clwwlkinwwlk  30542  clwwlkn1  30543  loopclwwlkn1b  30544  clwwlkn1loopb  30545  clwwlkn2  30546  clwwlkel  30548  clwwlkf  30549  clwwlkwwlksb  30556  clwwlkext2edg  30558  wwlksext2clwwlk  30559  wwlksubclwwlk  30560  eleclclwwlknlem2  30563  umgr2cwwk2dif  30566  s2elclwwlknon2  30606  clwwlknonwwlknonb  30608  clwwlknonex2lem2  30610  clwwlknonex2  30611  loop1cycl  30655  3wlkdlem4  30674  upgr3v3e3cycl  30692  upgr4cycl4dv4e  30697  eupth2lem2  30731  eulerpathpr  30752  1vwmgr  30788  3vfriswmgrlem  30789  3vfriswmgr  30790  3cyclfrgrrn1  30797  vdgn1frgrv2  30808  frgrncvvdeqlem3  30813  frgrncvvdeqlem8  30818  frgrncvvdeqlem9  30819  frgrwopregasn  30828  frgrwopregbsn  30829  frgrwopreglem5ALT  30834  frgr2wwlk1  30841  frgr2wwlkeqm  30843  fusgr2wsp2nb  30846  2clwwlk2clwwlklem  30858  extwwlkfabel  30865  nvvop  31122  isnvlem  31123  sspval  31236  nmorepnf  31281  phpar  31337  siilem2  31365  bnsscmcl  31381  ubthlem1  31383  shaddcl  31730  shmulcl  31731  hsn0elch  31761  hhssablo  31776  hhssnvt  31778  hhsssh  31782  shscl  31831  shintcl  31843  chintcl  31845  shincl  31894  chincl  32012  h1datomi  32094  chscllem2  32151  sumspansn  32162  spansncvi  32165  5oalem2  32168  5oalem3  32169  pjini  32212  pjjsi  32213  eigposi  32349  nmoprepnf  32380  nmfnrepnf  32393  dmadjrnb  32419  lnophmlem1  32529  lnophm  32532  nmcopex  32542  lnconi  32546  nmbdfnlb  32563  nmcfnex  32566  imaelshi  32571  rnbra  32620  leopg  32635  pjbdlni  32662  pjhmop  32663  hmopidmch  32666  pjclem4  32712  pj3si  32720  strlem1  32763  atssma  32891  atcv0eq  32892  atcv1  32893  atomli  32895  atcvatlem  32898  cdj3lem2a  32949  cdj3lem3a  32952  xppreima  33150  fmptcof2  33162  aciunf1lem  33167  funcnv4mpt  33173  1stpreimas  33210  f1od2  33222  fpwrelmapffslem  33235  xrofsup  33270  fzspl  33292  fzsplit3  33296  nnindf  33322  fprodex01  33327  fsumiunle  33331  indf1ofs  33344  gsumhashmul  33539  fzto1st  33575  fxpsubm  33644  fxpsubg  33645  fxpsubrg  33646  isslmd  33674  slmdlema  33675  elrgspnlem2  33715  elrgspnlem4  33717  rlocisunit  33748  subsdrg  33771  qusker  33821  0nellinds  33837  unitprodclb  33855  nsgmgclem  33873  nsgmgc  33874  nsgqusf1olem2  33876  elrspunidl  33889  opprlidlabs  33920  dfufd2lem  33992  psrbasfsupp  34054  selvply1rhmlemb  34062  mplidomlem  34070  lindsunlem  34167  brfldext  34188  brfinext  34195  finextfldext  34207  finexttrb  34208  extdg1id  34209  fldextrspunlsplem  34216  constrconj  34288  constrfin  34289  trisecnconstr  34335  smatrcl  34339  submateq  34352  lmatfval  34357  lmatcl  34359  qtophaus  34379  locfinreflem  34383  locfinref  34384  zartopn  34418  zarcmplem  34424  rhmpreimacnlem  34427  xpinpreima  34449  xpinpreima2  34450  cnre2csqlem  34453  tpr2rico  34455  prsdm  34457  prsrn  34458  ordtrest2NEWlem  34465  ordtrest2NEW  34466  zrhcntr  34522  qqhval2  34525  isrrext  34543  ismntoplly  34568  esumcvg  34629  sigaval  34654  issiga  34655  0elsiga  34657  sigaclcu  34660  issgon  34666  prsiga  34674  sigaclci  34675  difunielsiga  34676  unelsiga  34677  ispisys2  34697  inelpisys  34698  unelldsys  34702  sigapildsyslem  34705  sigapildsys  34706  ldgenpisyslem1  34707  ldgenpisys  34710  isros  34712  unelros  34715  difelros  34716  fiunelros  34718  inelsros  34722  diffiunisros  34723  rossros  34724  measvuni  34758  measiun  34762  voliune  34773  volfiniune  34774  brfae  34792  ismbfm  34795  mbfmcnvima  34799  mbfmcst  34803  1stmbfm  34804  2ndmbfm  34805  imambfm  34806  sitgval  34876  issibf  34877  sibfima  34882  sitgfval  34885  sitgclg  34886  eulerpartlemelr  34901  eulerpartlemsf  34903  eulerpartleme  34907  eulerpartlemt0  34913  eulerpartlemt  34915  eulerpartgbij  34916  eulerpartlemr  34918  eulerpartlemmf  34919  eulerpartlemgvv  34920  eulerpartlemgs2  34924  eulerpartlemn  34925  eulerpart  34926  cndprobprob  34982  rrvsum  34998  orvcelel  35014  ballotlemodife  35042  ballotlemsdom  35056  ballotlemrv  35064  ballotlemrv1  35065  ballotlemrv2  35066  ballotlem1ri  35079  fsum2dsub  35148  reprinfz1  35163  reprpmtf1o  35167  reprdifc  35168  breprexplema  35171  hgt750lema  35198  hgt750leme  35199  bnj149  35417  bnj222  35425  bnj1112  35525  bnj1148  35538  fissorduni  35627  fineqvrep  35683  fineqvnttrclse  35693  fineqvinfep  35694  kardnnfi  35738  gblacfnacd  35782  vonf1wev  35788  vonf1owevOLD  35790  vonf1osev  35792  vonf1oonfo  35795  subfacp1lem3  35844  subfacp1lem6  35847  erdszelem10  35862  kur14  35878  cvxsconn  35905  cnllysconn  35907  resconn  35908  iscvm  35921  cvmliftlem5  35951  cvmliftlem15  35960  cvmlift2lem1  35964  cvmlift2lem12  35976  cvmlift2lem13  35977  sat1el2xp  36041  fmlasuc  36048  gonan0  36054  gonar  36057  satefvfmla0  36080  msubrn  36191  msubco  36193  ismfs  36211  mvtinf  36217  mclsax  36231  mppspstlem  36233  elmpps  36235  nnuni  36389  dfdm5  36435  dfrn5  36436  elima4  36438  rdgprc0  36453  pprodss4v  36544  elfuns  36575  fnimage  36589  imageval  36590  fwddifval  36825  fwddifnval  36826  fwddifnp1  36828  hfninf  36833  nmulprop  36837  filnetlem4  37067  onsucconn  37124  onsucsuccmp  37130  limsucncmp  37132  onint1  37135  fveleq  37137  findreccl  37139  nndivsub  37143  weiunse  37154  mh-inf3f1  37227  mh-infprim2bi  37233  mh-infprim3bi  37234  bj-seex  37732  bj-adjg1  37854  bj-mooreset  37919  bj-ismoored0  37923  bj-ismoored  37924  bj-inftyexpitaudisj  38022  bj-inftyexpidisj  38027  bj-isvec  38104  bj-isclm  38108  csbmpo123  38150  topdifinffinlem  38166  topdifinffin  38167  csbfinxpg  38207  phpreu  38423  finixpnum  38424  poimirlem16  38450  poimirlem17  38451  poimirlem19  38453  poimirlem20  38454  poimirlem22  38456  poimirlem23  38457  poimirlem24  38458  poimirlem25  38459  poimirlem26  38460  poimirlem28  38462  poimirlem29  38463  poimirlem30  38464  poimirlem31  38465  poimirlem32  38466  poimir  38467  mblfinlem3  38473  ex-ovoliunnfl  38477  voliunnfl  38478  volsupnfl  38479  mbfresfi  38480  itgabsnc  38503  ftc1anclem6  38512  ftc1anclem7  38513  ftc1anclem8  38514  ftc1anc  38515  dvasin  38518  sdclem2  38557  fdc  38560  incsequz  38563  neificl  38568  mettrifi  38572  cntotbnd  38611  cnpwstotbnd  38612  ismtyima  38618  ismtyhmeolem  38619  heiborlem2  38627  heiborlem3  38628  heiborlem4  38629  heiborlem5  38630  heiborlem6  38631  heiborlem10  38635  isrngo  38712  isdivrngo  38765  drngoi  38766  idlval  38828  isidlc  38830  idladdcl  38834  idllmulcl  38835  idlrmulcl  38836  0idl  38840  pridlval  38848  smprngopr  38867  prnc  38882  ispridlc  38885  pridlc  38886  eqrelf  39071  iss2  39157  elcoeleqvrels  39492  elfunsALTV  39590  eldisjs  39632  eleldisjs  39641  fsumshftd  39890  riotaclbgBAD  39892  renegclALT  39901  lshpinN  39927  isopos  40118  oposlem  40120  glbconN  40315  lnnat  40365  2at0mat0  40463  islvol2aN  40530  dalawlem13  40821  pclfinclN  40888  lhpoc2N  40953  ltrncnvatb  41076  cdleme11h  41204  cdlemefr32sn2aw  41342  cdlemefs32sn1aw  41352  cdleme32fvaw  41377  cdlemg1fvawlemN  41511  dicelvalN  42116  dih1dimatlem  42267  dihlatat  42275  dihjatcclem4  42359  islpolN  42421  lpolsatN  42426  lpolpolsatN  42427  mapdordlem1a  42572  mapdordlem1  42574  mapdhcl  42665  iscsrg  42902  fzsplitnd  42913  lcmineqlem12  42971  intlewftc  42992  dvrelogpow2b  42999  aks4d1p1p3  43000  aks4d1p1p2  43001  aks4d1p1p4  43002  dvle2  43003  aks4d1p8  43018  aks4d1p9  43019  isprimroot  43024  primrootsunit1  43028  primrootscoprmpow  43030  aks6d1c1p1  43038  aks6d1c1p2  43040  aks6d1c1p3  43041  evl1gprodd  43048  hashscontpow  43053  aks6d1c3  43054  aks6d1c2  43061  sticksstones1  43077  sticksstones10  43086  sticksstones11  43087  sticksstones12a  43088  aks6d1c6lem1  43101  unitscyglem5  43130  retire  43259  reelznn0nn  43414  fsuppind  43501  fsuppssindlem2  43503  fsuppssind  43504  isnacs3  43620  nacsfix  43622  mzpclval  43635  mzpcl1  43639  mzpcl2  43640  mzpcl34  43641  mzpexpmpt  43655  mzpsubst  43658  diophin  43682  diophun  43683  2rexfrabdioph  43702  3rexfrabdioph  43703  4rexfrabdioph  43704  6rexfrabdioph  43705  7rexfrabdioph  43706  rabdiophlem2  43708  diophren  43719  fphpd  43722  fphpdo  43723  fiphp3d  43725  pellexlem1  43735  pell14qrexpclnn0  43772  pellqrex  43785  rmspecnonsq  43813  monotuz  43847  monotoddzzfi  43848  monotoddzz  43849  oddcomabszz  43850  modabsdifz  43892  rmxdioph  43922  expdiophlem2  43928  limsuc2  43947  dfac11  43968  kelac1  43969  dfac21  43972  lsmfgcl  43980  islnm  43983  lnmlssfg  43986  lmhmfgima  43990  pwslnm  44000  unxpwdom3  44001  pwfi2f1o  44002  islnr  44017  hbtlem2  44030  cnsrexpcl  44071  flcidc  44076  mendlmod  44095  proot1ex  44102  oaordnr  44202  omnord1  44211  oenord1  44222  cantnfresb  44230  onmcl  44237  tfsnfin  44258  nadd2rabtr  44290  nadd1rabtr  44294  nadd1rabex  44296  nadd1suc  44298  pwelg  44465  fipjust  44470  elnonrel  44490  elinlem  44503  elcnvlem  44506  ss2iundf  44564  dfhe3  44680  dffrege115  44883  rfovcnvf1od  44909  ntrneiel2  44991  clsneiel2  45014  neicvgel2  45025  grur1cld  45135  dvgrat  45201  cvgdvgrat  45202  radcnvrat  45203  binomcxplemdvsum  45244  binomcxplemnotnn0  45245  orbitcl  45845  modelaxreplem1  45866  modelaxreplem2  45867  modelaxrep  45869  fnchoice  45928  fiiuncl  45964  disjf1  46080  disjinfi  46089  choicefi  46096  axccdom  46117  fmptf  46133  fmptff  46163  monoords  46195  supminfrnmpt  46338  supxrleubrnmptf  46344  supminfxr  46357  supminfxr2  46362  supminfxrrnmpt  46364  monoordxrv  46374  monoordxr  46375  monoord2xrv  46376  monoord2xr  46377  caucvgbf  46382  cvgcaule  46384  fsummulc1f  46466  fsumnncl  46467  fsumf1of  46469  fsumreclf  46471  fsumlessf  46472  fsumsermpt  46474  fmul01  46475  fmulcl  46476  fmuldfeqlem1  46477  fmuldfeq  46478  fmul01lt1lem1  46479  fmul01lt1lem2  46480  fprodexp  46489  fprodabs2  46490  mccllem  46492  mccl  46493  fprodcnlem  46494  fprodcn  46495  climmulf  46499  climsuse  46503  climrecf  46504  climaddf  46510  climf  46517  sumnnodd  46525  clim2f  46529  0ellimcdiv  46542  climsubmpt  46553  climreclf  46557  climf2  46559  fnlimcnv  46560  climeldmeqmpt  46561  clim2f2  46563  climfveqmpt  46564  fnlimfvre  46567  fnlimabslt  46572  climfveqmpt3  46575  climbddf  46580  climeldmeqmpt3  46582  climinf2mpt  46607  climinfmpt  46608  limsupequzmptf  46624  lmbr3  46640  liminfreuzlem  46695  coseq0  46757  cncfshift  46767  cncfperiod  46772  fprodcncf  46793  ioodvbdlimc1lem2  46825  ioodvbdlimc2lem  46827  dvmptmulf  46830  dvnmptdivc  46831  dvnmul  46836  dvmptfprod  46838  iblspltprt  46866  itgspltprt  46872  stoweidlem2  46895  stoweidlem3  46896  stoweidlem4  46897  stoweidlem6  46899  stoweidlem8  46901  stoweidlem17  46910  stoweidlem19  46912  stoweidlem20  46913  stoweidlem21  46914  stoweidlem23  46916  stoweidlem27  46920  stoweidlem35  46928  stoweidlem42  46935  stoweidlem43  46936  stoweidlem62  46955  stoweid  46956  wallispilem3  46960  wallispi  46963  fourierdlem16  47016  fourierdlem21  47021  fourierdlem41  47041  fourierdlem42  47042  fourierdlem48  47047  fourierdlem49  47048  fourierdlem50  47049  fourierdlem51  47050  fourierdlem54  47053  fourierdlem63  47062  fourierdlem64  47063  fourierdlem65  47064  fourierdlem71  47070  fourierdlem72  47071  fourierdlem73  47072  fourierdlem83  47082  fourierdlem86  47085  fourierdlem89  47088  fourierdlem90  47089  fourierdlem91  47090  fourierdlem96  47095  fourierdlem97  47096  fourierdlem98  47097  fourierdlem99  47098  fourierdlem100  47099  fourierdlem103  47102  fourierdlem104  47103  fourierdlem105  47104  fourierdlem108  47107  fourierdlem109  47108  fourierdlem110  47109  fourierdlem112  47111  fourierdlem113  47112  etransclem24  47151  salunicl  47209  saluncl  47210  saldifcl  47212  sge0f1o  47275  sge0lempt  47303  sge0iunmptlemfi  47306  sge0p1  47307  sge0fodjrnlem  47309  sge0iunmpt  47311  sge0ltfirpmpt2  47319  sge0isummpt2  47325  sge0xaddlem2  47327  sge0xadd  47328  ismea  47344  nnfoctbdjlem  47348  nnfoctbdj  47349  meadjiun  47359  voliunsge0lem  47365  meaiuninclem  47373  meaiuninc3v  47377  hoidmvlelem2  47489  hoidmvlelem3  47490  vonvolmbl2  47556  hoimbl2  47558  vonhoire  47565  vonicclem2  47577  vonn0ioo2  47583  vonn0icc2  47585  salpreimagelt  47600  salpreimalegt  47602  salpreimagtge  47618  salpreimaltle  47619  issmf  47621  salpreimagtlt  47623  smfpreimalt  47624  smfpreimaltf  47629  issmfle  47638  smfpreimale  47647  issmfgt  47649  smfpreimagt  47655  issmfgelem  47662  issmfge  47663  smflimlem4  47667  smflim  47670  smfpreimage  47675  smfresal  47681  smfpimbor1lem1  47691  smfpimbor1lem2  47692  smflim2  47699  smflimmpt  47703  smflimsuplem1  47713  smflimsuplem2  47714  smflimsuplem3  47715  smflimsuplem5  47717  smflimsuplem7  47719  smflimsup  47721  smfliminf  47724  ormkglobd  47770  eu2ndop1stv  48078  dmfcoafv  48128  ffnaov  48152  faovcl  48153  funressndmafv2rn  48176  dfatdmfcoafv2  48207  mod2addne  48323  smonoord  48330  iccpartiltu  48387  iccpartigtl  48388  sprsymrelf1lem  48456  prproropf1olem2  48469  fmtno4prmfac193  48541  proththdlem  48581  proththd  48582  iseven  48609  isodd  48610  dfodd2  48617  evenm1odd  48620  evenp1odd  48621  enege  48626  onego  48627  epee  48686  perfectALTV  48704  bgoldbtbndlem2  48787  bgoldbtbndlem3  48788  bgoldbtbndlem4  48789  bgoldbtbnd  48790  clnbupgrel  48815  edgusgrclnbfin  48823  grimuhgr  48868  uhgrimedgi  48871  uhgrimprop  48873  isuspgrim0  48875  isuspgrimlem  48876  grimedg  48916  grtriproplem  48920  grtrif1o  48923  isgrtri  48924  grtriclwlk3  48926  cycl3grtrilem  48927  cycl3grtri  48928  grimgrtri  48930  usgrgrtrirex  48931  isubgr3stgrlem7  48953  grlimprclnbgrvtx  48980  grlimgredgex  48981  grlimgrtri  48984  usgrexmpl1tri  49006  gpgvtxel2  49029  gpgvtx0  49034  gpgvtx1  49035  gpgedgvtx0  49042  gpgedgvtx1  49043  gpgedgiov  49046  gpgedg2ov  49047  gpgedg2iv  49048  gpgnbgrvtx0  49055  gpgnbgrvtx1  49056  gpg3kgrtriex  49070  gpgprismgr4cycllem3  49078  pgnbgreunbgrlem1  49094  pgnbgreunbgrlem2lem1  49095  pgnbgreunbgrlem2lem2  49096  pgnbgreunbgrlem2lem3  49097  pgnbgreunbgrlem4  49100  pgnbgreunbgrlem5lem1  49101  pgnbgreunbgrlem5lem2  49102  pgnbgreunbgrlem5lem3  49103  pgnbgreunbgr  49106  grlimedgnedg  49112  uzlidlring  49215  smprngprmrng  49319  cbvmpox2  49331  lmod1  49487  nnolog2flm1  49585  dignn0flhalflem1  49610  catprsc  50004  nelsubc3lem  50061  fucofulem2  50302  fucofvalne  50316  isthincd2lem2  50426  euendfunc  50517  cnelsubclem  50594