Theorem eleq1d 2826

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

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

This theorem is referenced by:  eleq1  2829  eleq12d  2835  eqeltrd  2841  eqneltrd  2861  rspcimdv  3612  reuind  3759  sbcel2  4418  sbccsb2  4437  disjiun  5131  breq1  5146  breq2  5147  axrep6g  5290  inex1g  5319  intex  5344  pwexg  5378  reusv2lem4  5401  reusv2  5403  reusv3  5405  rabxfrd  5417  prex  5437  opelopabsb  5535  csbmpt12  5562  pofun  5610  seex  5644  seinxp  5769  opabid2  5838  opeliunxp2  5849  elrn2g  5901  opeldmd  5917  opeldm  5918  elreldm  5946  elsnres  6039  iss  6053  unielrel  6294  onunel  6489  funopg  6600  funimaexgOLD  6654  brprcneu  6896  brprcneuALT  6897  tz6.12f  6932  ndmfvrcl  6942  ssimaex  6994  dmfco  7005  fvmpti  7015  fvmpt3  7020  fvmptf  7037  fvmptss2  7042  respreima  7086  fvn0ssdmfun  7094  fvelrn  7096  ffnfvf  7140  ffvresb  7145  fmptco  7149  fmptcof  7150  fsn  7155  fsn2g  7158  fressnfv  7180  fvrnressn  7181  fvn0fvelrnOLD  7183  fnex  7237  funfvima  7250  funfvima3  7256  f1mpt  7281  fliftfuns  7334  isoselem  7361  isowe2  7370  riotaclb  7429  ovrspc2v  7457  ffnov  7559  fovcld  7560  ovmpos  7581  ov2gf  7582  ovg  7598  funimassov  7610  oprssdm  7614  ndmovrcl  7619  caovclg  7625  elovmpo  7678  ofmpteq  7720  sorpsscmpl  7754  uniexg  7760  unexbOLD  7768  abnexg  7776  difsnexi  7781  onint  7810  limsuc  7870  tfisi  7880  peano5  7915  xpexr  7940  xpexcnv  7942  fnexALT  7975  focdmex  7980  f1stres  8038  f2ndres  8039  xp1st  8046  xp2nd  8047  unielxp  8052  opiota  8084  fmpox  8092  offval22  8113  frxp  8151  fnse  8158  frxp2  8169  sexp2  8171  frxp3  8176  sexp3  8178  opeliunxp2f  8235  dftpos4  8270  fvmpocurryd  8296  undefnel2  8302  onnseq  8384  smoel  8400  smo11  8404  tfrlem8  8424  tfrlem9  8425  tfrlem15  8432  tfr2b  8436  tz7.44-2  8447  tz7.44-3  8448  oacl  8573  omcl  8574  oecl  8575  oaord1  8589  omordi  8604  oen0  8624  oeeui  8640  nnacl  8649  nnmcl  8650  nnecl  8651  nnmordi  8669  nnaordex  8676  omsmolem  8695  naddcllem  8714  naddov2  8717  naddf  8719  naddssim  8723  naddelim  8724  naddasslem1  8732  naddasslem2  8733  naddsuc2  8739  erexb  8770  qliftfuns  8844  ixpsnval  8940  elixp2  8941  resixp  8973  undifixp  8974  mptelixpg  8975  resixpfo  8976  elixpsn  8977  fundmen  9071  fopwdom  9120  disjen  9174  xpf1o  9179  unfi  9211  cnvfi  9216  fnfi  9218  f1oenfirn  9220  f1domfi  9221  unblem2  9329  imafiOLD  9354  pwfi  9357  xpfiOLD  9359  fiint  9366  fiintOLD  9367  iunfi  9383  isfsupp  9405  fsuppun  9427  ffsuppbi  9438  elfi2  9454  wdom2d  9620  ixpiunwdom  9630  dfom3  9687  cantnfvalf  9705  cantnflt  9712  cantnflem1  9729  r1fin  9813  tz9.12lem3  9829  ranksnb  9867  ranklim  9884  r1pw  9885  r1pwALT  9886  r1pwcl  9887  rankuni2b  9893  djuexb  9949  cardmin2  10039  infxpenc2lem1  10059  dfac8alem  10069  dfac8clem  10072  ac5num  10076  acni2  10086  acnlem  10088  alephon  10109  alephfplem3  10146  alephfplem4  10147  dfac4  10162  dfac5lem1  10163  dfac5lem5  10167  dfac2a  10170  dfac2b  10171  dfacacn  10182  dfac12lem2  10185  dfac12r  10187  dfac12k  10188  cofsmo  10309  cfsmolem  10310  isfin1a  10332  fin1ai  10333  isfin3  10336  infpssrlem3  10345  fin23lem7  10356  fin23lem11  10357  enfin2i  10361  isf34lem4  10417  fin1a2lem7  10446  hsmexlem9  10465  hsmexlem4  10469  hsmex  10472  axcc2lem  10476  axcc3  10478  axdc3lem2  10491  axcclem  10497  zornn0g  10545  ttukeylem3  10551  ttukeylem6  10554  ttukey2g  10556  brdom7disj  10571  brdom6disj  10572  fnct  10577  konigthlem  10608  axregndlem2  10643  axinfnd  10646  axacndlem5  10651  axacnd  10652  fpwwe2lem4  10674  fpwwe2lem12  10682  fpwwe  10686  pwfseqlem1  10698  pwfseqlem3  10700  pwfseqlem4a  10701  pwfseqlem4  10702  wununi  10746  wunpw  10747  wunpr  10749  wunr1om  10759  tskpw  10793  tskr1om  10807  inar1  10815  grupw  10835  grupr  10837  gruurn  10838  gruiun  10839  ingru  10855  grur1a  10859  grothomex  10869  grothac  10870  addnidpi  10941  indpi  10947  adderpq  10996  mulerpq  10997  addclprlem2  11057  mulclprlem  11059  distrlem4pr  11066  prlem934  11073  ltexprlem3  11078  ltexprlem4  11079  ltexprlem7  11082  ltexpri  11083  prlem936  11087  reclem2pr  11088  reclem3pr  11089  addclsr  11123  mulclsr  11124  supsrlem  11151  supsr  11152  axaddf  11185  axmulf  11186  axaddrcl  11192  axmulrcl  11194  renegcl  11572  negreb  11574  negn0  11692  negf1o  11693  ltord1  11789  leord1  11790  eqord1  11791  ltord2  11792  leord2  11793  eqord2  11794  negfi  12217  infm3  12227  cju  12262  peano5nni  12269  peano2nn  12278  dfnn2  12279  nn1m1nn  12287  nnaddcl  12289  nnmulcl  12290  nnsub  12310  nndivtr  12313  un0addcl  12559  un0mulcl  12560  elnnnn0  12569  nn0sub  12576  fcdmnn0fsuppg  12586  elz  12615  nnnegz  12616  elz2  12631  znegclb  12654  zaddcl  12657  nzadd  12665  zmulcl  12666  zneo  12701  nneo  12702  zeo  12704  peano5uzi  12707  zindd  12719  eluzsubOLD  12914  uzp1  12919  uzaddcl  12946  ublbneg  12975  eqreznegel  12976  supminf  12977  zsupss  12979  qmulz  12993  qnegcl  13008  irradd  13015  irrmul  13016  xnn0xaddcl  13277  fzrev2  13628  injresinjlem  13826  negmod0  13918  om2uzuzi  13990  uzindi  14023  fsuppmapnn0ub  14036  mptnn0fsuppr  14040  seqexw  14058  seqcl2  14061  seqcl  14063  seqf  14064  monoord  14073  monoord2  14074  sermono  14075  seqsplit  14076  seqcaopr2  14079  seqid3  14087  seqhomo  14090  expcllem  14113  expcl2lem  14114  m1expcl2  14126  faccl  14322  facdiv  14326  facndiv  14327  bccmpl  14348  bccl  14361  hashclb  14397  hasheq0  14402  hashfn  14414  seqcoll  14503  opfi1uzind  14550  ccatalpha  14631  reuccatpfxs1lem  14784  reuccatpfxs1  14785  repswccat  14824  repswrevw  14825  2cshw  14851  2cshwcshw  14864  cshimadifsn  14868  cshco  14875  swrd2lsw  14991  wwlktovf  14995  wwlktovf1  14996  wwlktovfo  14997  wrd2f1tovbij  14999  shftlem  15107  shftf  15118  cjval  15141  cjth  15142  remim  15156  cnpart  15279  uzin2  15383  caubnd2  15396  sqreulem  15398  clim  15530  clim2  15540  lo1o12  15569  climrlim2  15583  lo1resb  15600  o1resb  15602  lo1eq  15604  climmpt2  15609  climshftlem  15610  rlimcld2  15614  climcn1  15628  climcn2  15629  o1dif  15666  iserex  15693  climub  15698  climserle  15699  isercoll  15704  climcau  15707  caurcvg2  15714  caucvgb  15716  summolem3  15750  summolem2a  15751  zsum  15754  fsum  15756  sumss2  15762  fsumcvg2  15763  fsumclf  15774  fsumsplitf  15778  fsumsplit1  15781  sumpr  15784  sumtp  15785  fsumm1  15787  fsum1p  15789  isummulc2  15798  fsum2dlem  15806  fsumcom2  15810  fsumshftm  15817  fsum0diag2  15819  fsumge1  15833  fsum00  15834  fsumabs  15837  telfsumo  15838  telfsumo2  15839  fsumparts  15842  fsumrlim  15847  fsumo1  15848  o1fsum  15849  fsumiun  15857  binomlem  15865  isumshft  15875  isum1p  15877  isumrpcl  15879  climcndslem1  15885  climcndslem2  15886  climcnds  15887  infcvgaux2i  15894  cvgrat  15919  mertens  15922  clim2prod  15924  prodfn0  15930  prodfrec  15931  prodfdiv  15932  ntrivcvgfvn0  15935  prodmolem3  15969  prodmolem2a  15970  zprod  15973  fprod  15977  prodss  15983  fprodser  15985  fprodm1  16003  fprod1p  16004  fprodm1s  16006  fprodp1s  16007  fprodabs  16010  fprodn0  16015  fprod2dlem  16016  fprodcnv  16019  fprodcom2  16020  fproddivf  16023  fprodsplitf  16024  fprodsplit1f  16026  bpolycl  16088  fprodefsum  16131  rpnnen2lem11  16260  mod2eq1n2dvds  16384  mulsucdiv2z  16390  zob  16396  nn0o1gt2  16418  nno  16419  nn0o  16420  divalglem7  16436  bitsf1  16483  sadcp1  16492  smupp1  16517  qnumdencl  16776  iserodd  16873  pcqcl  16894  pcxnn0cl  16898  pcxcl  16899  pcgcd1  16915  dvdsprmpweqle  16924  pcmpt  16930  pcmpt2  16931  pcmptdvds  16932  infpnlem2  16949  infpn2  16951  1arith  16965  elgz  16969  mul4sq  16992  4sqlem13  16995  4sqlem17  16999  4sqlem18  17000  4sqlem19  17001  vdwlem1  17019  vdwlem2  17020  vdwnn  17036  ramtcl2  17049  ramcl  17067  prmonn2  17077  prmodvdslcmf  17085  isstruct2  17186  wunress  17295  wunressOLD  17296  firest  17477  imasaddfnlem  17573  imasvscafn  17582  xpsfrnel2  17609  mreintcl  17638  ismred2  17646  mreexexlemd  17687  mreexexlem3d  17689  mreexexlem4d  17690  iscatd2  17724  catpropd  17752  subsubc  17898  isfunc  17909  inclfusubc  17988  fncnvimaeqv  18164  joindef  18421  joinval  18422  meetdef  18435  meetval  18436  oduclatb  18552  acsdrsel  18588  isacs4lem  18589  isacs5lem  18590  acsdrscl  18591  mgmsscl  18658  mgmpropd  18664  mgm1  18671  gsumvalx  18689  issubmgm  18715  issubmgm2  18716  mgmhmima  18728  sgrppropd  18744  mndpropd  18772  issubm  18816  0subm  18830  insubm  18831  mhmimalem  18837  gsumwsubmcl  18850  gsumwspan  18859  symggrplem  18897  sursubmefmnd  18909  injsubmefmnd  18910  smndex1basss  18918  mulgsubcl  19106  issubg  19144  issubg2  19159  issubg4  19163  0subg  19169  0subgOLD  19170  isnsg  19173  isnsg2  19174  nsgbi  19175  isnsg3  19178  elnmz  19181  nmzbi  19182  nmzsubg  19183  eqgval  19195  eqgid  19198  cycsubgcl  19224  ghmrn  19247  ghmnsgima  19258  gass  19319  oppgsubg  19382  f1omvdconj  19464  symgfisg  19486  psgneldm  19521  0subgALT  19586  odhash3  19594  sylow2blem2  19639  lsmsubm  19671  lsmsubg  19672  efgsf  19747  efgsdm  19748  efgs1b  19754  efgredlema  19758  eqgabl  19852  ablnsg  19865  cyggenod2  19903  gsumzaddlem  19939  gsummhm2  19957  gsum2dlem2  19989  gsum2d2lem  19991  gsumcom2  19993  dprdfeq0  20042  dprdsubg  20044  dprd2da  20062  ablfacrp  20086  pgpfac1lem3  20097  pgpfaclem1  20101  ablfaclem3  20107  ablfac2  20109  cycsubggenodd  20129  isrng  20151  issrg  20185  srgfcl  20193  rglcom4d  20208  srgbinomlem4  20226  isring  20234  iscrng  20237  dvdsr  20362  irredrmul  20427  isrngim  20445  isrim0OLD  20481  isrim0  20483  issubrng  20547  subrngringnsg  20553  issubrng2  20558  rhmimasubrnglem  20565  issubrg  20571  issubrg2  20592  subrgpropd  20608  isdrngd  20765  isdrngdOLD  20767  issdrg  20789  sdrgacs  20802  issrngd  20856  islmod  20862  lmodlema  20863  islmodd  20864  lmodprop2d  20922  rmodislmodlem  20927  rmodislmod  20928  lssset  20931  islssd  20933  lsscl  20940  lsslss  20959  lsspropd  21016  lmhmima  21046  lbsind  21079  lsmcl  21082  islvec  21103  lmhmlvec  21109  lspsolvlem  21144  lspsolv  21145  lvecpropd  21169  rnglidlmcl  21226  rnglidl0  21239  rnglidlmmgm  21255  rngqiprngimf1lem  21304  rngqiprngimf1  21310  ring2idlqus  21319  xrsdsreclblem  21430  xrsdsreclb  21431  cnsubrglem  21434  prmirred  21485  pzriprnglem4  21495  pzriprnglem8  21499  pzriprngALT  21506  znunithash  21583  cofipsgn  21611  zrhpsgnelbas  21612  rzgrp  21641  isphl  21646  phllmhm  21650  ipcl  21651  isphld  21672  phlpropd  21673  phlssphl  21677  cssincl  21706  pjdm  21727  dsmmval  21754  dsmmbas2  21757  dsmmelbas  21759  frlmbas  21775  frlmup1  21818  lindfind  21836  lindsind  21837  f1lindf  21842  islindf4  21858  psrbag  21937  psrbaglefi  21946  mplsubglem  22019  mpllsslem  22020  ltbwe  22062  psrbagsn  22087  subrgasclcl  22091  mplind  22094  mpfind  22131  psdmul  22170  coe1mul2lem2  22271  gsumply1eq  22313  evl1vsd  22348  mpfpf1  22355  pf1mpf  22356  pf1ind  22359  matecl  22431  m1detdiag  22603  mdetralt  22614  mdetralt2  22615  mdetunilem2  22619  mdetunilem9  22626  m2detleiblem3  22635  m2detleiblem4  22636  smadiadetlem0  22667  cpmatacl  22722  chpscmat  22848  uniopn  22903  inopn  22905  fiinopn  22907  istps  22940  fctop  23011  iscld  23035  isopn2  23040  mretopd  23100  iscldtop  23103  perfi  23163  tgrest  23167  restcld  23180  ordtbaslem  23196  ordtrest2lem  23211  ordtrest2  23212  iscn  23243  cnpval  23244  iscnp  23245  tgcn  23260  subbascn  23262  ssidcn  23263  lmbrf  23268  cnpnei  23272  cnima  23273  iscncl  23277  cnconst2  23291  cnrest2  23294  cnpresti  23296  cnprest  23297  cnindis  23300  lmres  23308  lmcnp  23312  iscnrm  23331  t1sncld  23334  cnrmi  23368  cncmp  23400  cmpsublem  23407  fiuncmp  23412  unconn  23437  conncompid  23439  conncompconn  23440  conncompss  23441  1stcfb  23453  2ndcrest  23462  2ndcctbss  23463  2ndcdisj  23464  1stccnp  23470  islly  23476  isnlly  23477  subislly  23489  restnlly  23490  restlly  23491  islly2  23492  hausllycmp  23502  cldllycmp  23503  dislly  23505  isptfin  23524  islocfin  23525  ptfinfin  23527  finlocfin  23528  dissnlocfin  23537  locfindis  23538  comppfsc  23540  kgenval  23543  elkgen  23544  kgeni  23545  cmpkgen  23559  1stckgenlem  23561  kgencn2  23565  ptpjpre1  23579  elpt  23580  elptr  23581  ptbasin  23585  xkobval  23594  xkoval  23595  xkoopn  23597  txbasval  23614  tx1cn  23617  tx2cn  23618  dfac14  23626  xkoccn  23627  txcnp  23628  ptcnplem  23629  txcnmpt  23632  txindislem  23641  txdis1cn  23643  txlly  23644  txnlly  23645  pthaus  23646  ptrescn  23647  hauseqlcld  23654  txlm  23656  tx2ndc  23659  txkgen  23660  xkoptsub  23662  xkopt  23663  xkoco1cn  23665  xkoco2cn  23666  xkococnlem  23667  xkococn  23668  cnmpt11  23671  cnmpt12  23675  cnmpt21  23679  cnmpt22  23682  cnmptkp  23688  cnmptk1p  23693  xkoinjcn  23695  txconn  23697  qtopval2  23704  elqtop  23705  idqtop  23714  qtopcld  23721  qtopeu  23724  qtoprest  23725  qtopomap  23726  qtopcmap  23727  ishmeo  23767  hmeoopn  23774  hmeocld  23775  ordthmeolem  23809  ptcmpfi  23821  elmptrab  23835  fgcl  23886  trfil2  23895  cfinfil  23901  uzrest  23905  ufilss  23913  trufil  23918  cfinufil  23936  ufinffr  23937  ufildr  23939  rnelfm  23961  flfcntr  24051  ptcmplem2  24061  ptcmplem3  24062  ptcmplem4  24063  ptcmplem5  24064  cnextfvval  24073  tmdcn2  24097  tmdmulg  24100  tmdgsum2  24104  symgtgp  24114  opnsubg  24116  clssubg  24117  tgpconncompeqg  24120  ghmcnp  24123  tgphaus  24125  tgpt0  24127  qustgpopn  24128  qustgplem  24129  tsmsgsum  24147  tsmssubm  24151  tsmsres  24152  tsmsf1o  24153  tsmsxplem1  24161  tsmsxplem2  24162  tsmsxp  24163  istrg  24172  istdrg  24174  istdrg2  24186  istlm  24193  istvc  24200  ustval  24211  ustincl  24216  ustdiag  24217  ustinvel  24218  ustexhalf  24219  ust0  24228  ucnima  24290  fmucndlem  24300  prdsdsf  24377  prdsxmet  24379  imasf1oxmet  24385  imasf1omet  24386  prdsxmslem2  24542  metustsym  24568  isnlm  24696  qtopbaslem  24779  xrtgioo  24828  reperflem  24840  fsumcn  24894  expcn  24896  expcnOLD  24898  xrhmeo  24977  cnllycmp  24988  bndth  24990  isclm  25097  lmhmclm  25120  lmmcvg  25295  fmcfil  25306  iscfil3  25307  iscau2  25311  iscau4  25313  iscmet3lem1  25325  iscmet3  25327  cfilres  25330  caussi  25331  equivcfil  25333  flimcfil  25348  bcthlem1  25358  isbn  25372  srabn  25394  ishl2  25404  cmslssbn  25406  cmscsscms  25407  minveclem3b  25462  ivthlem1  25486  ivthlem2  25487  ivthlem3  25488  ivth2  25490  ivthle  25491  ivthle2  25492  ivthicc  25493  ovolficcss  25504  ovolunlem1a  25531  ovolunlem1  25532  ovolfiniun  25536  ovoliunlem1  25537  ovoliunlem3  25539  ovoliun  25540  ovoliun2  25541  shft2rab  25543  ovolshftlem1  25544  sca2rab  25547  ovolscalem1  25548  mblsplit  25567  finiunmbl  25579  volun  25580  volfiniun  25582  voliunlem1  25585  voliunlem3  25587  iunmbl  25588  voliun  25589  volsup  25591  ioombl  25600  ioorcl  25612  vitalilem1  25643  vitalilem2  25644  vitalilem3  25645  vitalilem4  25646  vitali  25648  ismbf1  25659  mbfdm  25661  ismbf  25663  ismbfcn  25664  mbfima  25665  mbfimaicc  25666  ismbfcn2  25673  ismbfd  25674  ismbf2d  25675  mbfeqalem1  25676  mbfmax  25684  mbfposr  25687  mbfposb  25688  ismbf3d  25689  mbfimaopnlem  25690  mbfimaopn2  25692  cncombf  25693  isi1f  25709  i1fd  25716  itg1mulc  25739  mbfi1fseqlem4  25753  itg2lcl  25762  isibl  25800  iblitg  25803  iblcnlem1  25823  iblcnlem  25824  iblrelem  25826  iblpos  25828  itgeqa  25849  itgfsum  25862  itgabs  25870  limcvallem  25906  ellimc  25908  ellimc2  25912  limcmpt  25918  cnmptlimc  25925  dvbsss  25937  cpnfval  25968  elcpn  25970  dvmptfsum  26013  dvle  26046  dvfsumle  26060  dvfsumleOLD  26061  dvfsumge  26062  dvfsumabs  26063  dvfsumrlimf  26065  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsumrlimge0  26071  dvfsumrlim  26072  dvfsumrlim2  26073  dvfsum2  26075  itgsubstlem  26089  itgsubst  26090  mdegcl  26108  deg1nn0clb  26129  isuc1p  26180  plyeq0lem  26249  plyco  26280  plycj  26317  plycjOLD  26319  dvply2g  26326  dvnply2  26329  plydivlem4  26338  fta1lem  26349  fta1  26350  elqaalem1  26361  elqaalem2  26362  elqaalem3  26363  elqaa  26364  ulmcau  26438  radcnv0  26459  radcnvlt1  26461  radcnvle  26463  pserdvlem2  26472  coseq1  26567  efeq1  26570  sinord  26576  efif1olem2  26585  efif1olem4  26587  lognegb  26632  logcj  26648  argimgt0  26654  logtayl  26702  2irrexpq  26773  root1eq1  26798  logrec  26806  2irrexpqALT  26843  angrteqvd  26849  angpieqvdlem  26871  atans  26973  atans2  26974  dmarea  27000  areambl  27001  rlimcnp  27008  rlimcnp2  27009  xrlimcnp  27011  harmonicbnd  27047  harmonicbnd2  27048  lgamcvglem  27083  wilthlem2  27112  wilth  27114  efnnfsumcl  27146  vmacl  27161  efvmacl  27163  efchtdvds  27202  sqff1o  27225  fsumdvdscom  27228  musumsum  27235  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  fsumvma  27257  perfect  27275  dchrelbasd  27283  lgsval  27345  lgsval2lem  27351  lgsdir2lem4  27372  lgsdir2  27374  lgsqrlem1  27390  lgsdchr  27399  m1lgs  27432  2lgs  27451  mul2sq  27463  2sqlem6  27467  2sqblem  27475  2sq2  27477  rplogsumlem2  27529  dchrisumlema  27532  dchrisumlem2  27534  dchrisumlem3  27535  dchrvmasumlem2  27542  dchrvmasumlem3  27543  dchrisum0flblem2  27553  dchrisum0flb  27554  dchrisum0fno1  27555  ostthlem1  27671  nodmon  27695  noextendseq  27712  nodense  27737  madefi  27950  addsproplem1  28002  addsproplem3  28004  addsprop  28009  addsf  28015  addsbdaylem  28049  negsproplem1  28060  negsproplem3  28062  negsprop  28067  negsbdaylem  28088  mulsproplemcbv  28141  mulsproplem1  28142  mulsproplem10  28151  mulsprop  28156  noseqp1  28297  noseqind  28298  peano5n0s  28324  dfn0s2  28336  n0addscl  28347  n0mulscl  28348  n0sbday  28354  n0s0m1  28359  n0subs  28360  n0p1nns  28361  dfnns2  28362  zaddscl  28380  zmulscld  28383  elzn0s  28384  peano5uzs  28390  expscl  28413  pw2bday  28418  zs12bday  28424  mirval  28663  perpneq  28722  isperp2  28723  isperp2d  28724  foot  28730  islnopp  28747  islnoppd  28748  outpasch  28763  hlpasch  28764  ishpg  28767  colopp  28777  colhp  28778  lmif  28793  islmib  28795  lmiinv  28800  trgcopy  28812  trgcopyeu  28814  acopyeu  28842  inaghl  28853  tgasa1  28866  f1otrgitv  28878  f1otrg  28879  isfusgr  29335  opfusgr  29340  fusgrfisbase  29345  fusgrfisstep  29346  nbupgrel  29362  nbumgrvtx  29363  nbusgreledg  29370  edgnbusgreu  29384  nb3grprlem1  29397  uvtxusgrel  29420  cusgredg  29441  cplgr2vpr  29450  cusgrexg  29461  usgredgsscusgredg  29477  fusgrn0degnn0  29517  rusgrnumwrdl2  29604  rgrx0ndm  29611  wlkcomp  29649  wlkdlem2  29701  clwlkcomp  29799  iswwlks  29856  wwlknllvtx  29866  0enwwlksnge1  29884  wlkiswwlks2lem5  29893  wwlksm1edg  29901  wwlksnred  29912  wwlksnext  29913  wwlksnextbi  29914  wwlksnredwwlkn  29915  wwlksnextfun  29918  wwlksnextinj  29919  wwlksnextsurj  29920  wwlksnextbij  29922  wwlksnfi  29926  wwlksnextproplem2  29930  wwlksnextprop  29932  2wlkdlem4  29948  rusgrnumwwlkl1  29988  rusgrnumwwlks  29994  isclwwlk  30003  clwwlk1loop  30007  clwwlkccatlem  30008  clwlkclwwlklem2a1  30011  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwlkclwwlklem3  30020  clwlkclwwlk  30021  clwlkclwwlk2  30022  clwwisshclwwslemlem  30032  clwwisshclwwslem  30033  clwwisshclwws  30034  clwwlknlbonbgr1  30058  clwwlkinwwlk  30059  clwwlkn1  30060  loopclwwlkn1b  30061  clwwlkn1loopb  30062  clwwlkn2  30063  clwwlkel  30065  clwwlkf  30066  clwwlkwwlksb  30073  clwwlkext2edg  30075  wwlksext2clwwlk  30076  wwlksubclwwlk  30077  eleclclwwlknlem2  30080  umgr2cwwk2dif  30083  s2elclwwlknon2  30123  clwwlknonwwlknonb  30125  clwwlknonex2lem2  30127  clwwlknonex2  30128  3wlkdlem4  30181  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  eupth2lem2  30238  eulerpathpr  30259  1vwmgr  30295  3vfriswmgrlem  30296  3vfriswmgr  30297  3cyclfrgrrn1  30304  vdgn1frgrv2  30315  frgrncvvdeqlem3  30320  frgrncvvdeqlem8  30325  frgrncvvdeqlem9  30326  frgrwopregasn  30335  frgrwopregbsn  30336  frgrwopreglem5ALT  30341  frgr2wwlk1  30348  frgr2wwlkeqm  30350  fusgr2wsp2nb  30353  2clwwlk2clwwlklem  30365  extwwlkfabel  30372  nvvop  30628  isnvlem  30629  sspval  30742  nmorepnf  30787  phpar  30843  siilem2  30871  bnsscmcl  30887  ubthlem1  30889  shaddcl  31236  shmulcl  31237  hsn0elch  31267  hhssablo  31282  hhssnvt  31284  hhsssh  31288  shscl  31337  shintcl  31349  chintcl  31351  shincl  31400  chincl  31518  h1datomi  31600  chscllem2  31657  sumspansn  31668  spansncvi  31671  5oalem2  31674  5oalem3  31675  pjini  31718  pjjsi  31719  eigposi  31855  nmoprepnf  31886  nmfnrepnf  31899  dmadjrnb  31925  lnophmlem1  32035  lnophm  32038  nmcopex  32048  lnconi  32052  nmbdfnlb  32069  nmcfnex  32072  imaelshi  32077  rnbra  32126  leopg  32141  pjbdlni  32168  pjhmop  32169  hmopidmch  32172  pjclem4  32218  pj3si  32226  strlem1  32269  atssma  32397  atcv0eq  32398  atcv1  32399  atomli  32401  atcvatlem  32404  cdj3lem2a  32455  cdj3lem3a  32458  xppreima  32655  fmptcof2  32667  aciunf1lem  32672  funcnv4mpt  32679  1stpreimas  32715  f1od2  32732  fpwrelmapffslem  32743  xrofsup  32771  fzspl  32791  fzsplit3  32795  nnindf  32821  fprodex01  32827  fsumiunle  32831  indfval  32841  indf1ofs  32851  gsumhashmul  33064  fzto1st  33123  isslmd  33208  slmdlema  33209  elrgspnlem2  33247  elrgspnlem4  33249  qusker  33377  0nellinds  33398  unitprodclb  33417  nsgmgclem  33439  nsgmgc  33440  nsgqusf1olem2  33442  elrspunidl  33456  prmidlval  33465  prmidlc  33476  opprlidlabs  33513  dfufd2lem  33577  lindsunlem  33675  brfldext  33698  brfinext  33704  finexttrb  33715  extdg1id  33716  fldextrspunlsplem  33723  constrconj  33786  constrfin  33787  smatrcl  33795  submateq  33808  lmatfval  33813  lmatcl  33815  qtophaus  33835  locfinreflem  33839  locfinref  33840  zartopn  33874  zarcmplem  33880  rhmpreimacnlem  33883  xpinpreima  33905  xpinpreima2  33906  cnre2csqlem  33909  tpr2rico  33911  prsdm  33913  prsrn  33914  ordtrest2NEWlem  33921  ordtrest2NEW  33922  zrhcntr  33980  qqhval2  33983  isrrext  34001  ismntoplly  34026  esumcvg  34087  sigaval  34112  issiga  34113  0elsiga  34115  sigaclcu  34118  issgon  34124  prsiga  34132  sigaclci  34133  difelsiga  34134  unelsiga  34135  ispisys2  34154  inelpisys  34155  unelldsys  34159  sigapildsyslem  34162  sigapildsys  34163  ldgenpisyslem1  34164  ldgenpisys  34167  isros  34169  unelros  34172  difelros  34173  fiunelros  34175  inelsros  34179  diffiunisros  34180  rossros  34181  measvuni  34215  measiun  34219  voliune  34230  volfiniune  34231  brfae  34249  ismbfm  34252  mbfmcnvima  34257  mbfmcst  34261  1stmbfm  34262  2ndmbfm  34263  imambfm  34264  sitgval  34334  issibf  34335  sibfima  34340  sitgfval  34343  sitgclg  34344  eulerpartlemelr  34359  eulerpartlemsf  34361  eulerpartleme  34365  eulerpartlemt0  34371  eulerpartlemt  34373  eulerpartgbij  34374  eulerpartlemr  34376  eulerpartlemmf  34377  eulerpartlemgvv  34378  eulerpartlemgs2  34382  eulerpartlemn  34383  eulerpart  34384  cndprobprob  34440  rrvsum  34456  orvcelel  34472  ballotlemodife  34500  ballotlemsdom  34514  ballotlemrv  34522  ballotlemrv1  34523  ballotlemrv2  34524  ballotlem1ri  34537  fsum2dsub  34622  reprinfz1  34637  reprpmtf1o  34641  reprdifc  34642  breprexplema  34645  hgt750lema  34672  hgt750leme  34673  bnj149  34889  bnj222  34897  bnj1112  34997  bnj1148  35010  fineqvrep  35109  gblacfnacd  35113  loop1cycl  35142  subfacp1lem3  35187  subfacp1lem6  35190  erdszelem10  35205  kur14  35221  cvxsconn  35248  cnllysconn  35250  resconn  35251  iscvm  35264  cvmliftlem5  35294  cvmliftlem15  35303  cvmlift2lem1  35307  cvmlift2lem12  35319  cvmlift2lem13  35320  sat1el2xp  35384  fmlasuc  35391  gonan0  35397  gonar  35400  satefvfmla0  35423  msubrn  35534  msubco  35536  ismfs  35554  mvtinf  35560  mclsax  35574  mppspstlem  35576  elmpps  35578  nnuni  35727  dfdm5  35773  dfrn5  35774  elima4  35776  rdgprc0  35794  pprodss4v  35885  elfuns  35916  fnimage  35930  imageval  35931  fwddifval  36163  fwddifnval  36164  fwddifnp1  36166  elhf2g  36177  hfun  36179  hfninf  36187  filnetlem4  36382  onsucconn  36439  onsucsuccmp  36445  limsucncmp  36447  onint1  36450  fveleq  36452  findreccl  36454  nndivsub  36458  weiunse  36469  bj-seex  36923  bj-adjg1  37044  bj-mooreset  37103  bj-ismoored0  37107  bj-ismoored  37108  bj-inftyexpitaudisj  37206  bj-inftyexpidisj  37211  bj-isvec  37288  bj-isclm  37292  csbmpo123  37332  topdifinffinlem  37348  topdifinffin  37349  csbfinxpg  37389  phpreu  37611  finixpnum  37612  lindsenlbs  37622  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem28  37655  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  poimir  37660  mblfinlem3  37666  ex-ovoliunnfl  37670  voliunnfl  37671  volsupnfl  37672  mbfresfi  37673  itgabsnc  37696  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  dvasin  37711  sdclem2  37749  fdc  37752  incsequz  37755  neificl  37760  mettrifi  37764  cntotbnd  37803  cnpwstotbnd  37804  ismtyima  37810  ismtyhmeolem  37811  heiborlem2  37819  heiborlem3  37820  heiborlem4  37821  heiborlem5  37822  heiborlem6  37823  heiborlem10  37827  isrngo  37904  isdivrngo  37957  drngoi  37958  idlval  38020  isidlc  38022  idladdcl  38026  idllmulcl  38027  idlrmulcl  38028  0idl  38032  pridlval  38040  smprngopr  38059  prnc  38074  ispridlc  38077  pridlc  38078  eqrelf  38256  ecex2  38329  imaexALTV  38331  iss2  38345  elcoeleqvrels  38596  elfunsALTV  38693  eldisjs  38723  eleldisjs  38729  fsumshftd  38953  riotaclbgBAD  38955  renegclALT  38964  lshpinN  38990  isopos  39181  oposlem  39183  glbconN  39378  glbconNOLD  39379  lnnat  39429  2at0mat0  39527  islvol2aN  39594  dalawlem13  39885  pclfinclN  39952  lhpoc2N  40017  ltrncnvatb  40140  cdleme11h  40268  cdlemefr32sn2aw  40406  cdlemefs32sn1aw  40416  cdleme32fvaw  40441  cdlemg1fvawlemN  40575  dicelvalN  41180  dih1dimatlem  41331  dihlatat  41339  dihjatcclem4  41423  islpolN  41485  lpolsatN  41490  lpolpolsatN  41491  mapdordlem1a  41636  mapdordlem1  41638  mapdhcl  41729  iscsrg  41970  fzsplitnd  41983  lcmineqlem12  42041  intlewftc  42062  dvrelogpow2b  42069  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  dvle2  42073  aks4d1p8  42088  aks4d1p9  42089  isprimroot  42094  primrootsunit1  42098  primrootscoprmpow  42100  aks6d1c1p1  42108  aks6d1c1p2  42110  aks6d1c1p3  42111  evl1gprodd  42118  hashscontpow  42123  aks6d1c3  42124  aks6d1c2  42131  sticksstones1  42147  sticksstones10  42156  sticksstones11  42157  sticksstones12a  42158  aks6d1c6lem1  42171  unitscyglem5  42200  metakunt26  42231  metakunt29  42234  metakunt30  42235  metakunt32  42237  retire  42354  reelznn0nn  42479  fsuppind  42600  fsuppssindlem2  42602  fsuppssind  42603  isnacs3  42721  nacsfix  42723  mzpclval  42736  mzpcl1  42740  mzpcl2  42741  mzpcl34  42742  mzpexpmpt  42756  mzpsubst  42759  diophin  42783  diophun  42784  2rexfrabdioph  42807  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  rabdiophlem2  42813  diophren  42824  fphpd  42827  fphpdo  42828  fiphp3d  42830  pellexlem1  42840  pell14qrexpclnn0  42877  pellqrex  42890  rmspecnonsq  42918  monotuz  42953  monotoddzzfi  42954  monotoddzz  42955  oddcomabszz  42956  modabsdifz  42998  rmxdioph  43028  expdiophlem2  43034  limsuc2  43053  dfac11  43074  kelac1  43075  dfac21  43078  lsmfgcl  43086  islnm  43089  lnmlssfg  43092  lmhmfgima  43096  pwslnm  43106  unxpwdom3  43107  pwfi2f1o  43108  islnr  43123  hbtlem2  43136  cnsrexpcl  43177  flcidc  43182  mendlmod  43201  proot1ex  43208  oaordnr  43309  omnord1  43318  oenord1  43329  cantnfresb  43337  onmcl  43344  tfsnfin  43365  nadd2rabtr  43397  nadd1rabtr  43401  nadd1rabex  43403  nadd1suc  43405  pwelg  43573  fipjust  43578  elnonrel  43598  elinlem  43611  elcnvlem  43614  ss2iundf  43672  dfhe3  43788  dffrege115  43991  rfovcnvf1od  44017  ntrneiel2  44099  clsneiel2  44122  neicvgel2  44133  grur1cld  44251  dvgrat  44331  cvgdvgrat  44332  radcnvrat  44333  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  modelaxreplem1  44995  modelaxreplem2  44996  modelaxrep  44998  fnchoice  45034  fiiuncl  45070  disjf1  45188  disjinfi  45197  choicefi  45205  axccdom  45227  fmptf  45245  fmptff  45276  monoords  45309  supminfrnmpt  45456  supxrleubrnmptf  45462  supminfxr  45475  supminfxr2  45480  supminfxrrnmpt  45482  monoordxrv  45492  monoordxr  45493  monoord2xrv  45494  monoord2xr  45495  caucvgbf  45500  cvgcaule  45502  fsummulc1f  45586  fsumnncl  45587  fsumf1of  45589  fsumreclf  45591  fsumlessf  45592  fsumsermpt  45594  fmul01  45595  fmulcl  45596  fmuldfeqlem1  45597  fmuldfeq  45598  fmul01lt1lem1  45599  fmul01lt1lem2  45600  fprodexp  45609  fprodabs2  45610  mccllem  45612  mccl  45613  fprodcnlem  45614  fprodcn  45615  climmulf  45619  climsuse  45623  climrecf  45624  climaddf  45630  climf  45637  sumnnodd  45645  clim2f  45651  0ellimcdiv  45664  climsubmpt  45675  climreclf  45679  climf2  45681  fnlimcnv  45682  climeldmeqmpt  45683  clim2f2  45685  climfveqmpt  45686  fnlimfvre  45689  fnlimabslt  45694  climfveqmpt3  45697  climbddf  45702  climeldmeqmpt3  45704  climinf2mpt  45729  climinfmpt  45730  limsupequzmptf  45746  lmbr3  45762  liminfreuzlem  45817  coseq0  45879  cncfshift  45889  cncfperiod  45894  fprodcncf  45915  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvmptmulf  45952  dvnmptdivc  45953  dvnmul  45958  dvmptfprod  45960  iblspltprt  45988  itgspltprt  45994  stoweidlem2  46017  stoweidlem3  46018  stoweidlem4  46019  stoweidlem6  46021  stoweidlem8  46023  stoweidlem17  46032  stoweidlem19  46034  stoweidlem20  46035  stoweidlem21  46036  stoweidlem23  46038  stoweidlem27  46042  stoweidlem35  46050  stoweidlem42  46057  stoweidlem43  46058  stoweidlem62  46077  stoweid  46078  wallispilem3  46082  wallispi  46085  fourierdlem16  46138  fourierdlem21  46143  fourierdlem41  46163  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem51  46172  fourierdlem54  46175  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem71  46192  fourierdlem72  46193  fourierdlem73  46194  fourierdlem83  46204  fourierdlem86  46207  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem96  46217  fourierdlem97  46218  fourierdlem98  46219  fourierdlem99  46220  fourierdlem100  46221  fourierdlem103  46224  fourierdlem104  46225  fourierdlem105  46226  fourierdlem108  46229  fourierdlem109  46230  fourierdlem110  46231  fourierdlem112  46233  fourierdlem113  46234  etransclem24  46273  salunicl  46331  saluncl  46332  saldifcl  46334  sge0f1o  46397  sge0lempt  46425  sge0iunmptlemfi  46428  sge0p1  46429  sge0fodjrnlem  46431  sge0iunmpt  46433  sge0ltfirpmpt2  46441  sge0isummpt2  46447  sge0xaddlem2  46449  sge0xadd  46450  ismea  46466  nnfoctbdjlem  46470  nnfoctbdj  46471  meadjiun  46481  voliunsge0lem  46487  meaiuninclem  46495  meaiuninc3v  46499  hoidmvlelem2  46611  hoidmvlelem3  46612  vonvolmbl2  46678  hoimbl2  46680  vonhoire  46687  vonicclem2  46699  vonn0ioo2  46705  vonn0icc2  46707  salpreimagelt  46722  salpreimalegt  46724  salpreimagtge  46740  salpreimaltle  46741  issmf  46743  salpreimagtlt  46745  smfpreimalt  46746  smfpreimaltf  46751  issmfle  46760  smfpreimale  46769  issmfgt  46771  smfpreimagt  46777  issmfgelem  46784  issmfge  46785  smflimlem4  46789  smflim  46792  smfpreimage  46797  smfresal  46803  smfpimbor1lem1  46813  smfpimbor1lem2  46814  smflim2  46821  smflimmpt  46825  smflimsuplem1  46835  smflimsuplem2  46836  smflimsuplem3  46837  smflimsuplem5  46839  smflimsuplem7  46841  smflimsup  46843  smfliminf  46846  ormkglobd  46890  eu2ndop1stv  47137  dmfcoafv  47187  ffnaov  47211  faovcl  47212  funressndmafv2rn  47235  dfatdmfcoafv2  47266  smonoord  47358  iccpartiltu  47409  iccpartigtl  47410  sprsymrelf1lem  47478  prproropf1olem2  47491  fmtno4prmfac193  47560  proththdlem  47600  proththd  47601  iseven  47615  isodd  47616  dfodd2  47623  evenm1odd  47626  evenp1odd  47627  enege  47632  onego  47633  epee  47692  perfectALTV  47710  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbndlem4  47795  bgoldbtbnd  47796  clnbupgrel  47821  edgusgrclnbfin  47828  isuspgrim0  47872  uspgrimprop  47873  isuspgrimlem  47874  grimuhgr  47878  grimedg  47903  grtriproplem  47906  grtrif1o  47909  isgrtri  47910  grtriclwlk3  47912  cycl3grtrilem  47913  cycl3grtri  47914  grimgrtri  47916  usgrgrtrirex  47917  isubgr3stgrlem7  47939  grlimgrtri  47963  usgrexmpl1tri  47984  gpgvtxel2  48006  gpgvtx0  48008  gpgvtx1  48009  gpgedgvtx0  48019  gpgedgvtx1  48020  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  gpg3kgrtriex  48045  uzlidlring  48151  cbvmpox2  48252  lmod1  48409  nnolog2flm1  48511  dignn0flhalflem1  48536  catprsc  48902  fucofulem2  49006  fucofvalne  49020  isthincd2lem2  49084