Theorem eleq1d 2865

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1520  ∃wex 1759   ∈ wcel 2079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-cleq 2786  df-clel 2861

This theorem is referenced by:  eleq1  2868  eleq12d  2875  eqeltrd  2881  eqneltrd  2900  rspcimdv  3555  reuind  3673  sbcel2  4281  sbccsb2  4295  disjiun  4944  breq1  4959  breq2  4960  inex1g  5108  intex  5124  pwexg  5163  reusv2lem4  5186  reusv2  5188  reusv3  5190  rabxfrd  5202  snex  5216  prex  5217  opelopabsb  5299  csbmpt12  5324  pofun  5371  seex  5398  seinxp  5513  opabid2  5578  opeliunxp2  5587  elrn2g  5639  opeldmd  5653  opeldm  5654  elreldm  5679  elrn2  5695  elsnres  5765  iss  5776  elimasng  5823  unielrel  5992  funopg  6251  funimaexg  6302  brprcneu  6522  tz6.12f  6554  ndmfvrcl  6561  ssimaex  6607  dmfco  6616  fvmpti  6625  fvmpt3  6630  fvmptf  6646  fvmptss2  6650  respreima  6692  fvn0ssdmfun  6698  fvelrn  6700  ffnfvf  6737  ffvresb  6742  fmptco  6745  fmptcof  6746  fsn  6751  fsn2g  6754  fressnfv  6776  fvrnressn  6777  fvn0fvelrn  6779  fnex  6837  funfvima  6849  funfvima3  6854  f1mpt  6875  fliftfuns  6921  isoselem  6948  isowe2  6957  riotaclb  7006  ovrspc2v  7033  ffnov  7125  fovcl  7126  ovmpos  7145  ov2gf  7146  ovg  7160  funimassov  7172  oprssdm  7176  ndmovrcl  7181  caovclg  7187  elovmpo  7240  ofmpteq  7277  sorpsscmpl  7309  uniex  7314  uniexg  7316  unexb  7319  abnexg  7326  difsnexi  7331  onint  7357  limsuc  7411  tfisi  7420  xpexr  7470  xpexcnv  7472  fnexALT  7499  fornex  7504  f1stres  7560  f2ndres  7561  xp1st  7568  xp2nd  7569  unielxp  7574  opiota  7604  fmpox  7612  offval22  7630  frxp  7664  fnse  7671  opeliunxp2f  7718  dftpos4  7753  fvmpocurryd  7779  undefnel2  7785  onnseq  7824  smoel  7840  smo11  7844  tfrlem8  7863  tfrlem9  7864  tfrlem15  7871  tfr2b  7875  tz7.44-2  7886  tz7.44-3  7887  oacl  8002  omcl  8003  oecl  8004  oaord1  8018  omordi  8033  oen0  8053  oeeui  8069  nnacl  8078  nnmcl  8079  nnecl  8080  nnmordi  8098  nnaordex  8105  omsmolem  8121  erexb  8155  qliftfuns  8225  ixpsnval  8303  elixp2  8304  resixp  8335  undifixp  8336  mptelixpg  8337  resixpfo  8338  elixpsn  8339  fundmen  8421  fopwdom  8462  disjen  8511  xpf1o  8516  unblem2  8607  xpfi  8625  fiint  8631  fnfi  8632  iunfi  8648  pwfi  8655  isfsupp  8673  fsuppun  8688  frnfsuppbi  8698  elfi2  8714  wdom2d  8880  ixpiunwdom  8891  dfom3  8945  cantnfvalf  8963  cantnflt  8970  cantnflem1  8987  r1fin  9037  tz9.12lem3  9053  ranksnb  9091  ranklim  9108  r1pw  9109  r1pwALT  9110  r1pwcl  9111  rankuni2b  9117  djuexb  9173  cardmin2  9262  infxpenc2lem1  9280  dfac8alem  9290  dfac8clem  9293  ac5num  9297  acni2  9307  acnlem  9309  alephon  9330  alephfplem3  9367  alephfplem4  9368  dfac4  9383  dfac5lem1  9384  dfac5lem5  9388  dfac2a  9390  dfac2b  9391  dfacacn  9402  dfac12lem2  9405  dfac12r  9407  dfac12k  9408  cofsmo  9526  cfsmolem  9527  isfin1a  9549  fin1ai  9550  isfin3  9553  infpssrlem3  9562  fin23lem7  9573  fin23lem11  9574  enfin2i  9578  isf34lem4  9634  fin1a2lem7  9663  hsmexlem9  9682  hsmexlem4  9686  hsmex  9689  axcc2lem  9693  axcc3  9695  axdc3lem2  9708  axcclem  9714  zornn0g  9762  ttukeylem3  9768  ttukeylem6  9771  ttukey2g  9773  brdom7disj  9788  brdom6disj  9789  fnct  9794  konigthlem  9825  axregndlem2  9860  axinfnd  9863  axacndlem5  9868  axacnd  9869  fpwwe2lem5  9891  fpwwe2lem13  9899  fpwwe  9903  pwfseqlem1  9915  pwfseqlem3  9917  pwfseqlem4a  9918  pwfseqlem4  9919  wununi  9963  wunpw  9964  wunpr  9966  wunr1om  9976  tskpw  10010  tskr1om  10024  inar1  10032  grupw  10052  grupr  10054  gruurn  10055  gruiun  10056  ingru  10072  grur1a  10076  grothomex  10086  grothac  10087  addnidpi  10158  indpi  10164  adderpq  10213  mulerpq  10214  addclprlem2  10274  mulclprlem  10276  distrlem4pr  10283  prlem934  10290  ltexprlem3  10295  ltexprlem4  10296  ltexprlem7  10299  ltexpri  10300  prlem936  10304  reclem2pr  10305  reclem3pr  10306  addclsr  10340  mulclsr  10341  supsrlem  10368  supsr  10369  axaddf  10402  axmulf  10403  axaddrcl  10409  axmulrcl  10411  renegcl  10786  negreb  10788  negn0  10906  negf1o  10907  ltord1  11003  leord1  11004  eqord1  11005  ltord2  11006  leord2  11007  eqord2  11008  negfi  11426  fiminreOLD  11427  infm3  11437  cju  11471  peano5nni  11478  peano2nn  11487  dfnn2  11488  nn1m1nn  11495  nnaddcl  11497  nnmulcl  11498  nnsub  11518  nndivtr  11521  un0addcl  11767  un0mulcl  11768  elnnnn0  11777  nn0sub  11784  frnnn0fsupp  11791  elz  11820  nnnegz  11821  elz2  11836  znegclb  11857  zaddcl  11860  nzadd  11868  zmulcl  11869  zneo  11903  nneo  11904  zeo  11906  peano5uzi  11909  zindd  11921  eluzsub  12112  uzp1  12117  uzaddcl  12142  ublbneg  12171  eqreznegel  12172  supminf  12173  zsupss  12175  qmulz  12189  qnegcl  12204  irradd  12211  irrmul  12212  xnn0xaddcl  12467  fzrev2  12810  injresinjlem  12995  negmod0  13084  om2uzuzi  13155  uzindi  13188  fsuppmapnn0ub  13201  mptnn0fsuppr  13205  seqexw  13223  seqcl2  13226  seqcl  13228  seqf  13229  monoord  13238  monoord2  13239  sermono  13240  seqsplit  13241  seqcaopr2  13244  seqid3  13252  seqhomo  13255  expcllem  13278  expcl2lem  13279  m1expcl2  13289  faccl  13481  facdiv  13485  facndiv  13486  bccmpl  13507  bccl  13520  focdmex  13549  hashclb  13557  hasheq0  13562  hashfn  13572  seqcoll  13658  opfi1uzind  13693  ccatalpha  13779  reuccatpfxs1lem  13932  reuccatpfxs1  13933  repswccat  13972  repswrevw  13973  2cshw  13999  2cshwcshw  14011  cshimadifsn  14015  cshco  14022  swrd2lsw  14138  wwlktovf  14142  wwlktovf1  14143  wwlktovfo  14144  wrd2f1tovbij  14146  shftlem  14249  shftf  14260  cjval  14283  cjth  14284  remim  14298  cnpart  14421  uzin2  14526  caubnd2  14539  sqreulem  14541  clim  14673  clim2  14683  lo1o12  14712  climrlim2  14726  lo1resb  14743  o1resb  14745  lo1eq  14747  climmpt2  14752  climshftlem  14753  rlimcld2  14757  climcn1  14770  climcn2  14771  o1dif  14808  iserex  14835  climub  14840  climserle  14841  isercoll  14846  climcau  14849  caurcvg2  14856  caucvgb  14858  summolem3  14892  summolem2a  14893  zsum  14896  fsum  14898  sumss2  14904  fsumcvg2  14905  fsumsplitf  14919  sumpr  14924  sumtp  14925  fsumm1  14927  fsum1p  14929  isummulc2  14938  fsum2dlem  14946  fsumcom2  14950  fsumshftm  14957  fsum0diag2  14959  fsumge1  14973  fsum00  14974  fsumabs  14977  telfsumo  14978  telfsumo2  14979  fsumparts  14982  fsumrlim  14987  fsumo1  14988  o1fsum  14989  fsumiun  14997  binomlem  15005  isumshft  15015  isum1p  15017  isumrpcl  15019  climcndslem1  15025  climcndslem2  15026  climcnds  15027  infcvgaux2i  15034  cvgrat  15060  mertens  15063  clim2prod  15065  prodfn0  15071  prodfrec  15072  prodfdiv  15073  ntrivcvgfvn0  15076  prodmolem3  15108  prodmolem2a  15109  zprod  15112  fprod  15116  prodss  15122  fprodser  15124  fprodm1  15142  fprod1p  15143  fprodm1s  15145  fprodp1s  15146  fprodabs  15149  fprodn0  15154  fprod2dlem  15155  fprodcnv  15158  fprodcom2  15159  fproddivf  15162  fprodsplitf  15163  fprodsplit1f  15165  bpolycl  15227  fprodefsum  15269  rpnnen2lem11  15398  mod2eq1n2dvds  15517  mulsucdiv2z  15523  zob  15529  nn0o1gt2  15553  nno  15554  nn0o  15555  divalglem7  15571  bitsf1  15616  sadcp1  15625  smupp1  15650  qnumdencl  15896  iserodd  15989  pcqcl  16010  pcxcl  16014  pcgcd1  16030  dvdsprmpweqle  16039  pcmpt  16045  pcmpt2  16046  pcmptdvds  16047  infpnlem2  16064  infpn2  16066  1arith  16080  elgz  16084  mul4sq  16107  4sqlem13  16110  4sqlem17  16114  4sqlem18  16115  4sqlem19  16116  vdwlem1  16134  vdwlem2  16135  vdwnn  16151  ramtcl2  16164  ramcl  16182  prmonn2  16192  prmodvdslcmf  16200  isstruct2  16310  wunress  16381  firest  16523  imasaddfnlem  16618  imasvscafn  16627  xpsfrnel2  16654  mreintcl  16683  ismred2  16691  mreexexlemd  16732  mreexexlem3d  16734  mreexexlem4d  16735  iscatd2  16769  catpropd  16796  subsubc  16940  isfunc  16951  fncnvimaeqv  17187  joindef  17431  joinval  17432  meetdef  17445  meetval  17446  oduclatb  17571  acsdrsel  17594  isacs4lem  17595  isacs5lem  17596  acsdrscl  17597  mgm1  17684  gsumvalx  17697  mndpropd  17743  issubm  17774  mhmima  17790  gsumwsubmcl  17802  gsumwspan  17810  mulgsubcl  17985  issubg  18021  issubg2  18036  issubg4  18040  grpissubg  18041  0subg  18046  cycsubgcl  18047  isnsg  18050  isnsg2  18051  nsgbi  18052  isnsg3  18055  elnmz  18060  nmzbi  18061  nmzsubg  18062  eqgval  18070  eqgid  18073  ghmrn  18100  ghmnsgima  18111  gass  18160  oppgsubg  18220  f1omvdconj  18293  symgfisg  18315  psgneldm  18350  odhash3  18419  sylow2blem2  18464  lsmsubm  18496  lsmsubg  18497  efgsf  18570  efgsdm  18571  efgs1b  18577  efgredlema  18581  eqgabl  18668  ablnsg  18678  cyggenod2  18715  gsumzaddlem  18749  gsummhm2  18767  gsum2dlem2  18799  gsum2d2lem  18801  gsumcom2  18803  dprdfeq0  18849  dprdsubg  18851  dprd2da  18869  ablfacrp  18893  pgpfac1lem3  18904  pgpfaclem1  18908  ablfaclem3  18914  ablfac2  18916  issrg  18935  srgfcl  18943  srgbinomlem4  18971  isring  18979  iscrng  18982  dvdsr  19074  irredrmul  19135  isrim0  19153  isdrngd  19205  issubrg  19213  issubrg2  19233  subrgpropd  19248  issdrg  19252  sdrgacs  19258  issrngd  19310  islmod  19316  lmodlema  19317  islmodd  19318  lmodprop2d  19374  rmodislmodlem  19379  rmodislmod  19380  lssset  19383  islssd  19385  lsscl  19392  lsslss  19411  lsspropd  19467  lmhmima  19497  lbsind  19530  lsmcl  19533  islvec  19554  lspsolvlem  19592  lspsolv  19593  lvecpropd  19617  isassa  19765  assapropd  19777  psrbag  19820  psrbaglefi  19828  psrbagconf1o  19830  mplsubglem  19890  mpllsslem  19891  ltbwe  19928  psrbagsn  19950  subrgasclcl  19954  mplind  19957  mpfind  19991  coe1mul2lem2  20107  gsumply1eq  20144  evl1vsd  20177  mpfpf1  20184  pf1mpf  20185  pf1ind  20188  xrsdsreclblem  20261  xrsdsreclb  20262  prmirred  20312  znunithash  20381  cofipsgn  20407  zrhpsgnelbas  20408  rzgrp  20437  isphl  20442  phllmhm  20446  ipcl  20447  isphld  20468  phlpropd  20469  phlssphl  20473  cssincl  20502  pjdm  20521  dsmmval  20548  dsmmbas2  20551  dsmmelbas  20553  frlmbas  20569  frlmup1  20612  lindfind  20630  lindsind  20631  f1lindf  20636  islindf4  20652  matecl  20706  m1detdiag  20878  mdetralt  20889  mdetralt2  20890  mdetunilem2  20894  mdetunilem9  20901  m2detleiblem3  20910  m2detleiblem4  20911  smadiadetlem0  20942  cpmatacl  20996  chpscmat  21122  uniopn  21177  inopn  21179  fiinopn  21181  istps  21214  fctop  21284  iscld  21307  isopn2  21312  mretopd  21372  iscldtop  21375  perfi  21435  tgrest  21439  restcld  21452  ordtbaslem  21468  ordtrest2lem  21483  ordtrest2  21484  iscn  21515  cnpval  21516  iscnp  21517  tgcn  21532  subbascn  21534  ssidcn  21535  lmbrf  21540  cnpnei  21544  cnima  21545  iscncl  21549  cnconst2  21563  cnrest2  21566  cnpresti  21568  cnprest  21569  cnindis  21572  lmres  21580  lmcnp  21584  iscnrm  21603  t1sncld  21606  cnrmi  21640  cncmp  21672  cmpsublem  21679  fiuncmp  21684  unconn  21709  conncompid  21711  conncompconn  21712  conncompss  21713  1stcfb  21725  2ndcrest  21734  2ndcctbss  21735  2ndcdisj  21736  1stccnp  21742  islly  21748  isnlly  21749  subislly  21761  restnlly  21762  restlly  21763  islly2  21764  hausllycmp  21774  cldllycmp  21775  dislly  21777  isptfin  21796  islocfin  21797  ptfinfin  21799  finlocfin  21800  dissnlocfin  21809  locfindis  21810  comppfsc  21812  kgenval  21815  elkgen  21816  kgeni  21817  cmpkgen  21831  1stckgenlem  21833  kgencn2  21837  ptpjpre1  21851  elpt  21852  elptr  21853  ptbasin  21857  xkobval  21866  xkoval  21867  xkoopn  21869  txbasval  21886  tx1cn  21889  tx2cn  21890  dfac14  21898  xkoccn  21899  txcnp  21900  ptcnplem  21901  txcnmpt  21904  txindislem  21913  txdis1cn  21915  txlly  21916  txnlly  21917  pthaus  21918  ptrescn  21919  hauseqlcld  21926  txlm  21928  tx2ndc  21931  txkgen  21932  xkoptsub  21934  xkopt  21935  xkoco1cn  21937  xkoco2cn  21938  xkococnlem  21939  xkococn  21940  cnmpt11  21943  cnmpt12  21947  cnmpt21  21951  cnmpt22  21954  cnmptkp  21960  cnmptk1p  21965  xkoinjcn  21967  txconn  21969  qtopval2  21976  elqtop  21977  idqtop  21986  qtopcld  21993  qtopeu  21996  qtoprest  21997  qtopomap  21998  qtopcmap  21999  ishmeo  22039  hmeoopn  22046  hmeocld  22047  ordthmeolem  22081  ptcmpfi  22093  elmptrab  22107  fgcl  22158  trfil2  22167  cfinfil  22173  uzrest  22177  ufilss  22185  trufil  22190  cfinufil  22208  ufinffr  22209  ufildr  22211  rnelfm  22233  flfcntr  22323  ptcmplem2  22333  ptcmplem3  22334  ptcmplem4  22335  ptcmplem5  22336  cnextfvval  22345  tmdcn2  22369  tmdmulg  22372  tmdgsum2  22376  symgtgp  22381  opnsubg  22387  clssubg  22388  tgpconncompeqg  22391  ghmcnp  22394  tgphaus  22396  tgpt0  22398  qustgpopn  22399  qustgplem  22400  tsmsgsum  22418  tsmssubm  22422  tsmsres  22423  tsmsf1o  22424  tsmsxplem1  22432  tsmsxplem2  22433  tsmsxp  22434  istrg  22443  istdrg  22445  istdrg2  22457  istlm  22464  istvc  22471  ustval  22482  ustincl  22487  ustdiag  22488  ustinvel  22489  ustexhalf  22490  ust0  22499  ucnima  22561  fmucndlem  22571  prdsdsf  22648  prdsxmet  22650  imasf1oxmet  22656  imasf1omet  22657  prdsxmslem2  22810  metustsym  22836  isnlm  22955  qtopbaslem  23038  xrtgioo  23085  reperflem  23097  fsumcn  23149  expcn  23151  xrhmeo  23221  cnllycmp  23231  bndth  23233  isclm  23339  lmhmclm  23362  lmmcvg  23535  fmcfil  23546  iscfil3  23547  iscau2  23551  iscau4  23553  iscmet3lem1  23565  iscmet3  23567  cfilres  23570  caussi  23571  equivcfil  23573  flimcfil  23588  bcthlem1  23598  isbn  23612  srabn  23634  ishl2  23644  cmslssbn  23646  cmscsscms  23647  minveclem3b  23702  ivthlem1  23723  ivthlem2  23724  ivthlem3  23725  ivth2  23727  ivthle  23728  ivthle2  23729  ivthicc  23730  ovolficcss  23741  ovolunlem1a  23768  ovolunlem1  23769  ovolfiniun  23773  ovoliunlem1  23774  ovoliunlem3  23776  ovoliun  23777  ovoliun2  23778  shft2rab  23780  ovolshftlem1  23781  sca2rab  23784  ovolscalem1  23785  mblsplit  23804  finiunmbl  23816  volun  23817  volfiniun  23819  voliunlem1  23822  voliunlem3  23824  iunmbl  23825  voliun  23826  volsup  23828  ioombl  23837  ioorcl  23849  vitalilem1  23880  vitalilem2  23881  vitalilem3  23882  vitalilem4  23883  vitali  23885  ismbf1  23896  mbfdm  23898  ismbf  23900  ismbfcn  23901  mbfima  23902  mbfimaicc  23903  ismbfcn2  23910  ismbfd  23911  ismbf2d  23912  mbfeqalem1  23913  mbfmax  23921  mbfposr  23924  mbfposb  23925  ismbf3d  23926  mbfimaopnlem  23927  mbfimaopn2  23929  cncombf  23930  isi1f  23946  i1fd  23953  itg1mulc  23976  mbfi1fseqlem4  23990  itg2lcl  23999  isibl  24037  iblitg  24040  iblcnlem1  24059  iblcnlem  24060  iblrelem  24062  iblpos  24064  itgeqa  24085  itgfsum  24098  itgabs  24106  limcvallem  24140  ellimc  24142  ellimc2  24146  limcmpt  24152  cnmptlimc  24159  dvbsss  24171  cpnfval  24200  elcpn  24202  dvmptfsum  24243  dvle  24275  dvfsumle  24289  dvfsumge  24290  dvfsumabs  24291  dvfsumrlimf  24293  dvfsumlem1  24294  dvfsumlem2  24295  dvfsumlem3  24296  dvfsumlem4  24297  dvfsumrlimge0  24298  dvfsumrlim  24299  dvfsumrlim2  24300  dvfsum2  24302  itgsubstlem  24316  itgsubst  24317  mdegcl  24334  deg1nn0clb  24355  isuc1p  24405  plyeq0lem  24471  plyco  24502  plycj  24538  dvnply2  24547  plydivlem4  24556  fta1lem  24567  fta1  24568  elqaalem1  24579  elqaalem2  24580  elqaalem3  24581  elqaa  24582  ulmcau  24654  radcnv0  24675  radcnvlt1  24677  radcnvle  24679  pserdvlem2  24687  coseq1  24781  efeq1  24782  sinord  24787  efif1olem2  24796  efif1olem4  24798  lognegb  24842  logcj  24858  argimgt0  24864  logtayl  24912  2irrexpq  24982  root1eq1  25005  logrec  25010  2irrexpqALT  25047  angrteqvd  25053  angpieqvdlem  25075  atans  25177  atans2  25178  leibpilem1OLD  25188  dmarea  25205  areambl  25206  rlimcnp  25213  rlimcnp2  25214  xrlimcnp  25216  harmonicbnd  25251  harmonicbnd2  25252  lgamcvglem  25287  wilthlem2  25316  wilth  25318  efnnfsumcl  25350  vmacl  25365  efvmacl  25367  efchtdvds  25406  sqff1o  25429  fsumdvdscom  25432  musumsum  25439  fsumdvdsmul  25442  fsumvma  25459  perfect  25477  dchrelbasd  25485  lgsval  25547  lgsval2lem  25553  lgsdir2lem4  25574  lgsdir2  25576  lgsqrlem1  25592  lgsdchr  25601  m1lgs  25634  2lgs  25653  mul2sq  25665  2sqlem6  25669  2sqblem  25677  2sq2  25679  rplogsumlem2  25731  dchrisumlema  25734  dchrisumlem2  25736  dchrisumlem3  25737  dchrvmasumlem2  25744  dchrvmasumlem3  25745  dchrisum0flblem2  25755  dchrisum0flb  25756  dchrisum0fno1  25757  ostthlem1  25873  mirval  26111  perpneq  26170  isperp2  26171  isperp2d  26172  foot  26178  islnopp  26195  islnoppd  26196  outpasch  26211  hlpasch  26212  ishpg  26215  colopp  26225  colhp  26226  lmif  26241  islmib  26243  lmiinv  26248  trgcopy  26260  trgcopyeu  26262  acopyeu  26291  inaghl  26302  tgasa1  26315  f1otrgitv  26327  f1otrg  26328  isfusgr  26771  opfusgr  26776  fusgrfisbase  26781  fusgrfisstep  26782  nbupgrel  26798  nbumgrvtx  26799  nbusgreledg  26806  edgnbusgreu  26820  nb3grprlem1  26833  uvtxusgrel  26856  cusgredg  26877  cplgr2vpr  26886  cusgrexg  26897  usgredgsscusgredg  26912  fusgrn0degnn0  26952  rusgrnumwrdl2  27039  rgrx0ndm  27046  wlkcomp  27083  wlkdlem2  27138  clwlkcomp  27235  iswwlks  27289  wwlknllvtx  27299  0enwwlksnge1  27317  wlkiswwlks2lem5  27326  wwlksm1edg  27334  wwlksnred  27345  wwlksnext  27346  wwlksnextbi  27347  wwlksnredwwlkn  27348  wwlksnextfun  27351  wwlksnextinj  27352  wwlksnextsurj  27353  wwlksnextbij  27355  wwlksnfi  27359  wwlksnextproplem2  27364  wwlksnextprop  27366  2wlkdlem4  27382  rusgrnumwwlkl1  27422  rusgrnumwwlks  27428  isclwwlk  27437  clwwlk1loop  27441  clwwlkccatlem  27442  clwlkclwwlklem2a1  27445  clwlkclwwlklem2a4  27450  clwlkclwwlklem2a  27451  clwlkclwwlklem2  27453  clwlkclwwlklem3  27454  clwlkclwwlk  27455  clwlkclwwlk2  27456  clwwisshclwwslemlem  27466  clwwisshclwwslem  27467  clwwisshclwws  27468  clwwlknlbonbgr1  27492  clwwlkinwwlk  27493  clwwlkn1  27494  loopclwwlkn1b  27495  clwwlkn1loopb  27496  clwwlkn2  27497  clwwlkel  27500  clwwlkf  27501  clwwlkwwlksb  27508  clwwlkext2edg  27510  wwlksext2clwwlk  27511  wwlksubclwwlk  27512  eleclclwwlknlem2  27515  umgr2cwwk2dif  27518  s2elclwwlknon2  27558  clwwlknonwwlknonb  27560  clwwlknonex2lem2  27562  clwwlknonex2  27563  3wlkdlem4  27616  upgr3v3e3cycl  27634  upgr4cycl4dv4e  27639  eupth2lem2  27674  eulerpathpr  27695  1vwmgr  27735  3vfriswmgrlem  27736  3vfriswmgr  27737  3cyclfrgrrn1  27744  vdgn1frgrv2  27755  frgrncvvdeqlem3  27760  frgrncvvdeqlem8  27765  frgrncvvdeqlem9  27766  frgrwopregasn  27775  frgrwopregbsn  27776  frgrwopreglem5ALT  27781  frgr2wwlk1  27788  frgr2wwlkeqm  27790  fusgr2wsp2nb  27793  2clwwlk2clwwlklem  27805  extwwlkfabel  27812  nvvop  28065  isnvlem  28066  sspval  28179  nmorepnf  28224  phpar  28280  siilem2  28308  bnsscmcl  28324  ubthlem1  28326  shaddcl  28673  shmulcl  28674  hsn0elch  28704  hhssablo  28719  hhssnvt  28721  hhsssh  28725  shscl  28774  shintcl  28786  chintcl  28788  shincl  28837  chincl  28955  h1datomi  29037  chscllem2  29094  sumspansn  29105  spansncvi  29108  5oalem2  29111  5oalem3  29112  pjini  29155  pjjsi  29156  eigposi  29292  nmoprepnf  29323  nmfnrepnf  29336  dmadjrnb  29362  lnophmlem1  29472  lnophm  29475  nmcopex  29485  lnconi  29489  nmbdfnlb  29506  nmcfnex  29509  imaelshi  29514  rnbra  29563  leopg  29578  pjbdlni  29605  pjhmop  29606  hmopidmch  29609  pjclem4  29655  pj3si  29663  strlem1  29706  atssma  29834  atcv0eq  29835  atcv1  29836  atomli  29838  atcvatlem  29841  cdj3lem2a  29892  cdj3lem3a  29895  fovcld  30048  xppreima  30057  fmptcof2  30065  aciunf1lem  30070  funcnv4mpt  30077  1stpreimas  30102  f1od2  30118  fpwrelmapffslem  30129  xrofsup  30153  fzspl  30171  fzsplit3  30175  nnindf  30190  fprodex01  30196  fsumiunle  30200  isslmd  30426  slmdlema  30427  qusker  30527  0nellinds  30538  lindsunlem  30579  brfldext  30596  brfinext  30602  finexttrb  30611  extdg1id  30612  fzto1st  30623  smatrcl  30632  submateq  30645  lmatfval  30650  lmatcl  30652  qtophaus  30673  locfinreflem  30677  locfinref  30678  xpinpreima  30722  xpinpreima2  30723  cnre2csqlem  30726  tpr2rico  30728  prsdm  30730  prsrn  30731  ordtrest2NEWlem  30738  ordtrest2NEW  30739  qqhval2  30796  isrrext  30814  ismntoplly  30839  indfval  30848  indf1ofs  30858  esumcvg  30918  sigaval  30943  issiga  30944  0elsiga  30946  sigaclcu  30949  issgon  30955  prsiga  30963  sigaclci  30964  difelsiga  30965  unelsiga  30966  ispisys2  30985  unelldsys  30990  sigapildsyslem  30993  sigapildsys  30994  ldgenpisyslem1  30995  ldgenpisys  30998  isros  31000  unelros  31003  difelros  31004  fiunelros  31006  inelsros  31010  diffiunisros  31011  rossros  31012  measvuni  31046  measiun  31050  voliune  31061  volfiniune  31062  brfae  31080  ismbfm  31083  mbfmcnvima  31088  mbfmcst  31090  1stmbfm  31091  2ndmbfm  31092  imambfm  31093  sitgval  31163  issibf  31164  sibfima  31169  sitgfval  31172  sitgclg  31173  eulerpartlemelr  31188  eulerpartlemsf  31190  eulerpartleme  31194  eulerpartlemt0  31200  eulerpartlemt  31202  eulerpartgbij  31203  eulerpartlemr  31205  eulerpartlemmf  31206  eulerpartlemgvv  31207  eulerpartlemgs2  31211  eulerpartlemn  31212  eulerpart  31213  cndprobprob  31269  rrvsum  31285  orvcelel  31300  ballotlemodife  31328  ballotlemsdom  31342  ballotlemrv  31350  ballotlemrv1  31351  ballotlemrv2  31352  ballotlem1ri  31365  fsum2dsub  31451  reprinfz1  31466  reprpmtf1o  31470  reprdifc  31471  breprexplema  31474  hgt750lema  31501  hgt750leme  31502  bnj149  31719  bnj222  31727  bnj1112  31825  bnj1148  31838  loop1cycl  31948  subfacp1lem3  31993  subfacp1lem6  31996  erdszelem10  32011  kur14  32027  cvxsconn  32054  cnllysconn  32056  resconn  32057  iscvm  32070  cvmliftlem5  32100  cvmliftlem15  32109  cvmlift2lem1  32113  cvmlift2lem12  32125  cvmlift2lem13  32126  sat1el2xp  32188  fmlasuc  32195  gonan0  32200  gonar  32203  satefvfmla0  32226  msubrn  32329  msubco  32331  ismfs  32349  mvtinf  32355  mclsax  32369  mppspstlem  32371  elmpps  32373  dfdm5  32569  dfrn5  32570  elima4  32572  rdgprc0  32592  nodmon  32711  noextendseq  32728  nodense  32750  pprodss4v  32899  elfuns  32930  fnimage  32944  imageval  32945  fwddifval  33177  fwddifnval  33178  fwddifnp1  33180  elhf2g  33191  hfun  33193  hfninf  33201  filnetlem4  33283  onsucconn  33339  onsucsuccmp  33345  limsucncmp  33347  onint1  33350  fveleq  33352  findreccl  33354  nndivsub  33358  bj-seex  33758  bj-mooreset  33939  bj-ismoored0  33944  bj-ismoored  33945  bj-ismooredr2  33948  bj-elid  33973  bj-inftyexpitaudisj  33991  bj-inftyexpidisj  33996  csbmpo123  34089  topdifinffinlem  34105  topdifinffin  34106  csbfinxpg  34146  phpreu  34353  finixpnum  34354  lindsenlbs  34364  poimirlem16  34385  poimirlem17  34386  poimirlem19  34388  poimirlem20  34389  poimirlem22  34391  poimirlem23  34392  poimirlem24  34393  poimirlem25  34394  poimirlem26  34395  poimirlem28  34397  poimirlem29  34398  poimirlem30  34399  poimirlem31  34400  poimirlem32  34401  poimir  34402  mblfinlem3  34408  ex-ovoliunnfl  34412  voliunnfl  34413  volsupnfl  34414  mbfresfi  34415  itgabsnc  34438  ftc1anclem6  34449  ftc1anclem7  34450  ftc1anclem8  34451  ftc1anc  34452  dvasin  34455  sdclem2  34495  fdc  34498  incsequz  34501  neificl  34506  mettrifi  34510  cntotbnd  34552  cnpwstotbnd  34553  ismtyima  34559  ismtyhmeolem  34560  heiborlem2  34568  heiborlem3  34569  heiborlem4  34570  heiborlem5  34571  heiborlem6  34572  heiborlem10  34576  isrngo  34653  isdivrngo  34706  drngoi  34707  idlval  34769  isidlc  34771  idladdcl  34775  idllmulcl  34776  idlrmulcl  34777  0idl  34781  pridlval  34789  smprngopr  34808  prnc  34823  ispridlc  34826  pridlc  34827  eqrelf  34997  ecex2  35066  imaexALTV  35068  iss2  35083  elcoeleqvrels  35311  elfunsALTV  35406  eldisjs  35436  eleldisjs  35442  fsumshftd  35569  riotaclbgBAD  35571  renegclALT  35580  lshpinN  35606  isopos  35797  oposlem  35799  glbconN  35994  lnnat  36044  2at0mat0  36142  islvol2aN  36209  dalawlem13  36500  pclfinclN  36567  lhpoc2N  36632  ltrncnvatb  36755  cdleme11h  36883  cdlemefr32sn2aw  37021  cdlemefs32sn1aw  37031  cdleme32fvaw  37056  cdlemg1fvawlemN  37190  dicelvalN  37795  dih1dimatlem  37946  dihlatat  37954  dihjatcclem4  38038  islpolN  38100  lpolsatN  38105  lpolpolsatN  38106  mapdordlem1a  38251  mapdordlem1  38253  mapdhcl  38344  lmhmlvec  38625  isnacs3  38742  nacsfix  38744  mzpclval  38757  mzpcl1  38761  mzpcl2  38762  mzpcl34  38763  mzpexpmpt  38777  mzpsubst  38780  diophin  38805  diophun  38806  2rexfrabdioph  38829  3rexfrabdioph  38830  4rexfrabdioph  38831  6rexfrabdioph  38832  7rexfrabdioph  38833  rabdiophlem2  38835  diophren  38846  fphpd  38849  fphpdo  38850  fiphp3d  38852  pellexlem1  38862  pell14qrexpclnn0  38899  pellqrex  38912  rmspecnonsq  38940  monotuz  38974  monotoddzzfi  38975  monotoddzz  38976  oddcomabszz  38977  modabsdifz  39019  rmxdioph  39049  expdiophlem2  39055  limsuc2  39077  dfac11  39098  kelac1  39099  dfac21  39102  lsmfgcl  39110  islnm  39113  lnmlssfg  39116  lmhmfgima  39120  pwslnm  39130  unxpwdom3  39131  pwfi2f1o  39132  islnr  39147  hbtlem2  39160  cnsrexpcl  39201  flcidc  39210  mendlmod  39229  proot1ex  39237  pwelg  39355  fipjust  39360  elnonrel  39381  elinlem  39394  elcnvlem  39397  ss2iundf  39440  dfhe3  39557  dffrege115  39760  rfovcnvf1od  39786  ntrneiel2  39872  clsneiel2  39895  neicvgel2  39906  grur1cld  40017  cycsubggenodd  40092  dvgrat  40134  cvgdvgrat  40135  radcnvrat  40136  binomcxplemdvsum  40177  binomcxplemnotnn0  40178  fnchoice  40777  fiiuncl  40818  disjf1  40936  disjinfi  40947  choicefi  40956  axccdom  40980  fmptf  41003  monoords  41058  supminfrnmpt  41215  supxrleubrnmptf  41223  supminfxr  41236  supminfxr2  41241  supminfxrrnmpt  41243  monoordxrv  41254  monoordxr  41255  monoord2xrv  41256  monoord2xr  41257  fsumclf  41346  fsummulc1f  41347  fsumnncl  41348  fsumsplit1  41349  fsumf1of  41351  fsumreclf  41353  fsumlessf  41354  fsumsermpt  41356  fmul01  41357  fmulcl  41358  fmuldfeqlem1  41359  fmuldfeq  41360  fmul01lt1lem1  41361  fmul01lt1lem2  41362  fprodexp  41371  fprodabs2  41372  mccllem  41374  mccl  41375  fprodcnlem  41376  fprodcn  41377  climmulf  41381  climsuse  41385  climrecf  41386  climaddf  41392  climf  41399  sumnnodd  41407  clim2f  41413  0ellimcdiv  41426  climsubmpt  41437  climreclf  41441  climf2  41443  fnlimcnv  41444  climeldmeqmpt  41445  clim2f2  41447  climfveqmpt  41448  fnlimfvre  41451  fnlimabslt  41456  climfveqmpt3  41459  climbddf  41464  climeldmeqmpt3  41466  climinf2mpt  41491  climinfmpt  41492  limsupequzmptf  41508  lmbr3  41524  liminfreuzlem  41579  coseq0  41640  cncfshift  41652  cncfperiod  41657  fprodcncf  41679  ioodvbdlimc1lem2  41712  ioodvbdlimc2lem  41714  dvmptmulf  41717  dvnmptdivc  41718  dvnmul  41723  dvmptfprod  41725  iblspltprt  41753  itgspltprt  41759  stoweidlem2  41783  stoweidlem3  41784  stoweidlem4  41785  stoweidlem6  41787  stoweidlem8  41789  stoweidlem17  41798  stoweidlem19  41800  stoweidlem20  41801  stoweidlem21  41802  stoweidlem23  41804  stoweidlem27  41808  stoweidlem35  41816  stoweidlem42  41823  stoweidlem43  41824  stoweidlem62  41843  stoweid  41844  wallispilem3  41848  wallispi  41851  fourierdlem16  41904  fourierdlem21  41909  fourierdlem41  41929  fourierdlem42  41930  fourierdlem48  41935  fourierdlem49  41936  fourierdlem50  41937  fourierdlem51  41938  fourierdlem54  41941  fourierdlem63  41950  fourierdlem64  41951  fourierdlem65  41952  fourierdlem71  41958  fourierdlem72  41959  fourierdlem73  41960  fourierdlem83  41970  fourierdlem86  41973  fourierdlem89  41976  fourierdlem90  41977  fourierdlem91  41978  fourierdlem96  41983  fourierdlem97  41984  fourierdlem98  41985  fourierdlem99  41986  fourierdlem100  41987  fourierdlem103  41990  fourierdlem104  41991  fourierdlem105  41992  fourierdlem108  41995  fourierdlem109  41996  fourierdlem110  41997  fourierdlem112  41999  fourierdlem113  42000  etransclem24  42039  salunicl  42097  saluncl  42098  saldifcl  42100  sge0f1o  42160  sge0lempt  42188  sge0iunmptlemfi  42191  sge0p1  42192  sge0fodjrnlem  42194  sge0iunmpt  42196  sge0ltfirpmpt2  42204  sge0isummpt2  42210  sge0xaddlem2  42212  sge0xadd  42213  ismea  42229  nnfoctbdjlem  42233  nnfoctbdj  42234  meadjiun  42244  voliunsge0lem  42250  meaiuninclem  42258  meaiuninc3v  42262  hoidmvlelem2  42374  hoidmvlelem3  42375  vonvolmbl2  42441  hoimbl2  42443  vonhoire  42450  vonicclem2  42462  vonn0ioo2  42468  vonn0icc2  42470  salpreimagelt  42482  salpreimalegt  42484  salpreimagtge  42498  salpreimaltle  42499  issmf  42501  salpreimagtlt  42503  smfpreimalt  42504  smfpreimaltf  42509  issmfle  42518  smfpreimale  42527  issmfgt  42529  smfpreimagt  42534  issmfgelem  42541  issmfge  42542  smflimlem4  42546  smflim  42549  smfpreimage  42554  smfresal  42559  smfpimbor1lem1  42569  smfpimbor1lem2  42570  smflim2  42576  smflimmpt  42580  smflimsuplem1  42590  smflimsuplem2  42591  smflimsuplem3  42592  smflimsuplem5  42594  smflimsuplem7  42596  smflimsup  42598  smfliminf  42601  eu2ndop1stv  42794  dmfcoafv  42844  ffnaov  42868  faovcl  42869  funressndmafv2rn  42892  dfatdmfcoafv2  42923  smonoord  43001  iccpartiltu  43018  iccpartigtl  43019  sprsymrelf1lem  43089  prproropf1olem2  43102  fmtno4prmfac193  43171  proththdlem  43214  proththd  43215  iseven  43229  isodd  43230  dfodd2  43237  evenm1odd  43240  evenp1odd  43241  enege  43246  onego  43247  epee  43306  perfectALTV  43324  bgoldbtbndlem2  43407  bgoldbtbndlem3  43408  bgoldbtbndlem4  43409  bgoldbtbnd  43410  isomuspgrlem1  43428  isomuspgrlem2b  43430  isomuspgrlem2d  43432  mgmpropd  43478  issubmgm  43492  issubmgm2  43493  mgmhmima  43505  inclfusubc  43570  isrng  43579  isrngisom  43599  lidlmmgm  43628  uzlidlring  43632  cbvmpox2  43816  lmod1  43981  nnolog2flm1  44085  dignn0flhalflem1  44110