Theorem eleq1d 2819

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809

This theorem is referenced by:  eleq1  2822  eleq12d  2828  eqeltrd  2834  eqneltrd  2854  rspcimdv  3591  reuind  3736  sbcel2  4393  sbccsb2  4412  disjiun  5107  breq1  5122  breq2  5123  axrep6g  5260  inex1g  5289  intex  5314  pwexg  5348  reusv2lem4  5371  reusv2  5373  reusv3  5375  rabxfrd  5387  prex  5407  opelopabsb  5505  csbmpt12  5532  pofun  5579  seex  5613  seinxp  5738  opabid2  5807  opeliunxp2  5818  elrn2g  5870  opeldmd  5886  opeldm  5887  elreldm  5915  elsnres  6008  iss  6022  unielrel  6263  onunel  6458  funopg  6569  funimaexgOLD  6623  brprcneu  6865  brprcneuALT  6866  tz6.12f  6901  ndmfvrcl  6911  ssimaex  6963  dmfco  6974  fvmpti  6984  fvmpt3  6989  fvmptf  7006  fvmptss2  7011  respreima  7055  fvn0ssdmfun  7063  fvelrn  7065  ffnfvf  7109  ffvresb  7114  fmptco  7118  fmptcof  7119  fsn  7124  fsn2g  7127  fressnfv  7149  fvrnressn  7150  fvn0fvelrnOLD  7152  fnex  7208  funfvima  7221  funfvima3  7227  f1mpt  7253  fliftfuns  7306  isoselem  7333  isowe2  7342  riotaclb  7401  ovrspc2v  7429  ffnov  7531  fovcld  7532  ovmpos  7553  ov2gf  7554  ovg  7570  funimassov  7582  oprssdm  7586  ndmovrcl  7591  caovclg  7597  elovmpo  7650  ofmpteq  7692  sorpsscmpl  7726  uniexg  7732  unexbOLD  7740  abnexg  7748  difsnexi  7753  onint  7782  limsuc  7842  tfisi  7852  peano5  7887  xpexr  7912  xpexcnv  7914  fnexALT  7947  focdmex  7952  f1stres  8010  f2ndres  8011  xp1st  8018  xp2nd  8019  unielxp  8024  opiota  8056  fmpox  8064  offval22  8085  frxp  8123  fnse  8130  frxp2  8141  sexp2  8143  frxp3  8148  sexp3  8150  opeliunxp2f  8207  dftpos4  8242  fvmpocurryd  8268  undefnel2  8274  onnseq  8356  smoel  8372  smo11  8376  tfrlem8  8396  tfrlem9  8397  tfrlem15  8404  tfr2b  8408  tz7.44-2  8419  tz7.44-3  8420  oacl  8545  omcl  8546  oecl  8547  oaord1  8561  omordi  8576  oen0  8596  oeeui  8612  nnacl  8621  nnmcl  8622  nnecl  8623  nnmordi  8641  nnaordex  8648  omsmolem  8667  naddcllem  8686  naddov2  8689  naddf  8691  naddssim  8695  naddelim  8696  naddasslem1  8704  naddasslem2  8705  naddsuc2  8711  erexb  8742  qliftfuns  8816  ixpsnval  8912  elixp2  8913  resixp  8945  undifixp  8946  mptelixpg  8947  resixpfo  8948  elixpsn  8949  fundmen  9043  fopwdom  9092  disjen  9146  xpf1o  9151  unfi  9183  cnvfi  9188  fnfi  9190  f1oenfirn  9192  f1domfi  9193  unblem2  9299  imafiOLD  9324  pwfi  9327  xpfiOLD  9329  fiint  9336  fiintOLD  9337  iunfi  9353  isfsupp  9375  fsuppun  9397  ffsuppbi  9408  elfi2  9424  wdom2d  9592  ixpiunwdom  9602  dfom3  9659  cantnfvalf  9677  cantnflt  9684  cantnflem1  9701  r1fin  9785  tz9.12lem3  9801  ranksnb  9839  ranklim  9856  r1pw  9857  r1pwALT  9858  r1pwcl  9859  rankuni2b  9865  djuexb  9921  cardmin2  10011  infxpenc2lem1  10031  dfac8alem  10041  dfac8clem  10044  ac5num  10048  acni2  10058  acnlem  10060  alephon  10081  alephfplem3  10118  alephfplem4  10119  dfac4  10134  dfac5lem1  10135  dfac5lem5  10139  dfac2a  10142  dfac2b  10143  dfacacn  10154  dfac12lem2  10157  dfac12r  10159  dfac12k  10160  cofsmo  10281  cfsmolem  10282  isfin1a  10304  fin1ai  10305  isfin3  10308  infpssrlem3  10317  fin23lem7  10328  fin23lem11  10329  enfin2i  10333  isf34lem4  10389  fin1a2lem7  10418  hsmexlem9  10437  hsmexlem4  10441  hsmex  10444  axcc2lem  10448  axcc3  10450  axdc3lem2  10463  axcclem  10469  zornn0g  10517  ttukeylem3  10523  ttukeylem6  10526  ttukey2g  10528  brdom7disj  10543  brdom6disj  10544  fnct  10549  konigthlem  10580  axregndlem2  10615  axinfnd  10618  axacndlem5  10623  axacnd  10624  fpwwe2lem4  10646  fpwwe2lem12  10654  fpwwe  10658  pwfseqlem1  10670  pwfseqlem3  10672  pwfseqlem4a  10673  pwfseqlem4  10674  wununi  10718  wunpw  10719  wunpr  10721  wunr1om  10731  tskpw  10765  tskr1om  10779  inar1  10787  grupw  10807  grupr  10809  gruurn  10810  gruiun  10811  ingru  10827  grur1a  10831  grothomex  10841  grothac  10842  addnidpi  10913  indpi  10919  adderpq  10968  mulerpq  10969  addclprlem2  11029  mulclprlem  11031  distrlem4pr  11038  prlem934  11045  ltexprlem3  11050  ltexprlem4  11051  ltexprlem7  11054  ltexpri  11055  prlem936  11059  reclem2pr  11060  reclem3pr  11061  addclsr  11095  mulclsr  11096  supsrlem  11123  supsr  11124  axaddf  11157  axmulf  11158  axaddrcl  11164  axmulrcl  11166  renegcl  11544  negreb  11546  negn0  11664  negf1o  11665  ltord1  11761  leord1  11762  eqord1  11763  ltord2  11764  leord2  11765  eqord2  11766  negfi  12189  infm3  12199  cju  12234  peano5nni  12241  peano2nn  12250  dfnn2  12251  nn1m1nn  12259  nnaddcl  12261  nnmulcl  12262  nnsub  12282  nndivtr  12285  un0addcl  12532  un0mulcl  12533  elnnnn0  12542  nn0sub  12549  fcdmnn0fsuppg  12559  elz  12588  nnnegz  12589  elz2  12604  znegclb  12627  zaddcl  12630  nzadd  12638  zmulcl  12639  zneo  12674  nneo  12675  zeo  12677  peano5uzi  12680  zindd  12692  eluzsubOLD  12886  uzp1  12891  uzaddcl  12918  ublbneg  12947  eqreznegel  12948  supminf  12949  zsupss  12951  qmulz  12965  qnegcl  12980  irradd  12987  irrmul  12988  xnn0xaddcl  13249  fzrev2  13603  injresinjlem  13801  negmod0  13893  om2uzuzi  13965  uzindi  13998  fsuppmapnn0ub  14011  mptnn0fsuppr  14015  seqexw  14033  seqcl2  14036  seqcl  14038  seqf  14039  monoord  14048  monoord2  14049  sermono  14050  seqsplit  14051  seqcaopr2  14054  seqid3  14062  seqhomo  14065  expcllem  14088  expcl2lem  14089  m1expcl2  14101  faccl  14299  facdiv  14303  facndiv  14304  bccmpl  14325  bccl  14338  hashclb  14374  hasheq0  14379  hashfn  14391  seqcoll  14480  opfi1uzind  14527  ccatalpha  14609  reuccatpfxs1lem  14762  reuccatpfxs1  14763  repswccat  14802  repswrevw  14803  2cshw  14829  2cshwcshw  14842  cshimadifsn  14846  cshco  14853  swrd2lsw  14969  wwlktovf  14973  wwlktovf1  14974  wwlktovfo  14975  wrd2f1tovbij  14977  shftlem  15085  shftf  15096  cjval  15119  cjth  15120  remim  15134  cnpart  15257  uzin2  15361  caubnd2  15374  sqreulem  15376  clim  15508  clim2  15518  lo1o12  15547  climrlim2  15561  lo1resb  15578  o1resb  15580  lo1eq  15582  climmpt2  15587  climshftlem  15588  rlimcld2  15592  climcn1  15606  climcn2  15607  o1dif  15644  iserex  15671  climub  15676  climserle  15677  isercoll  15682  climcau  15685  caurcvg2  15692  caucvgb  15694  summolem3  15728  summolem2a  15729  zsum  15732  fsum  15734  sumss2  15740  fsumcvg2  15741  fsumclf  15752  fsumsplitf  15756  fsumsplit1  15759  sumpr  15762  sumtp  15763  fsumm1  15765  fsum1p  15767  isummulc2  15776  fsum2dlem  15784  fsumcom2  15788  fsumshftm  15795  fsum0diag2  15797  fsumge1  15811  fsum00  15812  fsumabs  15815  telfsumo  15816  telfsumo2  15817  fsumparts  15820  fsumrlim  15825  fsumo1  15826  o1fsum  15827  fsumiun  15835  binomlem  15843  isumshft  15853  isum1p  15855  isumrpcl  15857  climcndslem1  15863  climcndslem2  15864  climcnds  15865  infcvgaux2i  15872  cvgrat  15897  mertens  15900  clim2prod  15902  prodfn0  15908  prodfrec  15909  prodfdiv  15910  ntrivcvgfvn0  15913  prodmolem3  15947  prodmolem2a  15948  zprod  15951  fprod  15955  prodss  15961  fprodser  15963  fprodm1  15981  fprod1p  15982  fprodm1s  15984  fprodp1s  15985  fprodabs  15988  fprodn0  15993  fprod2dlem  15994  fprodcnv  15997  fprodcom2  15998  fproddivf  16001  fprodsplitf  16002  fprodsplit1f  16004  bpolycl  16066  fprodefsum  16109  rpnnen2lem11  16240  mod2eq1n2dvds  16364  mulsucdiv2z  16370  zob  16376  nn0o1gt2  16398  nno  16399  nn0o  16400  divalglem7  16416  bitsf1  16463  sadcp1  16472  smupp1  16497  qnumdencl  16756  iserodd  16853  pcqcl  16874  pcxnn0cl  16878  pcxcl  16879  pcgcd1  16895  dvdsprmpweqle  16904  pcmpt  16910  pcmpt2  16911  pcmptdvds  16912  infpnlem2  16929  infpn2  16931  1arith  16945  elgz  16949  mul4sq  16972  4sqlem13  16975  4sqlem17  16979  4sqlem18  16980  4sqlem19  16981  vdwlem1  16999  vdwlem2  17000  vdwnn  17016  ramtcl2  17029  ramcl  17047  prmonn2  17057  prmodvdslcmf  17065  isstruct2  17166  wunress  17268  firest  17444  imasaddfnlem  17540  imasvscafn  17549  xpsfrnel2  17576  mreintcl  17605  ismred2  17613  mreexexlemd  17654  mreexexlem3d  17656  mreexexlem4d  17657  iscatd2  17691  catpropd  17719  subsubc  17864  isfunc  17875  inclfusubc  17954  fncnvimaeqv  18130  joindef  18384  joinval  18385  meetdef  18398  meetval  18399  oduclatb  18515  acsdrsel  18551  isacs4lem  18552  isacs5lem  18553  acsdrscl  18554  mgmsscl  18621  mgmpropd  18627  mgm1  18634  gsumvalx  18652  issubmgm  18678  issubmgm2  18679  mgmhmima  18691  sgrppropd  18707  mndpropd  18735  issubm  18779  0subm  18793  insubm  18794  mhmimalem  18800  gsumwsubmcl  18813  gsumwspan  18822  symggrplem  18860  sursubmefmnd  18872  injsubmefmnd  18873  smndex1basss  18881  mulgsubcl  19069  issubg  19107  issubg2  19122  issubg4  19126  0subg  19132  0subgOLD  19133  isnsg  19136  isnsg2  19137  nsgbi  19138  isnsg3  19141  elnmz  19144  nmzbi  19145  nmzsubg  19146  eqgval  19158  eqgid  19161  cycsubgcl  19187  ghmrn  19210  ghmnsgima  19221  gass  19282  oppgsubg  19344  f1omvdconj  19425  symgfisg  19447  psgneldm  19482  0subgALT  19547  odhash3  19555  sylow2blem2  19600  lsmsubm  19632  lsmsubg  19633  efgsf  19708  efgsdm  19709  efgs1b  19715  efgredlema  19719  eqgabl  19813  ablnsg  19826  cyggenod2  19864  gsumzaddlem  19900  gsummhm2  19918  gsum2dlem2  19950  gsum2d2lem  19952  gsumcom2  19954  dprdfeq0  20003  dprdsubg  20005  dprd2da  20023  ablfacrp  20047  pgpfac1lem3  20058  pgpfaclem1  20062  ablfaclem3  20068  ablfac2  20070  cycsubggenodd  20090  isrng  20112  issrg  20146  srgfcl  20154  rglcom4d  20169  srgbinomlem4  20187  isring  20195  iscrng  20198  dvdsr  20320  irredrmul  20385  isrngim  20403  isrim0OLD  20439  isrim0  20441  issubrng  20505  subrngringnsg  20511  issubrng2  20516  rhmimasubrnglem  20523  issubrg  20529  issubrg2  20550  subrgpropd  20566  isdrngd  20723  isdrngdOLD  20725  issdrg  20746  sdrgacs  20759  issrngd  20813  islmod  20819  lmodlema  20820  islmodd  20821  lmodprop2d  20879  rmodislmodlem  20884  rmodislmod  20885  lssset  20888  islssd  20890  lsscl  20897  lsslss  20916  lsspropd  20973  lmhmima  21003  lbsind  21036  lsmcl  21039  islvec  21060  lmhmlvec  21066  lspsolvlem  21101  lspsolv  21102  lvecpropd  21126  rnglidlmcl  21175  rnglidl0  21188  rnglidlmmgm  21204  rngqiprngimf1lem  21253  rngqiprngimf1  21259  ring2idlqus  21268  xrsdsreclblem  21378  xrsdsreclb  21379  cnsubrglem  21382  prmirred  21433  pzriprnglem4  21443  pzriprnglem8  21447  pzriprngALT  21454  znunithash  21523  cofipsgn  21551  zrhpsgnelbas  21552  rzgrp  21581  isphl  21586  phllmhm  21590  ipcl  21591  isphld  21612  phlpropd  21613  phlssphl  21617  cssincl  21646  pjdm  21665  dsmmval  21692  dsmmbas2  21695  dsmmelbas  21697  frlmbas  21713  frlmup1  21756  lindfind  21774  lindsind  21775  f1lindf  21780  islindf4  21796  psrbag  21875  psrbaglefi  21884  mplsubglem  21957  mpllsslem  21958  ltbwe  22000  psrbagsn  22019  subrgasclcl  22023  mplind  22026  mpfind  22063  psdmul  22102  coe1mul2lem2  22203  gsumply1eq  22245  evl1vsd  22280  mpfpf1  22287  pf1mpf  22288  pf1ind  22291  matecl  22361  m1detdiag  22533  mdetralt  22544  mdetralt2  22545  mdetunilem2  22549  mdetunilem9  22556  m2detleiblem3  22565  m2detleiblem4  22566  smadiadetlem0  22597  cpmatacl  22652  chpscmat  22778  uniopn  22833  inopn  22835  fiinopn  22837  istps  22870  fctop  22940  iscld  22963  isopn2  22968  mretopd  23028  iscldtop  23031  perfi  23091  tgrest  23095  restcld  23108  ordtbaslem  23124  ordtrest2lem  23139  ordtrest2  23140  iscn  23171  cnpval  23172  iscnp  23173  tgcn  23188  subbascn  23190  ssidcn  23191  lmbrf  23196  cnpnei  23200  cnima  23201  iscncl  23205  cnconst2  23219  cnrest2  23222  cnpresti  23224  cnprest  23225  cnindis  23228  lmres  23236  lmcnp  23240  iscnrm  23259  t1sncld  23262  cnrmi  23296  cncmp  23328  cmpsublem  23335  fiuncmp  23340  unconn  23365  conncompid  23367  conncompconn  23368  conncompss  23369  1stcfb  23381  2ndcrest  23390  2ndcctbss  23391  2ndcdisj  23392  1stccnp  23398  islly  23404  isnlly  23405  subislly  23417  restnlly  23418  restlly  23419  islly2  23420  hausllycmp  23430  cldllycmp  23431  dislly  23433  isptfin  23452  islocfin  23453  ptfinfin  23455  finlocfin  23456  dissnlocfin  23465  locfindis  23466  comppfsc  23468  kgenval  23471  elkgen  23472  kgeni  23473  cmpkgen  23487  1stckgenlem  23489  kgencn2  23493  ptpjpre1  23507  elpt  23508  elptr  23509  ptbasin  23513  xkobval  23522  xkoval  23523  xkoopn  23525  txbasval  23542  tx1cn  23545  tx2cn  23546  dfac14  23554  xkoccn  23555  txcnp  23556  ptcnplem  23557  txcnmpt  23560  txindislem  23569  txdis1cn  23571  txlly  23572  txnlly  23573  pthaus  23574  ptrescn  23575  hauseqlcld  23582  txlm  23584  tx2ndc  23587  txkgen  23588  xkoptsub  23590  xkopt  23591  xkoco1cn  23593  xkoco2cn  23594  xkococnlem  23595  xkococn  23596  cnmpt11  23599  cnmpt12  23603  cnmpt21  23607  cnmpt22  23610  cnmptkp  23616  cnmptk1p  23621  xkoinjcn  23623  txconn  23625  qtopval2  23632  elqtop  23633  idqtop  23642  qtopcld  23649  qtopeu  23652  qtoprest  23653  qtopomap  23654  qtopcmap  23655  ishmeo  23695  hmeoopn  23702  hmeocld  23703  ordthmeolem  23737  ptcmpfi  23749  elmptrab  23763  fgcl  23814  trfil2  23823  cfinfil  23829  uzrest  23833  ufilss  23841  trufil  23846  cfinufil  23864  ufinffr  23865  ufildr  23867  rnelfm  23889  flfcntr  23979  ptcmplem2  23989  ptcmplem3  23990  ptcmplem4  23991  ptcmplem5  23992  cnextfvval  24001  tmdcn2  24025  tmdmulg  24028  tmdgsum2  24032  symgtgp  24042  opnsubg  24044  clssubg  24045  tgpconncompeqg  24048  ghmcnp  24051  tgphaus  24053  tgpt0  24055  qustgpopn  24056  qustgplem  24057  tsmsgsum  24075  tsmssubm  24079  tsmsres  24080  tsmsf1o  24081  tsmsxplem1  24089  tsmsxplem2  24090  tsmsxp  24091  istrg  24100  istdrg  24102  istdrg2  24114  istlm  24121  istvc  24128  ustval  24139  ustincl  24144  ustdiag  24145  ustinvel  24146  ustexhalf  24147  ust0  24156  ucnima  24217  fmucndlem  24227  prdsdsf  24304  prdsxmet  24306  imasf1oxmet  24312  imasf1omet  24313  prdsxmslem2  24466  metustsym  24492  isnlm  24612  qtopbaslem  24695  xrtgioo  24744  reperflem  24756  fsumcn  24810  expcn  24812  expcnOLD  24814  xrhmeo  24893  cnllycmp  24904  bndth  24906  isclm  25013  lmhmclm  25036  lmmcvg  25211  fmcfil  25222  iscfil3  25223  iscau2  25227  iscau4  25229  iscmet3lem1  25241  iscmet3  25243  cfilres  25246  caussi  25247  equivcfil  25249  flimcfil  25264  bcthlem1  25274  isbn  25288  srabn  25310  ishl2  25320  cmslssbn  25322  cmscsscms  25323  minveclem3b  25378  ivthlem1  25402  ivthlem2  25403  ivthlem3  25404  ivth2  25406  ivthle  25407  ivthle2  25408  ivthicc  25409  ovolficcss  25420  ovolunlem1a  25447  ovolunlem1  25448  ovolfiniun  25452  ovoliunlem1  25453  ovoliunlem3  25455  ovoliun  25456  ovoliun2  25457  shft2rab  25459  ovolshftlem1  25460  sca2rab  25463  ovolscalem1  25464  mblsplit  25483  finiunmbl  25495  volun  25496  volfiniun  25498  voliunlem1  25501  voliunlem3  25503  iunmbl  25504  voliun  25505  volsup  25507  ioombl  25516  ioorcl  25528  vitalilem1  25559  vitalilem2  25560  vitalilem3  25561  vitalilem4  25562  vitali  25564  ismbf1  25575  mbfdm  25577  ismbf  25579  ismbfcn  25580  mbfima  25581  mbfimaicc  25582  ismbfcn2  25589  ismbfd  25590  ismbf2d  25591  mbfeqalem1  25592  mbfmax  25600  mbfposr  25603  mbfposb  25604  ismbf3d  25605  mbfimaopnlem  25606  mbfimaopn2  25608  cncombf  25609  isi1f  25625  i1fd  25632  itg1mulc  25655  mbfi1fseqlem4  25669  itg2lcl  25678  isibl  25716  iblitg  25719  iblcnlem1  25739  iblcnlem  25740  iblrelem  25742  iblpos  25744  itgeqa  25765  itgfsum  25778  itgabs  25786  limcvallem  25822  ellimc  25824  ellimc2  25828  limcmpt  25834  cnmptlimc  25841  dvbsss  25853  cpnfval  25884  elcpn  25886  dvmptfsum  25929  dvle  25962  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvfsumabs  25979  dvfsumrlimf  25981  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumlem4  25986  dvfsumrlimge0  25987  dvfsumrlim  25988  dvfsumrlim2  25989  dvfsum2  25991  itgsubstlem  26005  itgsubst  26006  mdegcl  26024  deg1nn0clb  26045  isuc1p  26096  plyeq0lem  26165  plyco  26196  plycj  26233  plycjOLD  26235  dvply2g  26242  dvnply2  26245  plydivlem4  26254  fta1lem  26265  fta1  26266  elqaalem1  26277  elqaalem2  26278  elqaalem3  26279  elqaa  26280  ulmcau  26354  radcnv0  26375  radcnvlt1  26377  radcnvle  26379  pserdvlem2  26388  coseq1  26484  efeq1  26487  sinord  26493  efif1olem2  26502  efif1olem4  26504  lognegb  26549  logcj  26565  argimgt0  26571  logtayl  26619  2irrexpq  26690  root1eq1  26715  logrec  26723  2irrexpqALT  26760  angrteqvd  26766  angpieqvdlem  26788  atans  26890  atans2  26891  dmarea  26917  areambl  26918  rlimcnp  26925  rlimcnp2  26926  xrlimcnp  26928  harmonicbnd  26964  harmonicbnd2  26965  lgamcvglem  27000  wilthlem2  27029  wilth  27031  efnnfsumcl  27063  vmacl  27078  efvmacl  27080  efchtdvds  27119  sqff1o  27142  fsumdvdscom  27145  musumsum  27152  fsumdvdsmul  27155  fsumdvdsmulOLD  27157  fsumvma  27174  perfect  27192  dchrelbasd  27200  lgsval  27262  lgsval2lem  27268  lgsdir2lem4  27289  lgsdir2  27291  lgsqrlem1  27307  lgsdchr  27316  m1lgs  27349  2lgs  27368  mul2sq  27380  2sqlem6  27384  2sqblem  27392  2sq2  27394  rplogsumlem2  27446  dchrisumlema  27449  dchrisumlem2  27451  dchrisumlem3  27452  dchrvmasumlem2  27459  dchrvmasumlem3  27460  dchrisum0flblem2  27470  dchrisum0flb  27471  dchrisum0fno1  27472  ostthlem1  27588  nodmon  27612  noextendseq  27629  nodense  27654  madefi  27867  addsproplem1  27919  addsproplem3  27921  addsprop  27926  addsf  27932  addsbdaylem  27966  negsproplem1  27977  negsproplem3  27979  negsprop  27984  negsbdaylem  28005  mulsproplemcbv  28058  mulsproplem1  28059  mulsproplem10  28068  mulsprop  28073  noseqp1  28214  noseqind  28215  peano5n0s  28241  dfn0s2  28253  n0addscl  28264  n0mulscl  28265  n0sbday  28271  n0s0m1  28276  n0subs  28277  n0p1nns  28278  dfnns2  28279  zaddscl  28297  zmulscld  28300  elzn0s  28301  peano5uzs  28307  expscl  28330  pw2bday  28335  zs12bday  28341  mirval  28580  perpneq  28639  isperp2  28640  isperp2d  28641  foot  28647  islnopp  28664  islnoppd  28665  outpasch  28680  hlpasch  28681  ishpg  28684  colopp  28694  colhp  28695  lmif  28710  islmib  28712  lmiinv  28717  trgcopy  28729  trgcopyeu  28731  acopyeu  28759  inaghl  28770  tgasa1  28783  f1otrgitv  28795  f1otrg  28796  isfusgr  29243  opfusgr  29248  fusgrfisbase  29253  fusgrfisstep  29254  nbupgrel  29270  nbumgrvtx  29271  nbusgreledg  29278  edgnbusgreu  29292  nb3grprlem1  29305  uvtxusgrel  29328  cusgredg  29349  cplgr2vpr  29358  cusgrexg  29369  usgredgsscusgredg  29385  fusgrn0degnn0  29425  rusgrnumwrdl2  29512  rgrx0ndm  29519  wlkcomp  29557  wlkdlem2  29609  clwlkcomp  29707  iswwlks  29764  wwlknllvtx  29774  0enwwlksnge1  29792  wlkiswwlks2lem5  29801  wwlksm1edg  29809  wwlksnred  29820  wwlksnext  29821  wwlksnextbi  29822  wwlksnredwwlkn  29823  wwlksnextfun  29826  wwlksnextinj  29827  wwlksnextsurj  29828  wwlksnextbij  29830  wwlksnfi  29834  wwlksnextproplem2  29838  wwlksnextprop  29840  2wlkdlem4  29856  rusgrnumwwlkl1  29896  rusgrnumwwlks  29902  isclwwlk  29911  clwwlk1loop  29915  clwwlkccatlem  29916  clwlkclwwlklem2a1  29919  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  clwlkclwwlklem2  29927  clwlkclwwlklem3  29928  clwlkclwwlk  29929  clwlkclwwlk2  29930  clwwisshclwwslemlem  29940  clwwisshclwwslem  29941  clwwisshclwws  29942  clwwlknlbonbgr1  29966  clwwlkinwwlk  29967  clwwlkn1  29968  loopclwwlkn1b  29969  clwwlkn1loopb  29970  clwwlkn2  29971  clwwlkel  29973  clwwlkf  29974  clwwlkwwlksb  29981  clwwlkext2edg  29983  wwlksext2clwwlk  29984  wwlksubclwwlk  29985  eleclclwwlknlem2  29988  umgr2cwwk2dif  29991  s2elclwwlknon2  30031  clwwlknonwwlknonb  30033  clwwlknonex2lem2  30035  clwwlknonex2  30036  3wlkdlem4  30089  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  eupth2lem2  30146  eulerpathpr  30167  1vwmgr  30203  3vfriswmgrlem  30204  3vfriswmgr  30205  3cyclfrgrrn1  30212  vdgn1frgrv2  30223  frgrncvvdeqlem3  30228  frgrncvvdeqlem8  30233  frgrncvvdeqlem9  30234  frgrwopregasn  30243  frgrwopregbsn  30244  frgrwopreglem5ALT  30249  frgr2wwlk1  30256  frgr2wwlkeqm  30258  fusgr2wsp2nb  30261  2clwwlk2clwwlklem  30273  extwwlkfabel  30280  nvvop  30536  isnvlem  30537  sspval  30650  nmorepnf  30695  phpar  30751  siilem2  30779  bnsscmcl  30795  ubthlem1  30797  shaddcl  31144  shmulcl  31145  hsn0elch  31175  hhssablo  31190  hhssnvt  31192  hhsssh  31196  shscl  31245  shintcl  31257  chintcl  31259  shincl  31308  chincl  31426  h1datomi  31508  chscllem2  31565  sumspansn  31576  spansncvi  31579  5oalem2  31582  5oalem3  31583  pjini  31626  pjjsi  31627  eigposi  31763  nmoprepnf  31794  nmfnrepnf  31807  dmadjrnb  31833  lnophmlem1  31943  lnophm  31946  nmcopex  31956  lnconi  31960  nmbdfnlb  31977  nmcfnex  31980  imaelshi  31985  rnbra  32034  leopg  32049  pjbdlni  32076  pjhmop  32077  hmopidmch  32080  pjclem4  32126  pj3si  32134  strlem1  32177  atssma  32305  atcv0eq  32306  atcv1  32307  atomli  32309  atcvatlem  32312  cdj3lem2a  32363  cdj3lem3a  32366  xppreima  32569  fmptcof2  32581  aciunf1lem  32586  funcnv4mpt  32593  1stpreimas  32629  f1od2  32644  fpwrelmapffslem  32655  xrofsup  32690  fzspl  32712  fzsplit3  32716  nnindf  32744  fprodex01  32750  fsumiunle  32754  indfval  32779  indf1ofs  32789  gsumhashmul  33001  fzto1st  33060  isslmd  33145  slmdlema  33146  elrgspnlem2  33184  elrgspnlem4  33186  subsdrg  33238  qusker  33310  0nellinds  33331  unitprodclb  33350  nsgmgclem  33372  nsgmgc  33373  nsgqusf1olem2  33375  elrspunidl  33389  prmidlval  33398  prmidlc  33409  opprlidlabs  33446  dfufd2lem  33510  lindsunlem  33610  brfldext  33633  brfinext  33640  finexttrb  33652  extdg1id  33653  fldextrspunlsplem  33660  constrconj  33725  constrfin  33726  smatrcl  33773  submateq  33786  lmatfval  33791  lmatcl  33793  qtophaus  33813  locfinreflem  33817  locfinref  33818  zartopn  33852  zarcmplem  33858  rhmpreimacnlem  33861  xpinpreima  33883  xpinpreima2  33884  cnre2csqlem  33887  tpr2rico  33889  prsdm  33891  prsrn  33892  ordtrest2NEWlem  33899  ordtrest2NEW  33900  zrhcntr  33956  qqhval2  33959  isrrext  33977  ismntoplly  34002  esumcvg  34063  sigaval  34088  issiga  34089  0elsiga  34091  sigaclcu  34094  issgon  34100  prsiga  34108  sigaclci  34109  difelsiga  34110  unelsiga  34111  ispisys2  34130  inelpisys  34131  unelldsys  34135  sigapildsyslem  34138  sigapildsys  34139  ldgenpisyslem1  34140  ldgenpisys  34143  isros  34145  unelros  34148  difelros  34149  fiunelros  34151  inelsros  34155  diffiunisros  34156  rossros  34157  measvuni  34191  measiun  34195  voliune  34206  volfiniune  34207  brfae  34225  ismbfm  34228  mbfmcnvima  34233  mbfmcst  34237  1stmbfm  34238  2ndmbfm  34239  imambfm  34240  sitgval  34310  issibf  34311  sibfima  34316  sitgfval  34319  sitgclg  34320  eulerpartlemelr  34335  eulerpartlemsf  34337  eulerpartleme  34341  eulerpartlemt0  34347  eulerpartlemt  34349  eulerpartgbij  34350  eulerpartlemr  34352  eulerpartlemmf  34353  eulerpartlemgvv  34354  eulerpartlemgs2  34358  eulerpartlemn  34359  eulerpart  34360  cndprobprob  34416  rrvsum  34432  orvcelel  34448  ballotlemodife  34476  ballotlemsdom  34490  ballotlemrv  34498  ballotlemrv1  34499  ballotlemrv2  34500  ballotlem1ri  34513  fsum2dsub  34585  reprinfz1  34600  reprpmtf1o  34604  reprdifc  34605  breprexplema  34608  hgt750lema  34635  hgt750leme  34636  bnj149  34852  bnj222  34860  bnj1112  34960  bnj1148  34973  fineqvrep  35072  gblacfnacd  35076  loop1cycl  35105  subfacp1lem3  35150  subfacp1lem6  35153  erdszelem10  35168  kur14  35184  cvxsconn  35211  cnllysconn  35213  resconn  35214  iscvm  35227  cvmliftlem5  35257  cvmliftlem15  35266  cvmlift2lem1  35270  cvmlift2lem12  35282  cvmlift2lem13  35283  sat1el2xp  35347  fmlasuc  35354  gonan0  35360  gonar  35363  satefvfmla0  35386  msubrn  35497  msubco  35499  ismfs  35517  mvtinf  35523  mclsax  35537  mppspstlem  35539  elmpps  35541  nnuni  35690  dfdm5  35736  dfrn5  35737  elima4  35739  rdgprc0  35757  pprodss4v  35848  elfuns  35879  fnimage  35893  imageval  35894  fwddifval  36126  fwddifnval  36127  fwddifnp1  36129  elhf2g  36140  hfun  36142  hfninf  36150  filnetlem4  36345  onsucconn  36402  onsucsuccmp  36408  limsucncmp  36410  onint1  36413  fveleq  36415  findreccl  36417  nndivsub  36421  weiunse  36432  bj-seex  36886  bj-adjg1  37007  bj-mooreset  37066  bj-ismoored0  37070  bj-ismoored  37071  bj-inftyexpitaudisj  37169  bj-inftyexpidisj  37174  bj-isvec  37251  bj-isclm  37255  csbmpo123  37295  topdifinffinlem  37311  topdifinffin  37312  csbfinxpg  37352  phpreu  37574  finixpnum  37575  lindsenlbs  37585  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem28  37618  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  poimir  37623  mblfinlem3  37629  ex-ovoliunnfl  37633  voliunnfl  37634  volsupnfl  37635  mbfresfi  37636  itgabsnc  37659  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  dvasin  37674  sdclem2  37712  fdc  37715  incsequz  37718  neificl  37723  mettrifi  37727  cntotbnd  37766  cnpwstotbnd  37767  ismtyima  37773  ismtyhmeolem  37774  heiborlem2  37782  heiborlem3  37783  heiborlem4  37784  heiborlem5  37785  heiborlem6  37786  heiborlem10  37790  isrngo  37867  isdivrngo  37920  drngoi  37921  idlval  37983  isidlc  37985  idladdcl  37989  idllmulcl  37990  idlrmulcl  37991  0idl  37995  pridlval  38003  smprngopr  38022  prnc  38037  ispridlc  38040  pridlc  38041  eqrelf  38219  ecex2  38292  imaexALTV  38294  iss2  38308  elcoeleqvrels  38559  elfunsALTV  38656  eldisjs  38686  eleldisjs  38692  fsumshftd  38916  riotaclbgBAD  38918  renegclALT  38927  lshpinN  38953  isopos  39144  oposlem  39146  glbconN  39341  glbconNOLD  39342  lnnat  39392  2at0mat0  39490  islvol2aN  39557  dalawlem13  39848  pclfinclN  39915  lhpoc2N  39980  ltrncnvatb  40103  cdleme11h  40231  cdlemefr32sn2aw  40369  cdlemefs32sn1aw  40379  cdleme32fvaw  40404  cdlemg1fvawlemN  40538  dicelvalN  41143  dih1dimatlem  41294  dihlatat  41302  dihjatcclem4  41386  islpolN  41448  lpolsatN  41453  lpolpolsatN  41454  mapdordlem1a  41599  mapdordlem1  41601  mapdhcl  41692  iscsrg  41929  fzsplitnd  41941  lcmineqlem12  41999  intlewftc  42020  dvrelogpow2b  42027  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  dvle2  42031  aks4d1p8  42046  aks4d1p9  42047  isprimroot  42052  primrootsunit1  42056  primrootscoprmpow  42058  aks6d1c1p1  42066  aks6d1c1p2  42068  aks6d1c1p3  42069  evl1gprodd  42076  hashscontpow  42081  aks6d1c3  42082  aks6d1c2  42089  sticksstones1  42105  sticksstones10  42114  sticksstones11  42115  sticksstones12a  42116  aks6d1c6lem1  42129  unitscyglem5  42158  metakunt26  42189  metakunt29  42192  metakunt30  42193  metakunt32  42195  retire  42315  reelznn0nn  42439  fsuppind  42560  fsuppssindlem2  42562  fsuppssind  42563  isnacs3  42680  nacsfix  42682  mzpclval  42695  mzpcl1  42699  mzpcl2  42700  mzpcl34  42701  mzpexpmpt  42715  mzpsubst  42718  diophin  42742  diophun  42743  2rexfrabdioph  42766  3rexfrabdioph  42767  4rexfrabdioph  42768  6rexfrabdioph  42769  7rexfrabdioph  42770  rabdiophlem2  42772  diophren  42783  fphpd  42786  fphpdo  42787  fiphp3d  42789  pellexlem1  42799  pell14qrexpclnn0  42836  pellqrex  42849  rmspecnonsq  42877  monotuz  42912  monotoddzzfi  42913  monotoddzz  42914  oddcomabszz  42915  modabsdifz  42957  rmxdioph  42987  expdiophlem2  42993  limsuc2  43012  dfac11  43033  kelac1  43034  dfac21  43037  lsmfgcl  43045  islnm  43048  lnmlssfg  43051  lmhmfgima  43055  pwslnm  43065  unxpwdom3  43066  pwfi2f1o  43067  islnr  43082  hbtlem2  43095  cnsrexpcl  43136  flcidc  43141  mendlmod  43160  proot1ex  43167  oaordnr  43267  omnord1  43276  oenord1  43287  cantnfresb  43295  onmcl  43302  tfsnfin  43323  nadd2rabtr  43355  nadd1rabtr  43359  nadd1rabex  43361  nadd1suc  43363  pwelg  43531  fipjust  43536  elnonrel  43556  elinlem  43569  elcnvlem  43572  ss2iundf  43630  dfhe3  43746  dffrege115  43949  rfovcnvf1od  43975  ntrneiel2  44057  clsneiel2  44080  neicvgel2  44091  grur1cld  44204  dvgrat  44284  cvgdvgrat  44285  radcnvrat  44286  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  orbitcl  44930  modelaxreplem1  44951  modelaxreplem2  44952  modelaxrep  44954  fnchoice  45001  fiiuncl  45037  disjf1  45155  disjinfi  45164  choicefi  45172  axccdom  45194  fmptf  45211  fmptff  45241  monoords  45274  supminfrnmpt  45420  supxrleubrnmptf  45426  supminfxr  45439  supminfxr2  45444  supminfxrrnmpt  45446  monoordxrv  45456  monoordxr  45457  monoord2xrv  45458  monoord2xr  45459  caucvgbf  45464  cvgcaule  45466  fsummulc1f  45548  fsumnncl  45549  fsumf1of  45551  fsumreclf  45553  fsumlessf  45554  fsumsermpt  45556  fmul01  45557  fmulcl  45558  fmuldfeqlem1  45559  fmuldfeq  45560  fmul01lt1lem1  45561  fmul01lt1lem2  45562  fprodexp  45571  fprodabs2  45572  mccllem  45574  mccl  45575  fprodcnlem  45576  fprodcn  45577  climmulf  45581  climsuse  45585  climrecf  45586  climaddf  45592  climf  45599  sumnnodd  45607  clim2f  45613  0ellimcdiv  45626  climsubmpt  45637  climreclf  45641  climf2  45643  fnlimcnv  45644  climeldmeqmpt  45645  clim2f2  45647  climfveqmpt  45648  fnlimfvre  45651  fnlimabslt  45656  climfveqmpt3  45659  climbddf  45664  climeldmeqmpt3  45666  climinf2mpt  45691  climinfmpt  45692  limsupequzmptf  45708  lmbr3  45724  liminfreuzlem  45779  coseq0  45841  cncfshift  45851  cncfperiod  45856  fprodcncf  45877  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvmptmulf  45914  dvnmptdivc  45915  dvnmul  45920  dvmptfprod  45922  iblspltprt  45950  itgspltprt  45956  stoweidlem2  45979  stoweidlem3  45980  stoweidlem4  45981  stoweidlem6  45983  stoweidlem8  45985  stoweidlem17  45994  stoweidlem19  45996  stoweidlem20  45997  stoweidlem21  45998  stoweidlem23  46000  stoweidlem27  46004  stoweidlem35  46012  stoweidlem42  46019  stoweidlem43  46020  stoweidlem62  46039  stoweid  46040  wallispilem3  46044  wallispi  46047  fourierdlem16  46100  fourierdlem21  46105  fourierdlem41  46125  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem51  46134  fourierdlem54  46137  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem71  46154  fourierdlem72  46155  fourierdlem73  46156  fourierdlem83  46166  fourierdlem86  46169  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem96  46179  fourierdlem97  46180  fourierdlem98  46181  fourierdlem99  46182  fourierdlem100  46183  fourierdlem103  46186  fourierdlem104  46187  fourierdlem105  46188  fourierdlem108  46191  fourierdlem109  46192  fourierdlem110  46193  fourierdlem112  46195  fourierdlem113  46196  etransclem24  46235  salunicl  46293  saluncl  46294  saldifcl  46296  sge0f1o  46359  sge0lempt  46387  sge0iunmptlemfi  46390  sge0p1  46391  sge0fodjrnlem  46393  sge0iunmpt  46395  sge0ltfirpmpt2  46403  sge0isummpt2  46409  sge0xaddlem2  46411  sge0xadd  46412  ismea  46428  nnfoctbdjlem  46432  nnfoctbdj  46433  meadjiun  46443  voliunsge0lem  46449  meaiuninclem  46457  meaiuninc3v  46461  hoidmvlelem2  46573  hoidmvlelem3  46574  vonvolmbl2  46640  hoimbl2  46642  vonhoire  46649  vonicclem2  46661  vonn0ioo2  46667  vonn0icc2  46669  salpreimagelt  46684  salpreimalegt  46686  salpreimagtge  46702  salpreimaltle  46703  issmf  46705  salpreimagtlt  46707  smfpreimalt  46708  smfpreimaltf  46713  issmfle  46722  smfpreimale  46731  issmfgt  46733  smfpreimagt  46739  issmfgelem  46746  issmfge  46747  smflimlem4  46751  smflim  46754  smfpreimage  46759  smfresal  46765  smfpimbor1lem1  46775  smfpimbor1lem2  46776  smflim2  46783  smflimmpt  46787  smflimsuplem1  46797  smflimsuplem2  46798  smflimsuplem3  46799  smflimsuplem5  46801  smflimsuplem7  46803  smflimsup  46805  smfliminf  46808  ormkglobd  46852  eu2ndop1stv  47102  dmfcoafv  47152  ffnaov  47176  faovcl  47177  funressndmafv2rn  47200  dfatdmfcoafv2  47231  smonoord  47333  iccpartiltu  47384  iccpartigtl  47385  sprsymrelf1lem  47453  prproropf1olem2  47466  fmtno4prmfac193  47535  proththdlem  47575  proththd  47576  iseven  47590  isodd  47591  dfodd2  47598  evenm1odd  47601  evenp1odd  47602  enege  47607  onego  47608  epee  47667  perfectALTV  47685  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbndlem4  47770  bgoldbtbnd  47771  clnbupgrel  47796  edgusgrclnbfin  47803  grimuhgr  47848  uhgrimedgi  47851  uhgrimprop  47853  isuspgrim0  47855  isuspgrimlem  47856  grimedg  47896  grtriproplem  47899  grtrif1o  47902  isgrtri  47903  grtriclwlk3  47905  cycl3grtrilem  47906  cycl3grtri  47907  grimgrtri  47909  usgrgrtrirex  47910  isubgr3stgrlem7  47932  grlimgrtri  47956  usgrexmpl1tri  47977  gpgvtxel2  48000  gpgvtx0  48005  gpgvtx1  48006  gpgedgvtx0  48013  gpgedgvtx1  48014  gpgnbgrvtx0  48024  gpgnbgrvtx1  48025  gpg3kgrtriex  48039  gpgprismgr4cycllem3  48044  uzlidlring  48158  cbvmpox2  48259  lmod1  48416  nnolog2flm1  48518  dignn0flhalflem1  48543  catprsc  48936  nelsubc3lem  48985  fucofulem2  49170  fucofvalne  49184  isthincd2lem2  49269  euendfunc  49359  cnelsubclem  49428