Theorem eleq1d 2823

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536  ∃wex 1775   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  eleq1  2826  eleq12d  2832  eqeltrd  2838  eqneltrd  2858  rspcimdv  3611  reuind  3761  sbcel2  4423  sbccsb2  4442  disjiun  5135  breq1  5150  breq2  5151  axrep6g  5295  inex1g  5324  intex  5349  pwexg  5383  reusv2lem4  5406  reusv2  5408  reusv3  5410  rabxfrd  5422  prex  5442  opelopabsb  5539  csbmpt12  5566  pofun  5614  seex  5647  seinxp  5771  opabid2  5840  opeliunxp2  5851  elrn2g  5903  opeldmd  5919  opeldm  5920  elreldm  5948  elsnres  6040  iss  6054  elimasngOLD  6110  unielrel  6295  onunel  6490  funopg  6601  funimaexgOLD  6654  brprcneu  6896  brprcneuALT  6897  tz6.12f  6932  ndmfvrcl  6942  ssimaex  6993  dmfco  7004  fvmpti  7014  fvmpt3  7019  fvmptf  7036  fvmptss2  7041  respreima  7085  fvn0ssdmfun  7093  fvelrn  7095  ffnfvf  7139  ffvresb  7144  fmptco  7148  fmptcof  7149  fsn  7154  fsn2g  7157  fressnfv  7179  fvrnressn  7180  fvn0fvelrnOLD  7182  fnex  7236  funfvima  7249  funfvima3  7255  f1mpt  7280  fliftfuns  7333  isoselem  7360  isowe2  7369  riotaclb  7428  ovrspc2v  7456  ffnov  7558  fovcld  7559  ovmpos  7580  ov2gf  7581  ovg  7597  funimassov  7609  oprssdm  7613  ndmovrcl  7618  caovclg  7624  elovmpo  7677  ofmpteq  7719  sorpsscmpl  7752  uniexg  7758  unexbOLD  7766  abnexg  7774  difsnexi  7779  onint  7809  limsuc  7869  tfisi  7879  peano5  7915  xpexr  7940  xpexcnv  7942  fnexALT  7973  focdmex  7978  f1stres  8036  f2ndres  8037  xp1st  8044  xp2nd  8045  unielxp  8050  opiota  8082  fmpox  8090  offval22  8111  frxp  8149  fnse  8156  frxp2  8167  sexp2  8169  frxp3  8174  sexp3  8176  opeliunxp2f  8233  dftpos4  8268  fvmpocurryd  8294  undefnel2  8300  onnseq  8382  smoel  8398  smo11  8402  tfrlem8  8422  tfrlem9  8423  tfrlem15  8430  tfr2b  8434  tz7.44-2  8445  tz7.44-3  8446  oacl  8571  omcl  8572  oecl  8573  oaord1  8587  omordi  8602  oen0  8622  oeeui  8638  nnacl  8647  nnmcl  8648  nnecl  8649  nnmordi  8667  nnaordex  8674  omsmolem  8693  naddcllem  8712  naddov2  8715  naddf  8717  naddssim  8721  naddelim  8722  naddasslem1  8730  naddasslem2  8731  naddsuc2  8737  erexb  8768  qliftfuns  8842  ixpsnval  8938  elixp2  8939  resixp  8971  undifixp  8972  mptelixpg  8973  resixpfo  8974  elixpsn  8975  fundmen  9069  fopwdom  9118  disjen  9172  xpf1o  9177  unfi  9209  cnvfi  9214  fnfi  9215  f1oenfirn  9217  f1domfi  9218  unblem2  9326  imafiOLD  9351  pwfi  9354  xpfiOLD  9356  fiint  9363  fiintOLD  9364  iunfi  9380  isfsupp  9402  fsuppun  9424  ffsuppbi  9435  elfi2  9451  wdom2d  9617  ixpiunwdom  9627  dfom3  9684  cantnfvalf  9702  cantnflt  9709  cantnflem1  9726  r1fin  9810  tz9.12lem3  9826  ranksnb  9864  ranklim  9881  r1pw  9882  r1pwALT  9883  r1pwcl  9884  rankuni2b  9890  djuexb  9946  cardmin2  10036  infxpenc2lem1  10056  dfac8alem  10066  dfac8clem  10069  ac5num  10073  acni2  10083  acnlem  10085  alephon  10106  alephfplem3  10143  alephfplem4  10144  dfac4  10159  dfac5lem1  10160  dfac5lem5  10164  dfac2a  10167  dfac2b  10168  dfacacn  10179  dfac12lem2  10182  dfac12r  10184  dfac12k  10185  cofsmo  10306  cfsmolem  10307  isfin1a  10329  fin1ai  10330  isfin3  10333  infpssrlem3  10342  fin23lem7  10353  fin23lem11  10354  enfin2i  10358  isf34lem4  10414  fin1a2lem7  10443  hsmexlem9  10462  hsmexlem4  10466  hsmex  10469  axcc2lem  10473  axcc3  10475  axdc3lem2  10488  axcclem  10494  zornn0g  10542  ttukeylem3  10548  ttukeylem6  10551  ttukey2g  10553  brdom7disj  10568  brdom6disj  10569  fnct  10574  konigthlem  10605  axregndlem2  10640  axinfnd  10643  axacndlem5  10648  axacnd  10649  fpwwe2lem4  10671  fpwwe2lem12  10679  fpwwe  10683  pwfseqlem1  10695  pwfseqlem3  10697  pwfseqlem4a  10698  pwfseqlem4  10699  wununi  10743  wunpw  10744  wunpr  10746  wunr1om  10756  tskpw  10790  tskr1om  10804  inar1  10812  grupw  10832  grupr  10834  gruurn  10835  gruiun  10836  ingru  10852  grur1a  10856  grothomex  10866  grothac  10867  addnidpi  10938  indpi  10944  adderpq  10993  mulerpq  10994  addclprlem2  11054  mulclprlem  11056  distrlem4pr  11063  prlem934  11070  ltexprlem3  11075  ltexprlem4  11076  ltexprlem7  11079  ltexpri  11080  prlem936  11084  reclem2pr  11085  reclem3pr  11086  addclsr  11120  mulclsr  11121  supsrlem  11148  supsr  11149  axaddf  11182  axmulf  11183  axaddrcl  11189  axmulrcl  11191  renegcl  11569  negreb  11571  negn0  11689  negf1o  11690  ltord1  11786  leord1  11787  eqord1  11788  ltord2  11789  leord2  11790  eqord2  11791  negfi  12214  infm3  12224  cju  12259  peano5nni  12266  peano2nn  12275  dfnn2  12276  nn1m1nn  12284  nnaddcl  12286  nnmulcl  12287  nnsub  12307  nndivtr  12310  un0addcl  12556  un0mulcl  12557  elnnnn0  12566  nn0sub  12573  fcdmnn0fsuppg  12583  elz  12612  nnnegz  12613  elz2  12628  znegclb  12651  zaddcl  12654  nzadd  12662  zmulcl  12663  zneo  12698  nneo  12699  zeo  12701  peano5uzi  12704  zindd  12716  eluzsubOLD  12911  uzp1  12916  uzaddcl  12943  ublbneg  12972  eqreznegel  12973  supminf  12974  zsupss  12976  qmulz  12990  qnegcl  13005  irradd  13012  irrmul  13013  xnn0xaddcl  13273  fzrev2  13624  injresinjlem  13822  negmod0  13914  om2uzuzi  13986  uzindi  14019  fsuppmapnn0ub  14032  mptnn0fsuppr  14036  seqexw  14054  seqcl2  14057  seqcl  14059  seqf  14060  monoord  14069  monoord2  14070  sermono  14071  seqsplit  14072  seqcaopr2  14075  seqid3  14083  seqhomo  14086  expcllem  14109  expcl2lem  14110  m1expcl2  14122  faccl  14318  facdiv  14322  facndiv  14323  bccmpl  14344  bccl  14357  hashclb  14393  hasheq0  14398  hashfn  14410  seqcoll  14499  opfi1uzind  14546  ccatalpha  14627  reuccatpfxs1lem  14780  reuccatpfxs1  14781  repswccat  14820  repswrevw  14821  2cshw  14847  2cshwcshw  14860  cshimadifsn  14864  cshco  14871  swrd2lsw  14987  wwlktovf  14991  wwlktovf1  14992  wwlktovfo  14993  wrd2f1tovbij  14995  shftlem  15103  shftf  15114  cjval  15137  cjth  15138  remim  15152  cnpart  15275  uzin2  15379  caubnd2  15392  sqreulem  15394  clim  15526  clim2  15536  lo1o12  15565  climrlim2  15579  lo1resb  15596  o1resb  15598  lo1eq  15600  climmpt2  15605  climshftlem  15606  rlimcld2  15610  climcn1  15624  climcn2  15625  o1dif  15662  iserex  15689  climub  15694  climserle  15695  isercoll  15700  climcau  15703  caurcvg2  15710  caucvgb  15712  summolem3  15746  summolem2a  15747  zsum  15750  fsum  15752  sumss2  15758  fsumcvg2  15759  fsumclf  15770  fsumsplitf  15774  fsumsplit1  15777  sumpr  15780  sumtp  15781  fsumm1  15783  fsum1p  15785  isummulc2  15794  fsum2dlem  15802  fsumcom2  15806  fsumshftm  15813  fsum0diag2  15815  fsumge1  15829  fsum00  15830  fsumabs  15833  telfsumo  15834  telfsumo2  15835  fsumparts  15838  fsumrlim  15843  fsumo1  15844  o1fsum  15845  fsumiun  15853  binomlem  15861  isumshft  15871  isum1p  15873  isumrpcl  15875  climcndslem1  15881  climcndslem2  15882  climcnds  15883  infcvgaux2i  15890  cvgrat  15915  mertens  15918  clim2prod  15920  prodfn0  15926  prodfrec  15927  prodfdiv  15928  ntrivcvgfvn0  15931  prodmolem3  15965  prodmolem2a  15966  zprod  15969  fprod  15973  prodss  15979  fprodser  15981  fprodm1  15999  fprod1p  16000  fprodm1s  16002  fprodp1s  16003  fprodabs  16006  fprodn0  16011  fprod2dlem  16012  fprodcnv  16015  fprodcom2  16016  fproddivf  16019  fprodsplitf  16020  fprodsplit1f  16022  bpolycl  16084  fprodefsum  16127  rpnnen2lem11  16256  mod2eq1n2dvds  16380  mulsucdiv2z  16386  zob  16392  nn0o1gt2  16414  nno  16415  nn0o  16416  divalglem7  16432  bitsf1  16479  sadcp1  16488  smupp1  16513  qnumdencl  16772  iserodd  16868  pcqcl  16889  pcxnn0cl  16893  pcxcl  16894  pcgcd1  16910  dvdsprmpweqle  16919  pcmpt  16925  pcmpt2  16926  pcmptdvds  16927  infpnlem2  16944  infpn2  16946  1arith  16960  elgz  16964  mul4sq  16987  4sqlem13  16990  4sqlem17  16994  4sqlem18  16995  4sqlem19  16996  vdwlem1  17014  vdwlem2  17015  vdwnn  17031  ramtcl2  17044  ramcl  17062  prmonn2  17072  prmodvdslcmf  17080  isstruct2  17182  wunress  17295  wunressOLD  17296  firest  17478  imasaddfnlem  17574  imasvscafn  17583  xpsfrnel2  17610  mreintcl  17639  ismred2  17647  mreexexlemd  17688  mreexexlem3d  17690  mreexexlem4d  17691  iscatd2  17725  catpropd  17753  subsubc  17903  isfunc  17914  inclfusubc  17994  fncnvimaeqv  18174  joindef  18433  joinval  18434  meetdef  18447  meetval  18448  oduclatb  18564  acsdrsel  18600  isacs4lem  18601  isacs5lem  18602  acsdrscl  18603  mgmsscl  18670  mgmpropd  18676  mgm1  18683  gsumvalx  18701  issubmgm  18727  issubmgm2  18728  mgmhmima  18740  sgrppropd  18756  mndpropd  18784  issubm  18828  0subm  18842  insubm  18843  mhmimalem  18849  gsumwsubmcl  18862  gsumwspan  18871  symggrplem  18909  sursubmefmnd  18921  injsubmefmnd  18922  smndex1basss  18930  mulgsubcl  19118  issubg  19156  issubg2  19171  issubg4  19175  0subg  19181  0subgOLD  19182  isnsg  19185  isnsg2  19186  nsgbi  19187  isnsg3  19190  elnmz  19193  nmzbi  19194  nmzsubg  19195  eqgval  19207  eqgid  19210  cycsubgcl  19236  ghmrn  19259  ghmnsgima  19270  gass  19331  oppgsubg  19396  f1omvdconj  19478  symgfisg  19500  psgneldm  19535  0subgALT  19600  odhash3  19608  sylow2blem2  19653  lsmsubm  19685  lsmsubg  19686  efgsf  19761  efgsdm  19762  efgs1b  19768  efgredlema  19772  eqgabl  19866  ablnsg  19879  cyggenod2  19917  gsumzaddlem  19953  gsummhm2  19971  gsum2dlem2  20003  gsum2d2lem  20005  gsumcom2  20007  dprdfeq0  20056  dprdsubg  20058  dprd2da  20076  ablfacrp  20100  pgpfac1lem3  20111  pgpfaclem1  20115  ablfaclem3  20121  ablfac2  20123  cycsubggenodd  20143  isrng  20171  issrg  20205  srgfcl  20213  rglcom4d  20228  srgbinomlem4  20246  isring  20254  iscrng  20257  dvdsr  20378  irredrmul  20443  isrngim  20461  isrim0OLD  20497  isrim0  20499  issubrng  20563  subrngringnsg  20569  issubrng2  20574  rhmimasubrnglem  20581  issubrg  20587  issubrg2  20608  subrgpropd  20624  isdrngd  20781  isdrngdOLD  20783  issdrg  20805  sdrgacs  20818  issrngd  20872  islmod  20878  lmodlema  20879  islmodd  20880  lmodprop2d  20938  rmodislmodlem  20943  rmodislmod  20944  rmodislmodOLD  20945  lssset  20948  islssd  20950  lsscl  20957  lsslss  20976  lsspropd  21033  lmhmima  21063  lbsind  21096  lsmcl  21099  islvec  21120  lmhmlvec  21126  lspsolvlem  21161  lspsolv  21162  lvecpropd  21186  rnglidlmcl  21243  rnglidl0  21256  rnglidlmmgm  21272  rngqiprngimf1lem  21321  rngqiprngimf1  21327  ring2idlqus  21336  xrsdsreclblem  21447  xrsdsreclb  21448  cnsubrglem  21451  prmirred  21502  pzriprnglem4  21512  pzriprnglem8  21516  pzriprngALT  21523  znunithash  21600  cofipsgn  21628  zrhpsgnelbas  21629  rzgrp  21658  isphl  21663  phllmhm  21667  ipcl  21668  isphld  21689  phlpropd  21690  phlssphl  21694  cssincl  21723  pjdm  21744  dsmmval  21771  dsmmbas2  21774  dsmmelbas  21776  frlmbas  21792  frlmup1  21835  lindfind  21853  lindsind  21854  f1lindf  21859  islindf4  21875  psrbag  21954  psrbaglefi  21963  mplsubglem  22036  mpllsslem  22037  ltbwe  22079  psrbagsn  22104  subrgasclcl  22108  mplind  22111  mpfind  22148  psdmul  22187  coe1mul2lem2  22286  gsumply1eq  22328  evl1vsd  22363  mpfpf1  22370  pf1mpf  22371  pf1ind  22374  matecl  22446  m1detdiag  22618  mdetralt  22629  mdetralt2  22630  mdetunilem2  22634  mdetunilem9  22641  m2detleiblem3  22650  m2detleiblem4  22651  smadiadetlem0  22682  cpmatacl  22737  chpscmat  22863  uniopn  22918  inopn  22920  fiinopn  22922  istps  22955  fctop  23026  iscld  23050  isopn2  23055  mretopd  23115  iscldtop  23118  perfi  23178  tgrest  23182  restcld  23195  ordtbaslem  23211  ordtrest2lem  23226  ordtrest2  23227  iscn  23258  cnpval  23259  iscnp  23260  tgcn  23275  subbascn  23277  ssidcn  23278  lmbrf  23283  cnpnei  23287  cnima  23288  iscncl  23292  cnconst2  23306  cnrest2  23309  cnpresti  23311  cnprest  23312  cnindis  23315  lmres  23323  lmcnp  23327  iscnrm  23346  t1sncld  23349  cnrmi  23383  cncmp  23415  cmpsublem  23422  fiuncmp  23427  unconn  23452  conncompid  23454  conncompconn  23455  conncompss  23456  1stcfb  23468  2ndcrest  23477  2ndcctbss  23478  2ndcdisj  23479  1stccnp  23485  islly  23491  isnlly  23492  subislly  23504  restnlly  23505  restlly  23506  islly2  23507  hausllycmp  23517  cldllycmp  23518  dislly  23520  isptfin  23539  islocfin  23540  ptfinfin  23542  finlocfin  23543  dissnlocfin  23552  locfindis  23553  comppfsc  23555  kgenval  23558  elkgen  23559  kgeni  23560  cmpkgen  23574  1stckgenlem  23576  kgencn2  23580  ptpjpre1  23594  elpt  23595  elptr  23596  ptbasin  23600  xkobval  23609  xkoval  23610  xkoopn  23612  txbasval  23629  tx1cn  23632  tx2cn  23633  dfac14  23641  xkoccn  23642  txcnp  23643  ptcnplem  23644  txcnmpt  23647  txindislem  23656  txdis1cn  23658  txlly  23659  txnlly  23660  pthaus  23661  ptrescn  23662  hauseqlcld  23669  txlm  23671  tx2ndc  23674  txkgen  23675  xkoptsub  23677  xkopt  23678  xkoco1cn  23680  xkoco2cn  23681  xkococnlem  23682  xkococn  23683  cnmpt11  23686  cnmpt12  23690  cnmpt21  23694  cnmpt22  23697  cnmptkp  23703  cnmptk1p  23708  xkoinjcn  23710  txconn  23712  qtopval2  23719  elqtop  23720  idqtop  23729  qtopcld  23736  qtopeu  23739  qtoprest  23740  qtopomap  23741  qtopcmap  23742  ishmeo  23782  hmeoopn  23789  hmeocld  23790  ordthmeolem  23824  ptcmpfi  23836  elmptrab  23850  fgcl  23901  trfil2  23910  cfinfil  23916  uzrest  23920  ufilss  23928  trufil  23933  cfinufil  23951  ufinffr  23952  ufildr  23954  rnelfm  23976  flfcntr  24066  ptcmplem2  24076  ptcmplem3  24077  ptcmplem4  24078  ptcmplem5  24079  cnextfvval  24088  tmdcn2  24112  tmdmulg  24115  tmdgsum2  24119  symgtgp  24129  opnsubg  24131  clssubg  24132  tgpconncompeqg  24135  ghmcnp  24138  tgphaus  24140  tgpt0  24142  qustgpopn  24143  qustgplem  24144  tsmsgsum  24162  tsmssubm  24166  tsmsres  24167  tsmsf1o  24168  tsmsxplem1  24176  tsmsxplem2  24177  tsmsxp  24178  istrg  24187  istdrg  24189  istdrg2  24201  istlm  24208  istvc  24215  ustval  24226  ustincl  24231  ustdiag  24232  ustinvel  24233  ustexhalf  24234  ust0  24243  ucnima  24305  fmucndlem  24315  prdsdsf  24392  prdsxmet  24394  imasf1oxmet  24400  imasf1omet  24401  prdsxmslem2  24557  metustsym  24583  isnlm  24711  qtopbaslem  24794  xrtgioo  24841  reperflem  24853  fsumcn  24907  expcn  24909  expcnOLD  24911  xrhmeo  24990  cnllycmp  25001  bndth  25003  isclm  25110  lmhmclm  25133  lmmcvg  25308  fmcfil  25319  iscfil3  25320  iscau2  25324  iscau4  25326  iscmet3lem1  25338  iscmet3  25340  cfilres  25343  caussi  25344  equivcfil  25346  flimcfil  25361  bcthlem1  25371  isbn  25385  srabn  25407  ishl2  25417  cmslssbn  25419  cmscsscms  25420  minveclem3b  25475  ivthlem1  25499  ivthlem2  25500  ivthlem3  25501  ivth2  25503  ivthle  25504  ivthle2  25505  ivthicc  25506  ovolficcss  25517  ovolunlem1a  25544  ovolunlem1  25545  ovolfiniun  25549  ovoliunlem1  25550  ovoliunlem3  25552  ovoliun  25553  ovoliun2  25554  shft2rab  25556  ovolshftlem1  25557  sca2rab  25560  ovolscalem1  25561  mblsplit  25580  finiunmbl  25592  volun  25593  volfiniun  25595  voliunlem1  25598  voliunlem3  25600  iunmbl  25601  voliun  25602  volsup  25604  ioombl  25613  ioorcl  25625  vitalilem1  25656  vitalilem2  25657  vitalilem3  25658  vitalilem4  25659  vitali  25661  ismbf1  25672  mbfdm  25674  ismbf  25676  ismbfcn  25677  mbfima  25678  mbfimaicc  25679  ismbfcn2  25686  ismbfd  25687  ismbf2d  25688  mbfeqalem1  25689  mbfmax  25697  mbfposr  25700  mbfposb  25701  ismbf3d  25702  mbfimaopnlem  25703  mbfimaopn2  25705  cncombf  25706  isi1f  25722  i1fd  25729  itg1mulc  25753  mbfi1fseqlem4  25767  itg2lcl  25776  isibl  25814  iblitg  25817  iblcnlem1  25837  iblcnlem  25838  iblrelem  25840  iblpos  25842  itgeqa  25863  itgfsum  25876  itgabs  25884  limcvallem  25920  ellimc  25922  ellimc2  25926  limcmpt  25932  cnmptlimc  25939  dvbsss  25951  cpnfval  25982  elcpn  25984  dvmptfsum  26027  dvle  26060  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  dvfsumrlimf  26079  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsumrlimge0  26085  dvfsumrlim  26086  dvfsumrlim2  26087  dvfsum2  26089  itgsubstlem  26103  itgsubst  26104  mdegcl  26122  deg1nn0clb  26143  isuc1p  26194  plyeq0lem  26263  plyco  26294  plycj  26331  plycjOLD  26333  dvply2g  26340  dvnply2  26343  plydivlem4  26352  fta1lem  26363  fta1  26364  elqaalem1  26375  elqaalem2  26376  elqaalem3  26377  elqaa  26378  ulmcau  26452  radcnv0  26473  radcnvlt1  26475  radcnvle  26477  pserdvlem2  26486  coseq1  26581  efeq1  26584  sinord  26590  efif1olem2  26599  efif1olem4  26601  lognegb  26646  logcj  26662  argimgt0  26668  logtayl  26716  2irrexpq  26787  root1eq1  26812  logrec  26820  2irrexpqALT  26857  angrteqvd  26863  angpieqvdlem  26885  atans  26987  atans2  26988  dmarea  27014  areambl  27015  rlimcnp  27022  rlimcnp2  27023  xrlimcnp  27025  harmonicbnd  27061  harmonicbnd2  27062  lgamcvglem  27097  wilthlem2  27126  wilth  27128  efnnfsumcl  27160  vmacl  27175  efvmacl  27177  efchtdvds  27216  sqff1o  27239  fsumdvdscom  27242  musumsum  27249  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  fsumvma  27271  perfect  27289  dchrelbasd  27297  lgsval  27359  lgsval2lem  27365  lgsdir2lem4  27386  lgsdir2  27388  lgsqrlem1  27404  lgsdchr  27413  m1lgs  27446  2lgs  27465  mul2sq  27477  2sqlem6  27481  2sqblem  27489  2sq2  27491  rplogsumlem2  27543  dchrisumlema  27546  dchrisumlem2  27548  dchrisumlem3  27549  dchrvmasumlem2  27556  dchrvmasumlem3  27557  dchrisum0flblem2  27567  dchrisum0flb  27568  dchrisum0fno1  27569  ostthlem1  27685  nodmon  27709  noextendseq  27726  nodense  27751  madefi  27964  addsproplem1  28016  addsproplem3  28018  addsprop  28023  addsf  28029  addsbdaylem  28063  negsproplem1  28074  negsproplem3  28076  negsprop  28081  negsbdaylem  28102  mulsproplemcbv  28155  mulsproplem1  28156  mulsproplem10  28165  mulsprop  28170  noseqp1  28311  noseqind  28312  peano5n0s  28338  dfn0s2  28350  n0addscl  28361  n0mulscl  28362  n0sbday  28368  n0s0m1  28373  n0subs  28374  n0p1nns  28375  dfnns2  28376  zaddscl  28394  zmulscld  28397  elzn0s  28398  peano5uzs  28404  expscl  28427  pw2bday  28432  zs12bday  28438  mirval  28677  perpneq  28736  isperp2  28737  isperp2d  28738  foot  28744  islnopp  28761  islnoppd  28762  outpasch  28777  hlpasch  28778  ishpg  28781  colopp  28791  colhp  28792  lmif  28807  islmib  28809  lmiinv  28814  trgcopy  28826  trgcopyeu  28828  acopyeu  28856  inaghl  28867  tgasa1  28880  f1otrgitv  28892  f1otrg  28893  isfusgr  29349  opfusgr  29354  fusgrfisbase  29359  fusgrfisstep  29360  nbupgrel  29376  nbumgrvtx  29377  nbusgreledg  29384  edgnbusgreu  29398  nb3grprlem1  29411  uvtxusgrel  29434  cusgredg  29455  cplgr2vpr  29464  cusgrexg  29475  usgredgsscusgredg  29491  fusgrn0degnn0  29531  rusgrnumwrdl2  29618  rgrx0ndm  29625  wlkcomp  29663  wlkdlem2  29715  clwlkcomp  29811  iswwlks  29865  wwlknllvtx  29875  0enwwlksnge1  29893  wlkiswwlks2lem5  29902  wwlksm1edg  29910  wwlksnred  29921  wwlksnext  29922  wwlksnextbi  29923  wwlksnredwwlkn  29924  wwlksnextfun  29927  wwlksnextinj  29928  wwlksnextsurj  29929  wwlksnextbij  29931  wwlksnfi  29935  wwlksnextproplem2  29939  wwlksnextprop  29941  2wlkdlem4  29957  rusgrnumwwlkl1  29997  rusgrnumwwlks  30003  isclwwlk  30012  clwwlk1loop  30016  clwwlkccatlem  30017  clwlkclwwlklem2a1  30020  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwlkclwwlklem3  30029  clwlkclwwlk  30030  clwlkclwwlk2  30031  clwwisshclwwslemlem  30041  clwwisshclwwslem  30042  clwwisshclwws  30043  clwwlknlbonbgr1  30067  clwwlkinwwlk  30068  clwwlkn1  30069  loopclwwlkn1b  30070  clwwlkn1loopb  30071  clwwlkn2  30072  clwwlkel  30074  clwwlkf  30075  clwwlkwwlksb  30082  clwwlkext2edg  30084  wwlksext2clwwlk  30085  wwlksubclwwlk  30086  eleclclwwlknlem2  30089  umgr2cwwk2dif  30092  s2elclwwlknon2  30132  clwwlknonwwlknonb  30134  clwwlknonex2lem2  30136  clwwlknonex2  30137  3wlkdlem4  30190  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  eupth2lem2  30247  eulerpathpr  30268  1vwmgr  30304  3vfriswmgrlem  30305  3vfriswmgr  30306  3cyclfrgrrn1  30313  vdgn1frgrv2  30324  frgrncvvdeqlem3  30329  frgrncvvdeqlem8  30334  frgrncvvdeqlem9  30335  frgrwopregasn  30344  frgrwopregbsn  30345  frgrwopreglem5ALT  30350  frgr2wwlk1  30357  frgr2wwlkeqm  30359  fusgr2wsp2nb  30362  2clwwlk2clwwlklem  30374  extwwlkfabel  30381  nvvop  30637  isnvlem  30638  sspval  30751  nmorepnf  30796  phpar  30852  siilem2  30880  bnsscmcl  30896  ubthlem1  30898  shaddcl  31245  shmulcl  31246  hsn0elch  31276  hhssablo  31291  hhssnvt  31293  hhsssh  31297  shscl  31346  shintcl  31358  chintcl  31360  shincl  31409  chincl  31527  h1datomi  31609  chscllem2  31666  sumspansn  31677  spansncvi  31680  5oalem2  31683  5oalem3  31684  pjini  31727  pjjsi  31728  eigposi  31864  nmoprepnf  31895  nmfnrepnf  31908  dmadjrnb  31934  lnophmlem1  32044  lnophm  32047  nmcopex  32057  lnconi  32061  nmbdfnlb  32078  nmcfnex  32081  imaelshi  32086  rnbra  32135  leopg  32150  pjbdlni  32177  pjhmop  32178  hmopidmch  32181  pjclem4  32227  pj3si  32235  strlem1  32278  atssma  32406  atcv0eq  32407  atcv1  32408  atomli  32410  atcvatlem  32413  cdj3lem2a  32464  cdj3lem3a  32467  xppreima  32661  fmptcof2  32673  aciunf1lem  32678  funcnv4mpt  32685  1stpreimas  32720  f1od2  32738  fpwrelmapffslem  32749  xrofsup  32777  fzspl  32797  fzsplit3  32801  nnindf  32825  fprodex01  32831  fsumiunle  32835  gsumhashmul  33046  fzto1st  33105  isslmd  33190  slmdlema  33191  elrgspnlem2  33232  elrgspnlem4  33234  qusker  33356  0nellinds  33377  unitprodclb  33396  nsgmgclem  33418  nsgmgc  33419  nsgqusf1olem2  33421  elrspunidl  33435  prmidlval  33444  prmidlc  33455  opprlidlabs  33492  dfufd2lem  33556  lindsunlem  33651  brfldext  33674  brfinext  33680  finexttrb  33689  extdg1id  33690  constrconj  33749  constrfin  33750  smatrcl  33756  submateq  33769  lmatfval  33774  lmatcl  33776  qtophaus  33796  locfinreflem  33800  locfinref  33801  zartopn  33835  zarcmplem  33841  rhmpreimacnlem  33844  xpinpreima  33866  xpinpreima2  33867  cnre2csqlem  33870  tpr2rico  33872  prsdm  33874  prsrn  33875  ordtrest2NEWlem  33882  ordtrest2NEW  33883  zrhcntr  33941  qqhval2  33944  isrrext  33962  ismntoplly  33987  indfval  33996  indf1ofs  34006  esumcvg  34066  sigaval  34091  issiga  34092  0elsiga  34094  sigaclcu  34097  issgon  34103  prsiga  34111  sigaclci  34112  difelsiga  34113  unelsiga  34114  ispisys2  34133  inelpisys  34134  unelldsys  34138  sigapildsyslem  34141  sigapildsys  34142  ldgenpisyslem1  34143  ldgenpisys  34146  isros  34148  unelros  34151  difelros  34152  fiunelros  34154  inelsros  34158  diffiunisros  34159  rossros  34160  measvuni  34194  measiun  34198  voliune  34209  volfiniune  34210  brfae  34228  ismbfm  34231  mbfmcnvima  34236  mbfmcst  34240  1stmbfm  34241  2ndmbfm  34242  imambfm  34243  sitgval  34313  issibf  34314  sibfima  34319  sitgfval  34322  sitgclg  34323  eulerpartlemelr  34338  eulerpartlemsf  34340  eulerpartleme  34344  eulerpartlemt0  34350  eulerpartlemt  34352  eulerpartgbij  34353  eulerpartlemr  34355  eulerpartlemmf  34356  eulerpartlemgvv  34357  eulerpartlemgs2  34361  eulerpartlemn  34362  eulerpart  34363  cndprobprob  34419  rrvsum  34435  orvcelel  34450  ballotlemodife  34478  ballotlemsdom  34492  ballotlemrv  34500  ballotlemrv1  34501  ballotlemrv2  34502  ballotlem1ri  34515  fsum2dsub  34600  reprinfz1  34615  reprpmtf1o  34619  reprdifc  34620  breprexplema  34623  hgt750lema  34650  hgt750leme  34651  bnj149  34867  bnj222  34875  bnj1112  34975  bnj1148  34988  fineqvrep  35087  gblacfnacd  35091  loop1cycl  35121  subfacp1lem3  35166  subfacp1lem6  35169  erdszelem10  35184  kur14  35200  cvxsconn  35227  cnllysconn  35229  resconn  35230  iscvm  35243  cvmliftlem5  35273  cvmliftlem15  35282  cvmlift2lem1  35286  cvmlift2lem12  35298  cvmlift2lem13  35299  sat1el2xp  35363  fmlasuc  35370  gonan0  35376  gonar  35379  satefvfmla0  35402  msubrn  35513  msubco  35515  ismfs  35533  mvtinf  35539  mclsax  35553  mppspstlem  35555  elmpps  35557  nnuni  35706  dfdm5  35753  dfrn5  35754  elima4  35756  rdgprc0  35774  pprodss4v  35865  elfuns  35896  fnimage  35910  imageval  35911  fwddifval  36143  fwddifnval  36144  fwddifnp1  36146  elhf2g  36157  hfun  36159  hfninf  36167  filnetlem4  36363  onsucconn  36420  onsucsuccmp  36426  limsucncmp  36428  onint1  36431  fveleq  36433  findreccl  36435  nndivsub  36439  weiunse  36450  bj-seex  36904  bj-adjg1  37025  bj-mooreset  37084  bj-ismoored0  37088  bj-ismoored  37089  bj-inftyexpitaudisj  37187  bj-inftyexpidisj  37192  bj-isvec  37269  bj-isclm  37273  csbmpo123  37313  topdifinffinlem  37329  topdifinffin  37330  csbfinxpg  37370  phpreu  37590  finixpnum  37591  lindsenlbs  37601  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem28  37634  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  poimir  37639  mblfinlem3  37645  ex-ovoliunnfl  37649  voliunnfl  37650  volsupnfl  37651  mbfresfi  37652  itgabsnc  37675  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  dvasin  37690  sdclem2  37728  fdc  37731  incsequz  37734  neificl  37739  mettrifi  37743  cntotbnd  37782  cnpwstotbnd  37783  ismtyima  37789  ismtyhmeolem  37790  heiborlem2  37798  heiborlem3  37799  heiborlem4  37800  heiborlem5  37801  heiborlem6  37802  heiborlem10  37806  isrngo  37883  isdivrngo  37936  drngoi  37937  idlval  37999  isidlc  38001  idladdcl  38005  idllmulcl  38006  idlrmulcl  38007  0idl  38011  pridlval  38019  smprngopr  38038  prnc  38053  ispridlc  38056  pridlc  38057  eqrelf  38236  ecex2  38309  imaexALTV  38311  iss2  38325  elcoeleqvrels  38576  elfunsALTV  38673  eldisjs  38703  eleldisjs  38709  fsumshftd  38933  riotaclbgBAD  38935  renegclALT  38944  lshpinN  38970  isopos  39161  oposlem  39163  glbconN  39358  glbconNOLD  39359  lnnat  39409  2at0mat0  39507  islvol2aN  39574  dalawlem13  39865  pclfinclN  39932  lhpoc2N  39997  ltrncnvatb  40120  cdleme11h  40248  cdlemefr32sn2aw  40386  cdlemefs32sn1aw  40396  cdleme32fvaw  40421  cdlemg1fvawlemN  40555  dicelvalN  41160  dih1dimatlem  41311  dihlatat  41319  dihjatcclem4  41403  islpolN  41465  lpolsatN  41470  lpolpolsatN  41471  mapdordlem1a  41616  mapdordlem1  41618  mapdhcl  41709  iscsrg  41950  fzsplitnd  41963  lcmineqlem12  42021  intlewftc  42042  dvrelogpow2b  42049  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  dvle2  42053  aks4d1p8  42068  aks4d1p9  42069  isprimroot  42074  primrootsunit1  42078  primrootscoprmpow  42080  aks6d1c1p1  42088  aks6d1c1p2  42090  aks6d1c1p3  42091  evl1gprodd  42098  hashscontpow  42103  aks6d1c3  42104  aks6d1c2  42111  sticksstones1  42127  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  aks6d1c6lem1  42151  unitscyglem5  42180  metakunt26  42211  metakunt29  42214  metakunt30  42215  metakunt32  42217  retire  42332  reelznn0nn  42455  fsuppind  42576  fsuppssindlem2  42578  fsuppssind  42579  isnacs3  42697  nacsfix  42699  mzpclval  42712  mzpcl1  42716  mzpcl2  42717  mzpcl34  42718  mzpexpmpt  42732  mzpsubst  42735  diophin  42759  diophun  42760  2rexfrabdioph  42783  3rexfrabdioph  42784  4rexfrabdioph  42785  6rexfrabdioph  42786  7rexfrabdioph  42787  rabdiophlem2  42789  diophren  42800  fphpd  42803  fphpdo  42804  fiphp3d  42806  pellexlem1  42816  pell14qrexpclnn0  42853  pellqrex  42866  rmspecnonsq  42894  monotuz  42929  monotoddzzfi  42930  monotoddzz  42931  oddcomabszz  42932  modabsdifz  42974  rmxdioph  43004  expdiophlem2  43010  limsuc2  43029  dfac11  43050  kelac1  43051  dfac21  43054  lsmfgcl  43062  islnm  43065  lnmlssfg  43068  lmhmfgima  43072  pwslnm  43082  unxpwdom3  43083  pwfi2f1o  43084  islnr  43099  hbtlem2  43112  cnsrexpcl  43153  flcidc  43158  mendlmod  43177  proot1ex  43184  oaordnr  43285  omnord1  43294  oenord1  43305  cantnfresb  43313  onmcl  43320  tfsnfin  43341  nadd2rabtr  43373  nadd1rabtr  43377  nadd1rabex  43379  nadd1suc  43381  pwelg  43549  fipjust  43554  elnonrel  43574  elinlem  43587  elcnvlem  43590  ss2iundf  43648  dfhe3  43764  dffrege115  43967  rfovcnvf1od  43993  ntrneiel2  44075  clsneiel2  44098  neicvgel2  44109  grur1cld  44227  dvgrat  44307  cvgdvgrat  44308  radcnvrat  44309  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  modelaxreplem1  44942  modelaxreplem2  44943  modelaxrep  44945  fnchoice  44966  fiiuncl  45004  disjf1  45125  disjinfi  45134  choicefi  45142  axccdom  45164  fmptf  45182  fmptff  45214  monoords  45247  supminfrnmpt  45394  supxrleubrnmptf  45400  supminfxr  45413  supminfxr2  45418  supminfxrrnmpt  45420  monoordxrv  45431  monoordxr  45432  monoord2xrv  45433  monoord2xr  45434  caucvgbf  45439  cvgcaule  45441  fsummulc1f  45526  fsumnncl  45527  fsumf1of  45529  fsumreclf  45531  fsumlessf  45532  fsumsermpt  45534  fmul01  45535  fmulcl  45536  fmuldfeqlem1  45537  fmuldfeq  45538  fmul01lt1lem1  45539  fmul01lt1lem2  45540  fprodexp  45549  fprodabs2  45550  mccllem  45552  mccl  45553  fprodcnlem  45554  fprodcn  45555  climmulf  45559  climsuse  45563  climrecf  45564  climaddf  45570  climf  45577  sumnnodd  45585  clim2f  45591  0ellimcdiv  45604  climsubmpt  45615  climreclf  45619  climf2  45621  fnlimcnv  45622  climeldmeqmpt  45623  clim2f2  45625  climfveqmpt  45626  fnlimfvre  45629  fnlimabslt  45634  climfveqmpt3  45637  climbddf  45642  climeldmeqmpt3  45644  climinf2mpt  45669  climinfmpt  45670  limsupequzmptf  45686  lmbr3  45702  liminfreuzlem  45757  coseq0  45819  cncfshift  45829  cncfperiod  45834  fprodcncf  45855  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvmptmulf  45892  dvnmptdivc  45893  dvnmul  45898  dvmptfprod  45900  iblspltprt  45928  itgspltprt  45934  stoweidlem2  45957  stoweidlem3  45958  stoweidlem4  45959  stoweidlem6  45961  stoweidlem8  45963  stoweidlem17  45972  stoweidlem19  45974  stoweidlem20  45975  stoweidlem21  45976  stoweidlem23  45978  stoweidlem27  45982  stoweidlem35  45990  stoweidlem42  45997  stoweidlem43  45998  stoweidlem62  46017  stoweid  46018  wallispilem3  46022  wallispi  46025  fourierdlem16  46078  fourierdlem21  46083  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem51  46112  fourierdlem54  46115  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem71  46132  fourierdlem72  46133  fourierdlem73  46134  fourierdlem83  46144  fourierdlem86  46147  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem96  46157  fourierdlem97  46158  fourierdlem98  46159  fourierdlem99  46160  fourierdlem100  46161  fourierdlem103  46164  fourierdlem104  46165  fourierdlem105  46166  fourierdlem108  46169  fourierdlem109  46170  fourierdlem110  46171  fourierdlem112  46173  fourierdlem113  46174  etransclem24  46213  salunicl  46271  saluncl  46272  saldifcl  46274  sge0f1o  46337  sge0lempt  46365  sge0iunmptlemfi  46368  sge0p1  46369  sge0fodjrnlem  46371  sge0iunmpt  46373  sge0ltfirpmpt2  46381  sge0isummpt2  46387  sge0xaddlem2  46389  sge0xadd  46390  ismea  46406  nnfoctbdjlem  46410  nnfoctbdj  46411  meadjiun  46421  voliunsge0lem  46427  meaiuninclem  46435  meaiuninc3v  46439  hoidmvlelem2  46551  hoidmvlelem3  46552  vonvolmbl2  46618  hoimbl2  46620  vonhoire  46627  vonicclem2  46639  vonn0ioo2  46645  vonn0icc2  46647  salpreimagelt  46662  salpreimalegt  46664  salpreimagtge  46680  salpreimaltle  46681  issmf  46683  salpreimagtlt  46685  smfpreimalt  46686  smfpreimaltf  46691  issmfle  46700  smfpreimale  46709  issmfgt  46711  smfpreimagt  46717  issmfgelem  46724  issmfge  46725  smflimlem4  46729  smflim  46732  smfpreimage  46737  smfresal  46743  smfpimbor1lem1  46753  smfpimbor1lem2  46754  smflim2  46761  smflimmpt  46765  smflimsuplem1  46775  smflimsuplem2  46776  smflimsuplem3  46777  smflimsuplem5  46779  smflimsuplem7  46781  smflimsup  46783  smfliminf  46786  eu2ndop1stv  47074  dmfcoafv  47124  ffnaov  47148  faovcl  47149  funressndmafv2rn  47172  dfatdmfcoafv2  47203  smonoord  47295  iccpartiltu  47346  iccpartigtl  47347  sprsymrelf1lem  47415  prproropf1olem2  47428  fmtno4prmfac193  47497  proththdlem  47537  proththd  47538  iseven  47552  isodd  47553  dfodd2  47560  evenm1odd  47563  evenp1odd  47564  enege  47569  onego  47570  epee  47629  perfectALTV  47647  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  bgoldbtbnd  47733  clnbupgrel  47758  edgusgrclnbfin  47765  isuspgrim0  47809  uspgrimprop  47810  isuspgrimlem  47811  grimuhgr  47815  grimedg  47840  grtriproplem  47843  grtrif1o  47846  isgrtri  47847  grtriclwlk3  47849  grimgrtri  47851  usgrgrtrirex  47852  isubgr3stgrlem7  47874  grlimgrtri  47898  usgrexmpl1tri  47919  gpgvtxel2  47941  gpgvtx0  47943  gpgvtx1  47944  gpgedgvtx0  47953  gpgedgvtx1  47954  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  uzlidlring  48078  cbvmpox2  48180  lmod1  48337  nnolog2flm1  48439  dignn0flhalflem1  48464  catprsc  48801  isthincd2lem2  48835