Theorem eleq1d 2850

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

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 2148  ax-9 2156  ax-ext 2737

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

This theorem is used by:  eleq1  2853  eleq12d  2859  eqeltrd  2865  eqneltrd  2885  rspcimdv  3573  reuind  3718  sbcel2  4383  sbccsb2  4402  disjiun  5099  breq1  5114  breq2  5115  axrep6g  5253  inex1g  5290  intex  5316  pwexg  5351  reusv2lem4  5374  reusv2  5376  reusv3  5378  rabxfrd  5390  prexOLD  5416  opelopabsb  5516  csbmpt12  5544  pofun  5589  seex  5622  seinxp  5747  opabid2  5817  opeliunxp2  5826  elrn2g  5882  opeldmd  5898  opeldm  5899  elreldm  5927  elsnres  6022  iss  6039  unielrel  6278  onunel  6472  funopg  6574  brprcneu  6875  brprcneuALT  6876  tz6.12f  6910  ndmfvrcl  6918  ssimaex  6970  dmfco  6981  fvmpti  6992  fvmpt3  6998  fvmptf  7015  fvmptss2  7020  respreima  7065  fvn0ssdmfun  7073  fvelrn  7075  ffnfvf  7119  ffvresb  7125  fmptco  7129  fmptcof  7130  fsn  7135  fsn2g  7138  fressnfv  7163  fvrnressn  7164  fnex  7222  funfvima  7235  funfvima3  7241  f1mpt  7264  fliftfuns  7321  isoselem  7348  isowe2  7357  riotaclb  7417  ovrspc2v  7445  ffnov  7545  fovcld  7546  ovmpos  7567  ov2gf  7568  ovg  7584  funimassov  7597  oprssdm  7601  ndmovrcl  7606  caovclg  7612  elovmpo  7665  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  8062  fmpox  8070  offval22  8089  frxp  8128  fnse  8135  frxp2  8146  sexp2  8148  frxp3  8153  sexp3  8155  opeliunxp2f  8212  dftpos4  8247  fvmpocurryd  8273  undefnel2  8280  onnseq  8337  smoel  8353  smo11  8357  tfrlem8  8377  tfrlem9  8378  tfrlem15  8385  tfr2b  8389  tz7.44-2  8400  tz7.44-3  8401  oacl  8526  omcl  8527  oecl  8528  oaord1  8542  omordi  8557  oen0  8578  oeeui  8594  nnacl  8603  nnmcl  8604  nnecl  8605  nnmordi  8623  nnaordex  8630  omsmolem  8649  naddcllem  8668  naddov2  8671  naddf  8674  naddssim  8678  naddelim  8679  naddasslem1  8687  naddasslem2  8688  naddsuc2  8694  erexb  8726  elecex  8751  qliftfuns  8808  ixpsnval  8904  elixp2  8905  resixp  8937  undifixp  8938  mptelixpg  8939  resixpfo  8940  elixpsn  8941  fundmen  9035  fopwdom  9080  disjen  9129  xpf1o  9134  unfi  9162  cnvfi  9167  fnfi  9169  f1oenfirn  9171  f1domfi  9172  unblem2  9260  pwfi  9285  fiint  9293  iunfi  9307  tfsnfin2  9327  isfsupp  9332  fsuppun  9354  ffsuppbi  9365  elfi2  9381  wdom2d  9549  ixpiunwdom  9559  dfom3  9623  cantnfvalf  9641  cantnflt  9648  cantnflem1  9665  r1fin  9752  tz9.12lem3  9768  ranksnb  9806  ranklim  9823  r1pw  9824  r1pwALT  9825  r1pwcl  9826  rankuni2b  9832  djuexb  9911  cardmin2  10001  infxpenc2lem1  10019  dfac8alem  10029  dfac8clem  10032  ac5num  10036  acni2  10046  acnlem  10048  alephon  10069  alephfplem3  10106  alephfplem4  10107  dfac4  10122  dfac5lem1  10123  dfac5lem5  10127  dfac2a  10129  dfac2b  10130  dfacacn  10141  dfac12lem2  10144  dfac12r  10146  dfac12k  10147  cofsmo  10268  cfsmolem  10269  isfin1a  10291  fin1ai  10292  isfin3  10295  infpssrlem3  10304  fin23lem7  10315  fin23lem11  10316  enfin2i  10320  isf34lem4  10376  fin1a2lem7  10405  hsmexlem9  10424  hsmexlem4  10428  hsmex  10431  axcc2lem  10435  axcc3  10437  axdc3lem2  10450  axcclem  10456  zornn0g  10504  ttukeylem3  10510  ttukeylem6  10513  ttukey2g  10515  brdom7disj  10531  brdom6disj  10532  fnct  10539  fnctOLD  10540  konigthlem  10572  axregndlem2  10607  axinfnd  10610  axacndlem5  10615  axacnd  10616  fpwwe2lem4  10638  fpwwe2lem12  10646  fpwwe  10650  pwfseqlem1  10662  pwfseqlem3  10664  pwfseqlem4a  10665  pwfseqlem4  10666  wununi  10710  wunpw  10711  wunpr  10713  wunr1om  10723  tskpw  10757  tskr1om  10771  inar1  10779  grupw  10799  grupr  10801  gruurn  10802  gruiun  10803  ingru  10819  grur1a  10823  grothomex  10833  grothac  10834  addnidpi  10905  indpi  10911  adderpq  10960  mulerpq  10961  addclprlem2  11021  mulclprlem  11023  distrlem4pr  11030  prlem934  11037  ltexprlem3  11042  ltexprlem4  11043  ltexprlem7  11046  ltexpri  11047  prlem936  11051  reclem2pr  11052  reclem3pr  11053  addclsr  11087  mulclsr  11088  supsrlem  11115  supsr  11116  axaddf  11149  axmulf  11150  axaddrcl  11156  axmulrcl  11158  renegcl  11540  negreb  11542  negn0  11662  negf1o  11663  ltord1  11759  leord1  11760  eqord1  11761  ltord2  11762  leord2  11763  eqord2  11764  negfi  12183  infm3  12193  cju  12233  indfval  12244  peano5nni  12255  peano2nn  12264  dfnn2  12265  nn1m1nn  12273  nnaddcl  12275  nnmulcl  12276  nnsub  12299  nndivtr  12302  un0addcl  12556  un0mulcl  12557  elnnnn0  12566  nn0sub  12573  fcdmnn0fsuppg  12583  elz  12612  nnnegz  12613  elz2  12628  znegclb  12650  zaddcl  12653  nzadd  12661  zmulcl  12662  zneo  12699  nneo  12700  zeo  12702  peano5uzi  12705  zindd  12717  uzp1  12919  uzaddcl  12948  ublbneg  12977  eqreznegel  12978  supminf  12979  zsupss  12981  qmulz  12995  qnegcl  13010  irradd  13017  irrmul  13018  xnn0xaddcl  13281  fzrev2  13637  injresinjlem  13840  negmod0  13933  om2uzuzi  14007  uzindi  14040  fsuppmapnn0ub  14053  mptnn0fsuppr  14057  seqexw  14075  seqcl2  14078  seqcl  14080  seqf  14081  monoord  14090  monoord2  14091  sermono  14092  seqsplit  14093  seqcaopr2  14096  seqid3  14104  seqhomo  14107  expcllem  14130  expcl2lem  14131  m1expcl2  14143  faccl  14341  facdiv  14345  facndiv  14346  bccmpl  14367  bccl  14380  hashclb  14416  hasheq0  14421  hashfn  14433  seqcoll  14523  opfi1uzind  14570  ccatalpha  14654  reuccatpfxs1lem  14809  reuccatpfxs1  14810  repswccat  14851  repswrevw  14852  2cshw  14878  2cshwcshw  14890  cshimadifsn  14894  cshco  14901  swrd2lsw  15017  wwlktovf  15021  wwlktovf1  15022  wwlktovfo  15023  wrd2f1tovbij  15025  shftlem  15133  shftf  15144  cjval  15181  cjth  15182  remim  15196  cnpart  15319  uzin2  15424  caubnd2  15437  sqreulem  15439  clim  15573  clim2  15583  lo1o12  15612  climrlim2  15626  lo1resb  15643  o1resb  15645  lo1eq  15647  climmpt2  15652  climshftlem  15653  rlimcld2  15657  climcn1  15671  climcn2  15672  o1dif  15709  iserex  15736  climub  15741  climserle  15742  isercoll  15747  climcau  15750  caurcvg2  15757  caucvgb  15759  summolem3  15792  summolem2a  15793  zsum  15796  fsum  15798  sumss2  15804  fsumcvg2  15805  fsumclf  15816  fsumsplitf  15820  fsumsplit1  15823  sumpr  15826  sumtp  15827  fsumm1  15829  fsum1p  15831  isummulc2  15840  fsum2dlem  15848  fsumcom2  15852  fsumshftm  15859  fsum0diag2  15861  fsumge1  15876  fsum00  15877  fsumabs  15880  telfsumo  15881  telfsumo2  15882  fsumparts  15885  fsumrlim  15890  fsumo1  15891  o1fsum  15892  fsumiun  15900  binomlem  15910  isumshft  15920  isum1p  15922  isumrpcl  15924  climcndslem1  15930  climcndslem2  15931  climcnds  15932  infcvgaux2i  15939  cvgrat  15964  mertens  15967  clim2prod  15969  prodfn0  15975  prodfrec  15976  prodfdiv  15977  ntrivcvgfvn0  15980  prodmolem3  16014  prodmolem2a  16015  zprod  16018  fprod  16022  prodss  16028  fprodser  16030  fprodm1  16048  fprod1p  16049  fprodm1s  16051  fprodp1s  16052  fprodabs  16055  fprodn0  16060  fprod2dlem  16061  fprodcnv  16064  fprodcom2  16065  fproddivf  16068  fprodsplitf  16069  fprodsplit1f  16071  bpolycl  16132  fprodefsum  16175  rpnnen2lem11  16306  mod2eq1n2dvds  16431  mulsucdiv2z  16437  zob  16443  nn0o1gt2  16465  nno  16466  nn0o  16467  divalglem7  16483  bitsf1  16530  sadcp1  16539  smupp1  16564  qnumdencl  16824  iserodd  16921  pcqcl  16942  pcxnn0cl  16946  pcxcl  16947  pcgcd1  16963  dvdsprmpweqle  16972  pcmpt  16978  pcmpt2  16979  pcmptdvds  16980  infpnlem2  16997  infpn2  16999  1arith  17013  elgz  17017  mul4sq  17040  4sqlem13  17043  4sqlem17  17047  4sqlem18  17048  4sqlem19  17049  vdwlem1  17067  vdwlem2  17068  vdwnn  17084  ramtcl2  17097  ramcl  17115  prmonn2  17125  prmodvdslcmf  17133  isstruct2  17235  wunress  17335  firest  17511  imasaddfnlem  17608  imasvscafn  17617  xpsfrnel2  17644  mreintcl  17673  ismred2  17681  mreexexlemd  17726  mreexexlem3d  17728  mreexexlem4d  17729  iscatd2  17763  catpropd  17791  subsubc  17936  isfunc  17947  inclfusubc  18026  fncnvimaeqv  18202  joindef  18456  joinval  18457  meetdef  18470  meetval  18471  oduclatb  18589  acsdrsel  18625  isacs4lem  18626  isacs5lem  18627  acsdrscl  18628  mgmsscl  18729  mgmn0plusgf  18735  mgmpropd  18737  mgm1  18744  gsumvalx  18770  issubmgm  18796  issubmgm2  18797  mgmhmima  18809  sgrppropd  18825  mndpropd  18856  issubm  18902  0subm  18917  insubm  18918  mhmimalem  18924  gsumwsubmcl  18937  gsumwspan  18946  symggrplem  18984  sursubmefmnd  18996  injsubmefmnd  18997  smndex1basss  19008  degenmgm  19041  degenmgm2nfun  19043  degenmgm2  19044  mulgsubcl  19202  issubg  19240  issubg2  19256  issubg4  19260  0subg  19266  isnsg  19269  isnsg2  19270  nsgbi  19271  isnsg3  19274  elnmz  19277  nmzbi  19278  nmzsubg  19279  eqgval  19293  eqgid  19296  cycsubgcl  19325  ghmrn  19347  ghmnsgima  19358  gass  19419  oppgsubg  19481  f1omvdconj  19564  symgfisg  19586  psgneldm  19621  0subgALT  19686  odhash3  19694  sylow2blem2  19739  lsmsubm  19771  lsmsubg  19772  efgsf  19847  efgsdm  19848  efgs1b  19854  efgredlema  19858  eqgabl  19952  ablnsg  19965  cyggenod2  20003  gsumzaddlem  20039  gsummhm2  20057  gsum2dlem2  20089  gsum2d2lem  20091  gsumcom2  20093  dprdfeq0  20142  dprdsubg  20144  dprd2da  20162  ablfacrp  20186  pgpfac1lem3  20197  pgpfaclem1  20201  ablfaclem3  20207  ablfac2  20209  cycsubggenodd  20229  isrng  20280  issrg  20318  srgfcl  20326  rglcom4d  20341  srgbinomlem4  20359  isring  20367  iscrng  20370  dvdsr  20494  irredrmul  20559  isrngim  20577  isrim0  20615  issubrng  20700  subrngringnsg  20706  issubrng2  20711  rhmimasubrnglem  20718  issubrg  20724  issubrg2  20745  subrgpropd  20761  isdrngd  20922  isdrngdOLD  20924  issdrg  20945  sdrgacs  20958  issrngd  21012  islmod  21039  lmodlema  21040  islmodd  21041  lmodprop2d  21099  rmodislmodlem  21104  rmodislmod  21105  lssset  21108  islssd  21110  lsscl  21117  lsslss  21136  lsspropd  21192  lmhmima  21222  lbsind  21255  lsmcl  21258  islvec  21279  lmhmlvec  21285  lspsolvlem  21320  lspsolv  21321  lvecpropd  21345  rnglidlmcl  21395  rnglidl0  21409  rnglidlmmgm  21433  df2idl2crng  21475  rngqiprngimf1lem  21488  rngqiprngimf1  21494  ring2idlqus  21503  prmidlval  21516  prmidlc  21527  prmidlprop  21530  xrsdsreclblem  21617  xrsdsreclb  21618  cnsubrglem  21621  prmirred  21678  pzriprnglem4  21688  pzriprnglem8  21692  pzriprngALT  21699  znunithash  21768  cofipsgn  21797  zrhpsgnelbas  21798  rzgrp  21827  isphl  21832  phllmhm  21836  ipcl  21837  isphld  21858  phlpropd  21859  phlssphl  21863  cssincl  21892  pjdm  21911  dsmmval  21938  dsmmbas2  21941  dsmmelbas  21943  frlmbas  21959  frlmup1  22002  lindfind  22020  lindsind  22021  f1lindf  22026  islindf4  22042  psrbag  22121  psrbaglefi  22130  mplsubglem  22202  mpllsslem  22203  ltbwe  22249  psrbagsn  22268  subrgasclcl  22272  mplind  22275  mpfind  22320  psdmul  22383  coe1mul2lem2  22483  gsumply1eq  22523  evl1vsd  22558  mpfpf1  22565  pf1mpf  22566  pf1ind  22569  matecl  22636  m1detdiag  22808  mdetralt  22819  mdetralt2  22820  mdetunilem2  22824  mdetunilem9  22831  m2detleiblem3  22840  m2detleiblem4  22841  smadiadetlem0  22872  cpmatacl  22927  chpscmat  23053  uniopn  23108  inopn  23110  fiinopn  23112  istps  23145  fctop  23215  iscld  23238  isopn2  23243  mretopd  23303  iscldtop  23306  perfi  23366  tgrest  23370  restcld  23383  ordtbaslem  23399  ordtrest2lem  23414  ordtrest2  23415  iscn  23446  cnpval  23447  iscnp  23448  tgcn  23463  subbascn  23465  ssidcn  23466  lmbrf  23471  cnpnei  23475  cnima  23476  iscncl  23480  cnconst2  23494  cnrest2  23497  cnpresti  23499  cnprest  23500  cnindis  23503  lmres  23511  lmcnp  23515  iscnrm  23534  t1sncld  23537  cnrmi  23571  cncmp  23603  cmpsublem  23610  fiuncmp  23615  unconn  23640  conncompid  23642  conncompconn  23643  conncompss  23644  1stcfb  23656  2ndcrest  23665  2ndcctbss  23667  2ndcdisj  23668  1stccnp  23674  islly  23680  isnlly  23681  subislly  23693  restnlly  23694  restlly  23695  islly2  23696  hausllycmp  23706  cldllycmp  23707  dislly  23709  isptfin  23728  islocfin  23729  ptfinfin  23731  finlocfin  23732  dissnlocfin  23741  locfindis  23742  comppfsc  23744  kgenval  23747  elkgen  23748  kgeni  23749  cmpkgen  23763  1stckgenlem  23765  kgencn2  23769  ptpjpre1  23783  elpt  23784  elptr  23785  ptbasin  23789  xkobval  23798  xkoval  23799  xkoopn  23801  txbasval  23818  tx1cn  23821  tx2cn  23822  dfac14  23830  xkoccn  23831  txcnp  23832  ptcnplem  23833  txcnmpt  23836  txindislem  23845  txdis1cn  23847  txlly  23848  txnlly  23849  pthaus  23850  ptrescn  23851  hauseqlcld  23858  txlm  23860  tx2ndc  23863  txkgen  23864  xkoptsub  23866  xkopt  23867  xkoco1cn  23869  xkoco2cn  23870  xkococnlem  23871  xkococn  23872  cnmpt11  23875  cnmpt12  23879  cnmpt21  23883  cnmpt22  23886  cnmptkp  23892  cnmptk1p  23897  xkoinjcn  23899  txconn  23901  qtopval2  23908  elqtop  23909  idqtop  23918  qtopcld  23925  qtopeu  23928  qtoprest  23929  qtopomap  23930  qtopcmap  23931  ishmeo  23971  hmeoopn  23978  hmeocld  23979  ordthmeolem  24013  ptcmpfi  24025  elmptrab  24039  fgcl  24090  trfil2  24099  cfinfil  24105  uzrest  24109  ufilss  24117  trufil  24122  cfinufil  24140  ufinffr  24141  ufildr  24143  rnelfm  24165  flfcntr  24255  ptcmplem2  24265  ptcmplem3  24266  ptcmplem4  24267  ptcmplem5  24268  cnextfvval  24277  tmdcn2  24301  tmdmulg  24304  tmdgsum2  24308  symgtgp  24318  opnsubg  24320  clssubg  24321  tgpconncompeqg  24324  ghmcnp  24327  tgphaus  24329  tgpt0  24331  qustgpopn  24332  qustgplem  24333  tsmsgsum  24351  tsmssubm  24355  tsmsres  24356  tsmsf1o  24357  tsmsxplem1  24365  tsmsxplem2  24366  tsmsxp  24367  istrg  24376  istdrg  24378  istdrg2  24390  istlm  24397  istvc  24404  ustval  24415  ustincl  24420  ustdiag  24421  ustinvel  24422  ustexhalf  24423  ust0  24432  ucnima  24492  fmucndlem  24502  prdsdsf  24579  prdsxmet  24581  imasf1oxmet  24587  imasf1omet  24588  prdsxmslem2  24741  metustsym  24767  isnlm  24887  qtopbaslem  24970  xrtgioo  25019  reperflem  25031  fsumcn  25084  expcn  25086  xrhmeo  25160  cnllycmp  25170  bndth  25172  isclm  25278  lmhmclm  25301  lmmcvg  25475  fmcfil  25486  iscfil3  25487  iscau2  25491  iscau4  25493  iscmet3lem1  25505  iscmet3  25507  cfilres  25510  caussi  25511  equivcfil  25513  flimcfil  25528  bcthlem1  25538  isbn  25552  srabn  25574  ishl2  25584  cmslssbn  25586  cmscsscms  25587  minveclem3b  25642  ivthlem1  25665  ivthlem2  25666  ivthlem3  25667  ivth2  25669  ivthle  25670  ivthle2  25671  ivthicc  25672  ovolficcss  25683  ovolunlem1a  25710  ovolunlem1  25711  ovolfiniun  25715  ovoliunlem1  25716  ovoliunlem3  25718  ovoliun  25719  ovoliun2  25720  shft2rab  25722  ovolshftlem1  25723  sca2rab  25726  ovolscalem1  25727  mblsplit  25746  finiunmbl  25758  volun  25759  volfiniun  25761  voliunlem1  25764  voliunlem3  25766  iunmbl  25767  voliun  25768  volsup  25770  ioombl  25779  ioorcl  25791  vitalilem1  25822  vitalilem2  25823  vitalilem3  25824  vitalilem4  25825  vitali  25827  ismbf1  25838  mbfdm  25840  ismbf  25842  ismbfcn  25843  mbfima  25844  mbfimaicc  25845  ismbfcn2  25852  ismbfd  25853  ismbf2d  25854  mbfeqalem1  25855  mbfmax  25863  mbfposr  25866  mbfposb  25867  ismbf3d  25868  mbfimaopnlem  25869  mbfimaopn2  25871  cncombf  25872  isi1f  25888  i1fd  25895  itg1mulc  25918  mbfi1fseqlem4  25932  itg2lcl  25941  isibl  25979  iblitg  25982  iblcnlem1  26002  iblcnlem  26003  iblrelem  26005  iblpos  26007  itgeqa  26028  itgfsum  26041  itgabs  26049  limcvallem  26085  ellimc  26087  ellimc2  26091  limcmpt  26097  cnmptlimc  26104  dvbsss  26116  cpnfval  26146  elcpn  26148  dvmptfsum  26189  dvle  26221  dvfsumle  26235  dvfsumge  26236  dvfsumabs  26237  dvfsumrlimf  26239  dvfsumlem1  26240  dvfsumlem2  26241  dvfsumlem3  26242  dvfsumlem4  26243  dvfsumrlimge0  26244  dvfsumrlim  26245  dvfsumrlim2  26246  dvfsum2  26248  itgsubstlem  26262  itgsubst  26263  mdegcl  26281  deg1nn0clb  26302  isuc1p  26353  plyeq0lem  26422  plyco  26453  plycj  26489  plycjOLD  26491  dvply2g  26501  dvnply2  26503  plydivlem4  26512  fta1lem  26523  fta1  26524  elqaalem1  26535  elqaalem2  26536  elqaalem3  26537  elqaa  26538  ulmcau  26613  radcnv0  26634  radcnvlt1  26636  radcnvle  26638  pserdvlem2  26646  coseq1  26745  efeq1  26748  sinord  26754  efif1olem2  26763  efif1olem4  26765  lognegb  26810  logcj  26826  argimgt0  26832  logtayl  26880  2irrexpq  26951  root1eq1  26975  logrec  26983  2irrexpqALT  27020  angrteqvd  27026  angpieqvdlem  27048  atans  27150  atans2  27151  dmarea  27177  areambl  27178  rlimcnp  27185  rlimcnp2  27186  xrlimcnp  27188  harmonicbnd  27223  harmonicbnd2  27224  lgamcvglem  27259  wilthlem2  27288  wilth  27290  efnnfsumcl  27322  vmacl  27337  efvmacl  27339  efchtdvds  27378  sqff1o  27401  fsumdvdscom  27404  musumsum  27411  fsumdvdsmul  27414  fsumvma  27432  perfect  27450  dchrelbasd  27458  lgsval  27520  lgsval2lem  27526  lgsdir2lem4  27547  lgsdir2  27549  lgsqrlem1  27565  lgsdchr  27574  m1lgs  27607  2lgs  27626  mul2sq  27638  2sqlem6  27642  2sqblem  27650  2sq2  27652  rplogsumlem2  27704  dchrisumlema  27707  dchrisumlem2  27709  dchrisumlem3  27710  dchrvmasumlem2  27717  dchrvmasumlem3  27718  dchrisum0flblem2  27728  dchrisum0flb  27729  dchrisum0fno1  27730  ostthlem1  27846  nodmon  27869  noextendseq  27886  nodense  27911  madefi  28161  addsproplem1  28217  addsproplem3  28219  addsprop  28224  addsf  28230  addbdaylem  28265  negsproplem1  28276  negsproplem3  28278  negsprop  28283  negbdaylem  28304  mulsproplemcbv  28363  mulsproplem1  28364  mulsproplem10  28373  mulsprop  28378  addonbday  28527  noseqp1  28539  noseqind  28540  peano5n0s  28567  dfn0s2  28580  n0addscl  28592  n0mulscl  28593  n0bday  28600  onsfi  28604  n0s0m1  28610  n0subs  28611  n0p1nns  28619  dfnns2  28620  nn1m1nns  28622  oldfib  28625  zaddscl  28642  zmulscld  28645  elzn0s  28646  peano5uzs  28652  expscllem  28678  z12addscl  28725  z12shalf  28728  z12negsclb  28729  z12zsodd  28730  z12bdaylem  28732  z12bday  28733  bdayfin  28735  mirval  28987  perpneq  29049  isperp2  29050  isperp2d  29051  foot  29057  islnopp  29075  islnoppd  29076  outpasch  29092  hlpasch  29093  ishpg  29096  colopp  29106  colhp  29107  lmif  29149  islmib  29151  lmiinv  29156  trgcopy  29170  trgcopyeu  29172  acopyeu  29200  inaghl  29221  tgasa1  29234  f1otrgitv  29278  f1otrg  29279  isfusgr  29730  opfusgr  29735  fusgrfisbase  29740  fusgrfisstep  29741  nbupgrel  29757  nbumgrvtx  29758  nbusgreledg  29765  edgnbusgreu  29779  nb3grprlem1  29792  uvtxusgrel  29815  cusgredg  29836  cplgr2vpr  29845  cusgrexg  29856  usgredgsscusgredg  29871  fusgrn0degnn0  29911  rusgrnumwrdl2  29998  rgrx0ndm  30005  wlkcomp  30042  wlkdlem2  30093  clwlkcomp  30197  iswwlks  30256  wwlknllvtx  30266  0enwwlksnge1  30284  wlkiswwlks2lem5  30293  wwlksm1edg  30301  wwlksnred  30312  wwlksnext  30313  wwlksnextbi  30314  wwlksnredwwlkn  30315  wwlksnextfun  30318  wwlksnextinj  30319  wwlksnextsurj  30320  wwlksnextbij  30322  wwlksnfi  30326  wwlksnextproplem2  30330  wwlksnextprop  30332  2wlkdlem4  30348  rusgrnumwwlkl1  30391  rusgrnumwwlks  30397  isclwwlk  30406  clwwlk1loop  30410  clwwlkccatlem  30411  clwlkclwwlklem2a1  30414  clwlkclwwlklem2a4  30419  clwlkclwwlklem2a  30420  clwlkclwwlklem2  30422  clwlkclwwlklem3  30423  clwlkclwwlk  30424  clwlkclwwlk2  30425  clwwisshclwwslemlem  30435  clwwisshclwwslem  30436  clwwisshclwws  30437  clwwlknlbonbgr1  30461  clwwlkinwwlk  30462  clwwlkn1  30463  loopclwwlkn1b  30464  clwwlkn1loopb  30465  clwwlkn2  30466  clwwlkel  30468  clwwlkf  30469  clwwlkwwlksb  30476  clwwlkext2edg  30478  wwlksext2clwwlk  30479  wwlksubclwwlk  30480  eleclclwwlknlem2  30483  umgr2cwwk2dif  30486  s2elclwwlknon2  30526  clwwlknonwwlknonb  30528  clwwlknonex2lem2  30530  clwwlknonex2  30531  loop1cycl  30575  3wlkdlem4  30588  upgr3v3e3cycl  30606  upgr4cycl4dv4e  30611  eupth2lem2  30645  eulerpathpr  30666  1vwmgr  30702  3vfriswmgrlem  30703  3vfriswmgr  30704  3cyclfrgrrn1  30711  vdgn1frgrv2  30722  frgrncvvdeqlem3  30727  frgrncvvdeqlem8  30732  frgrncvvdeqlem9  30733  frgrwopregasn  30742  frgrwopregbsn  30743  frgrwopreglem5ALT  30748  frgr2wwlk1  30755  frgr2wwlkeqm  30757  fusgr2wsp2nb  30760  2clwwlk2clwwlklem  30772  extwwlkfabel  30779  nvvop  31036  isnvlem  31037  sspval  31150  nmorepnf  31195  phpar  31251  siilem2  31279  bnsscmcl  31295  ubthlem1  31297  shaddcl  31644  shmulcl  31645  hsn0elch  31675  hhssablo  31690  hhssnvt  31692  hhsssh  31696  shscl  31745  shintcl  31757  chintcl  31759  shincl  31808  chincl  31926  h1datomi  32008  chscllem2  32065  sumspansn  32076  spansncvi  32079  5oalem2  32082  5oalem3  32083  pjini  32126  pjjsi  32127  eigposi  32263  nmoprepnf  32294  nmfnrepnf  32307  dmadjrnb  32333  lnophmlem1  32443  lnophm  32446  nmcopex  32456  lnconi  32460  nmbdfnlb  32477  nmcfnex  32480  imaelshi  32485  rnbra  32534  leopg  32549  pjbdlni  32576  pjhmop  32577  hmopidmch  32580  pjclem4  32626  pj3si  32634  strlem1  32677  atssma  32805  atcv0eq  32806  atcv1  32807  atomli  32809  atcvatlem  32812  cdj3lem2a  32863  cdj3lem3a  32866  xppreima  33065  fmptcof2  33077  aciunf1lem  33082  funcnv4mpt  33088  1stpreimas  33126  f1od2  33138  fpwrelmapffslem  33151  xrofsup  33186  fzspl  33208  fzsplit3  33212  nnindf  33238  fprodex01  33243  fsumiunle  33247  indf1ofs  33260  gsumhashmul  33455  fzto1st  33491  fxpsubm  33560  fxpsubg  33561  fxpsubrg  33562  isslmd  33590  slmdlema  33591  elrgspnlem2  33631  elrgspnlem4  33633  rlocisunit  33664  subsdrg  33687  qusker  33737  0nellinds  33753  unitprodclb  33770  nsgmgclem  33788  nsgmgc  33789  nsgqusf1olem2  33791  elrspunidl  33804  opprlidlabs  33835  dfufd2lem  33907  psrbasfsupp  33969  selvply1rhmlemb  33977  mplidomlem  33985  lindsunlem  34082  brfldext  34103  brfinext  34110  finextfldext  34122  finexttrb  34123  extdg1id  34124  fldextrspunlsplem  34131  constrconj  34203  constrfin  34204  trisecnconstr  34250  smatrcl  34254  submateq  34267  lmatfval  34272  lmatcl  34274  qtophaus  34294  locfinreflem  34298  locfinref  34299  zartopn  34333  zarcmplem  34339  rhmpreimacnlem  34342  xpinpreima  34364  xpinpreima2  34365  cnre2csqlem  34368  tpr2rico  34370  prsdm  34372  prsrn  34373  ordtrest2NEWlem  34380  ordtrest2NEW  34381  zrhcntr  34437  qqhval2  34440  isrrext  34458  ismntoplly  34483  esumcvg  34544  sigaval  34569  issiga  34570  0elsiga  34572  sigaclcu  34575  issgon  34581  prsiga  34589  sigaclci  34590  difunielsiga  34591  unelsiga  34592  ispisys2  34612  inelpisys  34613  unelldsys  34617  sigapildsyslem  34620  sigapildsys  34621  ldgenpisyslem1  34622  ldgenpisys  34625  isros  34627  unelros  34630  difelros  34631  fiunelros  34633  inelsros  34637  diffiunisros  34638  rossros  34639  measvuni  34673  measiun  34677  voliune  34688  volfiniune  34689  brfae  34707  ismbfm  34710  mbfmcnvima  34714  mbfmcst  34718  1stmbfm  34719  2ndmbfm  34720  imambfm  34721  sitgval  34791  issibf  34792  sibfima  34797  sitgfval  34800  sitgclg  34801  eulerpartlemelr  34816  eulerpartlemsf  34818  eulerpartleme  34822  eulerpartlemt0  34828  eulerpartlemt  34830  eulerpartgbij  34831  eulerpartlemr  34833  eulerpartlemmf  34834  eulerpartlemgvv  34835  eulerpartlemgs2  34839  eulerpartlemn  34840  eulerpart  34841  cndprobprob  34897  rrvsum  34913  orvcelel  34929  ballotlemodife  34957  ballotlemsdom  34971  ballotlemrv  34979  ballotlemrv1  34980  ballotlemrv2  34981  ballotlem1ri  34994  fsum2dsub  35063  reprinfz1  35078  reprpmtf1o  35082  reprdifc  35083  breprexplema  35086  hgt750lema  35113  hgt750leme  35114  bnj149  35332  bnj222  35340  bnj1112  35440  bnj1148  35453  fissorduni  35542  fineqvrep  35588  fineqvnttrclse  35598  fineqvinfep  35599  kardnnfi  35643  gblacfnacd  35647  vonf1wev  35653  vonf1owevOLD  35655  vonf1osev  35657  vonf1oonfo  35660  subfacp1lem3  35715  subfacp1lem6  35718  erdszelem10  35733  kur14  35749  cvxsconn  35776  cnllysconn  35778  resconn  35779  iscvm  35792  cvmliftlem5  35822  cvmliftlem15  35831  cvmlift2lem1  35835  cvmlift2lem12  35847  cvmlift2lem13  35848  sat1el2xp  35912  fmlasuc  35919  gonan0  35925  gonar  35928  satefvfmla0  35951  msubrn  36062  msubco  36064  ismfs  36082  mvtinf  36088  mclsax  36102  mppspstlem  36104  elmpps  36106  nnuni  36260  dfdm5  36306  dfrn5  36307  elima4  36309  rdgprc0  36324  pprodss4v  36415  elfuns  36446  fnimage  36460  imageval  36461  fwddifval  36695  fwddifnval  36696  fwddifnp1  36698  elhf2g  36709  hfun  36711  hfninf  36719  nmulprop  36723  filnetlem4  36953  onsucconn  37010  onsucsuccmp  37016  limsucncmp  37018  onint1  37021  fveleq  37023  findreccl  37025  nndivsub  37029  weiunse  37040  mh-inf3f1  37113  mh-infprim2bi  37119  mh-infprim3bi  37120  bj-seex  37618  bj-adjg1  37740  bj-mooreset  37805  bj-ismoored0  37809  bj-ismoored  37810  bj-inftyexpitaudisj  37910  bj-inftyexpidisj  37915  bj-isvec  37992  bj-isclm  37996  csbmpo123  38038  topdifinffinlem  38054  topdifinffin  38055  csbfinxpg  38095  phpreu  38316  finixpnum  38317  lindsenlbs  38327  poimirlem16  38348  poimirlem17  38349  poimirlem19  38351  poimirlem20  38352  poimirlem22  38354  poimirlem23  38355  poimirlem24  38356  poimirlem25  38357  poimirlem26  38358  poimirlem28  38360  poimirlem29  38361  poimirlem30  38362  poimirlem31  38363  poimirlem32  38364  poimir  38365  mblfinlem3  38371  ex-ovoliunnfl  38375  voliunnfl  38376  volsupnfl  38377  mbfresfi  38378  itgabsnc  38401  ftc1anclem6  38410  ftc1anclem7  38411  ftc1anclem8  38412  ftc1anc  38413  dvasin  38416  sdclem2  38455  fdc  38458  incsequz  38461  neificl  38466  mettrifi  38470  cntotbnd  38509  cnpwstotbnd  38510  ismtyima  38516  ismtyhmeolem  38517  heiborlem2  38525  heiborlem3  38526  heiborlem4  38527  heiborlem5  38528  heiborlem6  38529  heiborlem10  38533  isrngo  38610  isdivrngo  38663  drngoi  38664  idlval  38726  isidlc  38728  idladdcl  38732  idllmulcl  38733  idlrmulcl  38734  0idl  38738  pridlval  38746  smprngopr  38765  prnc  38780  ispridlc  38783  pridlc  38784  eqrelf  38969  iss2  39055  elcoeleqvrels  39390  elfunsALTV  39488  eldisjs  39530  eleldisjs  39539  fsumshftd  39788  riotaclbgBAD  39790  renegclALT  39799  lshpinN  39825  isopos  40016  oposlem  40018  glbconN  40213  lnnat  40263  2at0mat0  40361  islvol2aN  40428  dalawlem13  40719  pclfinclN  40786  lhpoc2N  40851  ltrncnvatb  40974  cdleme11h  41102  cdlemefr32sn2aw  41240  cdlemefs32sn1aw  41250  cdleme32fvaw  41275  cdlemg1fvawlemN  41409  dicelvalN  42014  dih1dimatlem  42165  dihlatat  42173  dihjatcclem4  42257  islpolN  42319  lpolsatN  42324  lpolpolsatN  42325  mapdordlem1a  42470  mapdordlem1  42472  mapdhcl  42563  iscsrg  42800  fzsplitnd  42811  lcmineqlem12  42869  intlewftc  42890  dvrelogpow2b  42897  aks4d1p1p3  42898  aks4d1p1p2  42899  aks4d1p1p4  42900  dvle2  42901  aks4d1p8  42916  aks4d1p9  42917  isprimroot  42922  primrootsunit1  42926  primrootscoprmpow  42928  aks6d1c1p1  42936  aks6d1c1p2  42938  aks6d1c1p3  42939  evl1gprodd  42946  hashscontpow  42951  aks6d1c3  42952  aks6d1c2  42959  sticksstones1  42975  sticksstones10  42984  sticksstones11  42985  sticksstones12a  42986  aks6d1c6lem1  42999  unitscyglem5  43028  retire  43157  reelznn0nn  43312  fsuppind  43399  fsuppssindlem2  43401  fsuppssind  43402  isnacs3  43518  nacsfix  43520  mzpclval  43533  mzpcl1  43537  mzpcl2  43538  mzpcl34  43539  mzpexpmpt  43553  mzpsubst  43556  diophin  43580  diophun  43581  2rexfrabdioph  43600  3rexfrabdioph  43601  4rexfrabdioph  43602  6rexfrabdioph  43603  7rexfrabdioph  43604  rabdiophlem2  43606  diophren  43617  fphpd  43620  fphpdo  43621  fiphp3d  43623  pellexlem1  43633  pell14qrexpclnn0  43670  pellqrex  43683  rmspecnonsq  43711  monotuz  43745  monotoddzzfi  43746  monotoddzz  43747  oddcomabszz  43748  modabsdifz  43790  rmxdioph  43820  expdiophlem2  43826  limsuc2  43845  dfac11  43866  kelac1  43867  dfac21  43870  lsmfgcl  43878  islnm  43881  lnmlssfg  43884  lmhmfgima  43888  pwslnm  43898  unxpwdom3  43899  pwfi2f1o  43900  islnr  43915  hbtlem2  43928  cnsrexpcl  43969  flcidc  43974  mendlmod  43993  proot1ex  44000  oaordnr  44100  omnord1  44109  oenord1  44120  cantnfresb  44128  onmcl  44135  tfsnfin  44156  nadd2rabtr  44188  nadd1rabtr  44192  nadd1rabex  44194  nadd1suc  44196  pwelg  44363  fipjust  44368  elnonrel  44388  elinlem  44401  elcnvlem  44404  ss2iundf  44462  dfhe3  44578  dffrege115  44781  rfovcnvf1od  44807  ntrneiel2  44889  clsneiel2  44912  neicvgel2  44923  grur1cld  45033  dvgrat  45099  cvgdvgrat  45100  radcnvrat  45101  binomcxplemdvsum  45142  binomcxplemnotnn0  45143  orbitcl  45743  modelaxreplem1  45764  modelaxreplem2  45765  modelaxrep  45767  fnchoice  45826  fiiuncl  45862  disjf1  45978  disjinfi  45987  choicefi  45994  axccdom  46015  fmptf  46031  fmptff  46061  monoords  46093  supminfrnmpt  46236  supxrleubrnmptf  46242  supminfxr  46255  supminfxr2  46260  supminfxrrnmpt  46262  monoordxrv  46272  monoordxr  46273  monoord2xrv  46274  monoord2xr  46275  caucvgbf  46280  cvgcaule  46282  fsummulc1f  46364  fsumnncl  46365  fsumf1of  46367  fsumreclf  46369  fsumlessf  46370  fsumsermpt  46372  fmul01  46373  fmulcl  46374  fmuldfeqlem1  46375  fmuldfeq  46376  fmul01lt1lem1  46377  fmul01lt1lem2  46378  fprodexp  46387  fprodabs2  46388  mccllem  46390  mccl  46391  fprodcnlem  46392  fprodcn  46393  climmulf  46397  climsuse  46401  climrecf  46402  climaddf  46408  climf  46415  sumnnodd  46423  clim2f  46427  0ellimcdiv  46440  climsubmpt  46451  climreclf  46455  climf2  46457  fnlimcnv  46458  climeldmeqmpt  46459  clim2f2  46461  climfveqmpt  46462  fnlimfvre  46465  fnlimabslt  46470  climfveqmpt3  46473  climbddf  46478  climeldmeqmpt3  46480  climinf2mpt  46505  climinfmpt  46506  limsupequzmptf  46522  lmbr3  46538  liminfreuzlem  46593  coseq0  46655  cncfshift  46665  cncfperiod  46670  fprodcncf  46691  ioodvbdlimc1lem2  46723  ioodvbdlimc2lem  46725  dvmptmulf  46728  dvnmptdivc  46729  dvnmul  46734  dvmptfprod  46736  iblspltprt  46764  itgspltprt  46770  stoweidlem2  46793  stoweidlem3  46794  stoweidlem4  46795  stoweidlem6  46797  stoweidlem8  46799  stoweidlem17  46808  stoweidlem19  46810  stoweidlem20  46811  stoweidlem21  46812  stoweidlem23  46814  stoweidlem27  46818  stoweidlem35  46826  stoweidlem42  46833  stoweidlem43  46834  stoweidlem62  46853  stoweid  46854  wallispilem3  46858  wallispi  46861  fourierdlem16  46914  fourierdlem21  46919  fourierdlem41  46939  fourierdlem42  46940  fourierdlem48  46945  fourierdlem49  46946  fourierdlem50  46947  fourierdlem51  46948  fourierdlem54  46951  fourierdlem63  46960  fourierdlem64  46961  fourierdlem65  46962  fourierdlem71  46968  fourierdlem72  46969  fourierdlem73  46970  fourierdlem83  46980  fourierdlem86  46983  fourierdlem89  46986  fourierdlem90  46987  fourierdlem91  46988  fourierdlem96  46993  fourierdlem97  46994  fourierdlem98  46995  fourierdlem99  46996  fourierdlem100  46997  fourierdlem103  47000  fourierdlem104  47001  fourierdlem105  47002  fourierdlem108  47005  fourierdlem109  47006  fourierdlem110  47007  fourierdlem112  47009  fourierdlem113  47010  etransclem24  47049  salunicl  47107  saluncl  47108  saldifcl  47110  sge0f1o  47173  sge0lempt  47201  sge0iunmptlemfi  47204  sge0p1  47205  sge0fodjrnlem  47207  sge0iunmpt  47209  sge0ltfirpmpt2  47217  sge0isummpt2  47223  sge0xaddlem2  47225  sge0xadd  47226  ismea  47242  nnfoctbdjlem  47246  nnfoctbdj  47247  meadjiun  47257  voliunsge0lem  47263  meaiuninclem  47271  meaiuninc3v  47275  hoidmvlelem2  47387  hoidmvlelem3  47388  vonvolmbl2  47454  hoimbl2  47456  vonhoire  47463  vonicclem2  47475  vonn0ioo2  47481  vonn0icc2  47483  salpreimagelt  47498  salpreimalegt  47500  salpreimagtge  47516  salpreimaltle  47517  issmf  47519  salpreimagtlt  47521  smfpreimalt  47522  smfpreimaltf  47527  issmfle  47536  smfpreimale  47545  issmfgt  47547  smfpreimagt  47553  issmfgelem  47560  issmfge  47561  smflimlem4  47565  smflim  47568  smfpreimage  47573  smfresal  47579  smfpimbor1lem1  47589  smfpimbor1lem2  47590  smflim2  47597  smflimmpt  47601  smflimsuplem1  47611  smflimsuplem2  47612  smflimsuplem3  47613  smflimsuplem5  47615  smflimsuplem7  47617  smflimsup  47619  smfliminf  47622  ormkglobd  47668  cjnpoly  47703  eu2ndop1stv  47939  dmfcoafv  47989  ffnaov  48013  faovcl  48014  funressndmafv2rn  48037  dfatdmfcoafv2  48068  mod2addne  48184  smonoord  48191  iccpartiltu  48248  iccpartigtl  48249  sprsymrelf1lem  48317  prproropf1olem2  48330  fmtno4prmfac193  48402  proththdlem  48442  proththd  48443  iseven  48470  isodd  48471  dfodd2  48478  evenm1odd  48481  evenp1odd  48482  enege  48487  onego  48488  epee  48547  perfectALTV  48565  bgoldbtbndlem2  48648  bgoldbtbndlem3  48649  bgoldbtbndlem4  48650  bgoldbtbnd  48651  clnbupgrel  48676  edgusgrclnbfin  48684  grimuhgr  48729  uhgrimedgi  48732  uhgrimprop  48734  isuspgrim0  48736  isuspgrimlem  48737  grimedg  48777  grtriproplem  48781  grtrif1o  48784  isgrtri  48785  grtriclwlk3  48787  cycl3grtrilem  48788  cycl3grtri  48789  grimgrtri  48791  usgrgrtrirex  48792  isubgr3stgrlem7  48814  grlimprclnbgrvtx  48841  grlimgredgex  48842  grlimgrtri  48845  usgrexmpl1tri  48867  gpgvtxel2  48890  gpgvtx0  48895  gpgvtx1  48896  gpgedgvtx0  48903  gpgedgvtx1  48904  gpgedgiov  48907  gpgedg2ov  48908  gpgedg2iv  48909  gpgnbgrvtx0  48916  gpgnbgrvtx1  48917  gpg3kgrtriex  48931  gpgprismgr4cycllem3  48939  pgnbgreunbgrlem1  48955  pgnbgreunbgrlem2lem1  48956  pgnbgreunbgrlem2lem2  48957  pgnbgreunbgrlem2lem3  48958  pgnbgreunbgrlem4  48961  pgnbgreunbgrlem5lem1  48962  pgnbgreunbgrlem5lem2  48963  pgnbgreunbgrlem5lem3  48964  pgnbgreunbgr  48967  grlimedgnedg  48973  uzlidlring  49076  smprngprmrng  49180  cbvmpox2  49192  lmod1  49348  nnolog2flm1  49446  dignn0flhalflem1  49471  catprsc  49867  nelsubc3lem  49924  fucofulem2  50165  fucofvalne  50179  isthincd2lem2  50289  euendfunc  50380  cnelsubclem  50457