Theorem eleq1d 2821

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eleq1  2824  eleq12d  2830  eqeltrd  2836  eqneltrd  2856  rspcimdv  3554  reuind  3699  sbcel2  4358  sbccsb2  4377  disjiun  5073  breq1  5088  breq2  5089  axrep6g  5225  inex1g  5260  intex  5285  pwexg  5320  reusv2lem4  5343  reusv2  5345  reusv3  5347  rabxfrd  5359  prexOLD  5385  opelopabsb  5485  csbmpt12  5512  pofun  5557  seex  5590  seinxp  5715  opabid2  5784  opeliunxp2  5793  elrn2g  5845  opeldmd  5861  opeldm  5862  elreldm  5890  elsnres  5986  iss  6000  unielrel  6238  onunel  6430  funopg  6532  brprcneu  6830  brprcneuALT  6831  tz6.12f  6865  ndmfvrcl  6873  ssimaex  6925  dmfco  6936  fvmpti  6946  fvmpt3  6952  fvmptf  6969  fvmptss2  6974  respreima  7018  fvn0ssdmfun  7026  fvelrn  7028  ffnfvf  7072  ffvresb  7078  fmptco  7082  fmptcof  7083  fsn  7088  fsn2g  7091  fressnfv  7114  fvrnressn  7115  fnex  7172  funfvima  7185  funfvima3  7191  f1mpt  7216  fliftfuns  7269  isoselem  7296  isowe2  7305  riotaclb  7365  ovrspc2v  7393  ffnov  7493  fovcld  7494  ovmpos  7515  ov2gf  7516  ovg  7532  funimassov  7544  oprssdm  7548  ndmovrcl  7553  caovclg  7559  elovmpo  7612  ofmpteq  7654  sorpsscmpl  7688  uniexg  7694  unexbOLD  7702  abnexg  7710  difsnexi  7715  onint  7744  limsuc  7800  tfisi  7810  peano5  7844  xpexr  7869  xpexcnv  7871  fnexALT  7904  focdmex  7909  f1stres  7966  f2ndres  7967  xp1st  7974  xp2nd  7975  unielxp  7980  opiota  8012  fmpox  8020  offval22  8038  frxp  8076  fnse  8083  frxp2  8094  sexp2  8096  frxp3  8101  sexp3  8103  opeliunxp2f  8160  dftpos4  8195  fvmpocurryd  8221  undefnel2  8227  onnseq  8284  smoel  8300  smo11  8304  tfrlem8  8323  tfrlem9  8324  tfrlem15  8331  tfr2b  8335  tz7.44-2  8346  tz7.44-3  8347  oacl  8470  omcl  8471  oecl  8472  oaord1  8486  omordi  8501  oen0  8522  oeeui  8538  nnacl  8547  nnmcl  8548  nnecl  8549  nnmordi  8567  nnaordex  8574  omsmolem  8593  naddcllem  8612  naddov2  8615  naddf  8617  naddssim  8621  naddelim  8622  naddasslem1  8630  naddasslem2  8631  naddsuc2  8637  erexb  8669  elecex  8694  qliftfuns  8751  ixpsnval  8848  elixp2  8849  resixp  8881  undifixp  8882  mptelixpg  8883  resixpfo  8884  elixpsn  8885  fundmen  8978  fopwdom  9023  disjen  9072  xpf1o  9077  unfi  9105  cnvfi  9110  fnfi  9112  f1oenfirn  9114  f1domfi  9115  unblem2  9203  imafiOLD  9226  pwfi  9229  fiint  9237  iunfi  9253  tfsnfin2  9273  isfsupp  9278  fsuppun  9300  ffsuppbi  9311  elfi2  9327  wdom2d  9495  ixpiunwdom  9505  dfom3  9568  cantnfvalf  9586  cantnflt  9593  cantnflem1  9610  r1fin  9697  tz9.12lem3  9713  ranksnb  9751  ranklim  9768  r1pw  9769  r1pwALT  9770  r1pwcl  9771  rankuni2b  9777  djuexb  9833  cardmin2  9923  infxpenc2lem1  9941  dfac8alem  9951  dfac8clem  9954  ac5num  9958  acni2  9968  acnlem  9970  alephon  9991  alephfplem3  10028  alephfplem4  10029  dfac4  10044  dfac5lem1  10045  dfac5lem5  10049  dfac2a  10052  dfac2b  10053  dfacacn  10064  dfac12lem2  10067  dfac12r  10069  dfac12k  10070  cofsmo  10191  cfsmolem  10192  isfin1a  10214  fin1ai  10215  isfin3  10218  infpssrlem3  10227  fin23lem7  10238  fin23lem11  10239  enfin2i  10243  isf34lem4  10299  fin1a2lem7  10328  hsmexlem9  10347  hsmexlem4  10351  hsmex  10354  axcc2lem  10358  axcc3  10360  axdc3lem2  10373  axcclem  10379  zornn0g  10427  ttukeylem3  10433  ttukeylem6  10436  ttukey2g  10438  brdom7disj  10453  brdom6disj  10454  fnct  10459  konigthlem  10491  axregndlem2  10526  axinfnd  10529  axacndlem5  10534  axacnd  10535  fpwwe2lem4  10557  fpwwe2lem12  10565  fpwwe  10569  pwfseqlem1  10581  pwfseqlem3  10583  pwfseqlem4a  10584  pwfseqlem4  10585  wununi  10629  wunpw  10630  wunpr  10632  wunr1om  10642  tskpw  10676  tskr1om  10690  inar1  10698  grupw  10718  grupr  10720  gruurn  10721  gruiun  10722  ingru  10738  grur1a  10742  grothomex  10752  grothac  10753  addnidpi  10824  indpi  10830  adderpq  10879  mulerpq  10880  addclprlem2  10940  mulclprlem  10942  distrlem4pr  10949  prlem934  10956  ltexprlem3  10961  ltexprlem4  10962  ltexprlem7  10965  ltexpri  10966  prlem936  10970  reclem2pr  10971  reclem3pr  10972  addclsr  11006  mulclsr  11007  supsrlem  11034  supsr  11035  axaddf  11068  axmulf  11069  axaddrcl  11075  axmulrcl  11077  renegcl  11457  negreb  11459  negn0  11579  negf1o  11580  ltord1  11676  leord1  11677  eqord1  11678  ltord2  11679  leord2  11680  eqord2  11681  negfi  12105  infm3  12115  cju  12155  indfval  12166  peano5nni  12177  peano2nn  12186  dfnn2  12187  nn1m1nn  12195  nnaddcl  12197  nnmulcl  12198  nnsub  12221  nndivtr  12224  un0addcl  12470  un0mulcl  12471  elnnnn0  12480  nn0sub  12487  fcdmnn0fsuppg  12497  elz  12526  nnnegz  12527  elz2  12542  znegclb  12564  zaddcl  12567  nzadd  12575  zmulcl  12576  zneo  12612  nneo  12613  zeo  12615  peano5uzi  12618  zindd  12630  uzp1  12825  uzaddcl  12854  ublbneg  12883  eqreznegel  12884  supminf  12885  zsupss  12887  qmulz  12901  qnegcl  12916  irradd  12923  irrmul  12924  xnn0xaddcl  13187  fzrev2  13542  injresinjlem  13745  negmod0  13837  om2uzuzi  13911  uzindi  13944  fsuppmapnn0ub  13957  mptnn0fsuppr  13961  seqexw  13979  seqcl2  13982  seqcl  13984  seqf  13985  monoord  13994  monoord2  13995  sermono  13996  seqsplit  13997  seqcaopr2  14000  seqid3  14008  seqhomo  14011  expcllem  14034  expcl2lem  14035  m1expcl2  14047  faccl  14245  facdiv  14249  facndiv  14250  bccmpl  14271  bccl  14284  hashclb  14320  hasheq0  14325  hashfn  14337  seqcoll  14426  opfi1uzind  14473  ccatalpha  14556  reuccatpfxs1lem  14708  reuccatpfxs1  14709  repswccat  14748  repswrevw  14749  2cshw  14775  2cshwcshw  14787  cshimadifsn  14791  cshco  14798  swrd2lsw  14914  wwlktovf  14918  wwlktovf1  14919  wwlktovfo  14920  wrd2f1tovbij  14922  shftlem  15030  shftf  15041  cjval  15064  cjth  15065  remim  15079  cnpart  15202  uzin2  15307  caubnd2  15320  sqreulem  15322  clim  15456  clim2  15466  lo1o12  15495  climrlim2  15509  lo1resb  15526  o1resb  15528  lo1eq  15530  climmpt2  15535  climshftlem  15536  rlimcld2  15540  climcn1  15554  climcn2  15555  o1dif  15592  iserex  15619  climub  15624  climserle  15625  isercoll  15630  climcau  15633  caurcvg2  15640  caucvgb  15642  summolem3  15676  summolem2a  15677  zsum  15680  fsum  15682  sumss2  15688  fsumcvg2  15689  fsumclf  15700  fsumsplitf  15704  fsumsplit1  15707  sumpr  15710  sumtp  15711  fsumm1  15713  fsum1p  15715  isummulc2  15724  fsum2dlem  15732  fsumcom2  15736  fsumshftm  15743  fsum0diag2  15745  fsumge1  15760  fsum00  15761  fsumabs  15764  telfsumo  15765  telfsumo2  15766  fsumparts  15769  fsumrlim  15774  fsumo1  15775  o1fsum  15776  fsumiun  15784  binomlem  15794  isumshft  15804  isum1p  15806  isumrpcl  15808  climcndslem1  15814  climcndslem2  15815  climcnds  15816  infcvgaux2i  15823  cvgrat  15848  mertens  15851  clim2prod  15853  prodfn0  15859  prodfrec  15860  prodfdiv  15861  ntrivcvgfvn0  15864  prodmolem3  15898  prodmolem2a  15899  zprod  15902  fprod  15906  prodss  15912  fprodser  15914  fprodm1  15932  fprod1p  15933  fprodm1s  15935  fprodp1s  15936  fprodabs  15939  fprodn0  15944  fprod2dlem  15945  fprodcnv  15948  fprodcom2  15949  fproddivf  15952  fprodsplitf  15953  fprodsplit1f  15955  bpolycl  16017  fprodefsum  16060  rpnnen2lem11  16191  mod2eq1n2dvds  16316  mulsucdiv2z  16322  zob  16328  nn0o1gt2  16350  nno  16351  nn0o  16352  divalglem7  16368  bitsf1  16415  sadcp1  16424  smupp1  16449  qnumdencl  16709  iserodd  16806  pcqcl  16827  pcxnn0cl  16831  pcxcl  16832  pcgcd1  16848  dvdsprmpweqle  16857  pcmpt  16863  pcmpt2  16864  pcmptdvds  16865  infpnlem2  16882  infpn2  16884  1arith  16898  elgz  16902  mul4sq  16925  4sqlem13  16928  4sqlem17  16932  4sqlem18  16933  4sqlem19  16934  vdwlem1  16952  vdwlem2  16953  vdwnn  16969  ramtcl2  16982  ramcl  17000  prmonn2  17010  prmodvdslcmf  17018  isstruct2  17119  wunress  17219  firest  17395  imasaddfnlem  17492  imasvscafn  17501  xpsfrnel2  17528  mreintcl  17557  ismred2  17565  mreexexlemd  17610  mreexexlem3d  17612  mreexexlem4d  17613  iscatd2  17647  catpropd  17675  subsubc  17820  isfunc  17831  inclfusubc  17910  fncnvimaeqv  18086  joindef  18340  joinval  18341  meetdef  18354  meetval  18355  oduclatb  18473  acsdrsel  18509  isacs4lem  18510  isacs5lem  18511  acsdrscl  18512  mgmsscl  18613  mgmpropd  18619  mgm1  18626  gsumvalx  18644  issubmgm  18670  issubmgm2  18671  mgmhmima  18683  sgrppropd  18699  mndpropd  18727  issubm  18771  0subm  18785  insubm  18786  mhmimalem  18792  gsumwsubmcl  18805  gsumwspan  18814  symggrplem  18852  sursubmefmnd  18864  injsubmefmnd  18865  smndex1basss  18876  mulgsubcl  19064  issubg  19102  issubg2  19117  issubg4  19121  0subg  19127  isnsg  19130  isnsg2  19131  nsgbi  19132  isnsg3  19135  elnmz  19138  nmzbi  19139  nmzsubg  19140  eqgval  19152  eqgid  19155  cycsubgcl  19181  ghmrn  19204  ghmnsgima  19215  gass  19276  oppgsubg  19338  f1omvdconj  19421  symgfisg  19443  psgneldm  19478  0subgALT  19543  odhash3  19551  sylow2blem2  19596  lsmsubm  19628  lsmsubg  19629  efgsf  19704  efgsdm  19705  efgs1b  19711  efgredlema  19715  eqgabl  19809  ablnsg  19822  cyggenod2  19860  gsumzaddlem  19896  gsummhm2  19914  gsum2dlem2  19946  gsum2d2lem  19948  gsumcom2  19950  dprdfeq0  19999  dprdsubg  20001  dprd2da  20019  ablfacrp  20043  pgpfac1lem3  20054  pgpfaclem1  20058  ablfaclem3  20064  ablfac2  20066  cycsubggenodd  20086  isrng  20135  issrg  20169  srgfcl  20177  rglcom4d  20192  srgbinomlem4  20210  isring  20218  iscrng  20221  dvdsr  20342  irredrmul  20407  isrngim  20425  isrim0  20462  issubrng  20524  subrngringnsg  20530  issubrng2  20535  rhmimasubrnglem  20542  issubrg  20548  issubrg2  20569  subrgpropd  20585  isdrngd  20742  isdrngdOLD  20744  issdrg  20765  sdrgacs  20778  issrngd  20832  islmod  20859  lmodlema  20860  islmodd  20861  lmodprop2d  20919  rmodislmodlem  20924  rmodislmod  20925  lssset  20928  islssd  20930  lsscl  20937  lsslss  20956  lsspropd  21012  lmhmima  21042  lbsind  21075  lsmcl  21078  islvec  21099  lmhmlvec  21105  lspsolvlem  21140  lspsolv  21141  lvecpropd  21165  rnglidlmcl  21214  rnglidl0  21227  rnglidlmmgm  21243  rngqiprngimf1lem  21292  rngqiprngimf1  21298  ring2idlqus  21307  xrsdsreclblem  21393  xrsdsreclb  21394  cnsubrglem  21397  prmirred  21454  pzriprnglem4  21464  pzriprnglem8  21468  pzriprngALT  21475  znunithash  21544  cofipsgn  21573  zrhpsgnelbas  21574  rzgrp  21603  isphl  21608  phllmhm  21612  ipcl  21613  isphld  21634  phlpropd  21635  phlssphl  21639  cssincl  21668  pjdm  21687  dsmmval  21714  dsmmbas2  21717  dsmmelbas  21719  frlmbas  21735  frlmup1  21778  lindfind  21796  lindsind  21797  f1lindf  21802  islindf4  21818  psrbag  21897  psrbaglefi  21906  mplsubglem  21977  mpllsslem  21978  ltbwe  22022  psrbagsn  22041  subrgasclcl  22045  mplind  22048  mpfind  22093  psdmul  22132  coe1mul2lem2  22233  gsumply1eq  22274  evl1vsd  22309  mpfpf1  22316  pf1mpf  22317  pf1ind  22320  matecl  22390  m1detdiag  22562  mdetralt  22573  mdetralt2  22574  mdetunilem2  22578  mdetunilem9  22585  m2detleiblem3  22594  m2detleiblem4  22595  smadiadetlem0  22626  cpmatacl  22681  chpscmat  22807  uniopn  22862  inopn  22864  fiinopn  22866  istps  22899  fctop  22969  iscld  22992  isopn2  22997  mretopd  23057  iscldtop  23060  perfi  23120  tgrest  23124  restcld  23137  ordtbaslem  23153  ordtrest2lem  23168  ordtrest2  23169  iscn  23200  cnpval  23201  iscnp  23202  tgcn  23217  subbascn  23219  ssidcn  23220  lmbrf  23225  cnpnei  23229  cnima  23230  iscncl  23234  cnconst2  23248  cnrest2  23251  cnpresti  23253  cnprest  23254  cnindis  23257  lmres  23265  lmcnp  23269  iscnrm  23288  t1sncld  23291  cnrmi  23325  cncmp  23357  cmpsublem  23364  fiuncmp  23369  unconn  23394  conncompid  23396  conncompconn  23397  conncompss  23398  1stcfb  23410  2ndcrest  23419  2ndcctbss  23420  2ndcdisj  23421  1stccnp  23427  islly  23433  isnlly  23434  subislly  23446  restnlly  23447  restlly  23448  islly2  23449  hausllycmp  23459  cldllycmp  23460  dislly  23462  isptfin  23481  islocfin  23482  ptfinfin  23484  finlocfin  23485  dissnlocfin  23494  locfindis  23495  comppfsc  23497  kgenval  23500  elkgen  23501  kgeni  23502  cmpkgen  23516  1stckgenlem  23518  kgencn2  23522  ptpjpre1  23536  elpt  23537  elptr  23538  ptbasin  23542  xkobval  23551  xkoval  23552  xkoopn  23554  txbasval  23571  tx1cn  23574  tx2cn  23575  dfac14  23583  xkoccn  23584  txcnp  23585  ptcnplem  23586  txcnmpt  23589  txindislem  23598  txdis1cn  23600  txlly  23601  txnlly  23602  pthaus  23603  ptrescn  23604  hauseqlcld  23611  txlm  23613  tx2ndc  23616  txkgen  23617  xkoptsub  23619  xkopt  23620  xkoco1cn  23622  xkoco2cn  23623  xkococnlem  23624  xkococn  23625  cnmpt11  23628  cnmpt12  23632  cnmpt21  23636  cnmpt22  23639  cnmptkp  23645  cnmptk1p  23650  xkoinjcn  23652  txconn  23654  qtopval2  23661  elqtop  23662  idqtop  23671  qtopcld  23678  qtopeu  23681  qtoprest  23682  qtopomap  23683  qtopcmap  23684  ishmeo  23724  hmeoopn  23731  hmeocld  23732  ordthmeolem  23766  ptcmpfi  23778  elmptrab  23792  fgcl  23843  trfil2  23852  cfinfil  23858  uzrest  23862  ufilss  23870  trufil  23875  cfinufil  23893  ufinffr  23894  ufildr  23896  rnelfm  23918  flfcntr  24008  ptcmplem2  24018  ptcmplem3  24019  ptcmplem4  24020  ptcmplem5  24021  cnextfvval  24030  tmdcn2  24054  tmdmulg  24057  tmdgsum2  24061  symgtgp  24071  opnsubg  24073  clssubg  24074  tgpconncompeqg  24077  ghmcnp  24080  tgphaus  24082  tgpt0  24084  qustgpopn  24085  qustgplem  24086  tsmsgsum  24104  tsmssubm  24108  tsmsres  24109  tsmsf1o  24110  tsmsxplem1  24118  tsmsxplem2  24119  tsmsxp  24120  istrg  24129  istdrg  24131  istdrg2  24143  istlm  24150  istvc  24157  ustval  24168  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  ust0  24185  ucnima  24245  fmucndlem  24255  prdsdsf  24332  prdsxmet  24334  imasf1oxmet  24340  imasf1omet  24341  prdsxmslem2  24494  metustsym  24520  isnlm  24640  qtopbaslem  24723  xrtgioo  24772  reperflem  24784  fsumcn  24837  expcn  24839  xrhmeo  24913  cnllycmp  24923  bndth  24925  isclm  25031  lmhmclm  25054  lmmcvg  25228  fmcfil  25239  iscfil3  25240  iscau2  25244  iscau4  25246  iscmet3lem1  25258  iscmet3  25260  cfilres  25263  caussi  25264  equivcfil  25266  flimcfil  25281  bcthlem1  25291  isbn  25305  srabn  25327  ishl2  25337  cmslssbn  25339  cmscsscms  25340  minveclem3b  25395  ivthlem1  25418  ivthlem2  25419  ivthlem3  25420  ivth2  25422  ivthle  25423  ivthle2  25424  ivthicc  25425  ovolficcss  25436  ovolunlem1a  25463  ovolunlem1  25464  ovolfiniun  25468  ovoliunlem1  25469  ovoliunlem3  25471  ovoliun  25472  ovoliun2  25473  shft2rab  25475  ovolshftlem1  25476  sca2rab  25479  ovolscalem1  25480  mblsplit  25499  finiunmbl  25511  volun  25512  volfiniun  25514  voliunlem1  25517  voliunlem3  25519  iunmbl  25520  voliun  25521  volsup  25523  ioombl  25532  ioorcl  25544  vitalilem1  25575  vitalilem2  25576  vitalilem3  25577  vitalilem4  25578  vitali  25580  ismbf1  25591  mbfdm  25593  ismbf  25595  ismbfcn  25596  mbfima  25597  mbfimaicc  25598  ismbfcn2  25605  ismbfd  25606  ismbf2d  25607  mbfeqalem1  25608  mbfmax  25616  mbfposr  25619  mbfposb  25620  ismbf3d  25621  mbfimaopnlem  25622  mbfimaopn2  25624  cncombf  25625  isi1f  25641  i1fd  25648  itg1mulc  25671  mbfi1fseqlem4  25685  itg2lcl  25694  isibl  25732  iblitg  25735  iblcnlem1  25755  iblcnlem  25756  iblrelem  25758  iblpos  25760  itgeqa  25781  itgfsum  25794  itgabs  25802  limcvallem  25838  ellimc  25840  ellimc2  25844  limcmpt  25850  cnmptlimc  25857  dvbsss  25869  cpnfval  25899  elcpn  25901  dvmptfsum  25942  dvle  25974  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  dvfsumrlimf  25992  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsumrlimge0  25997  dvfsumrlim  25998  dvfsumrlim2  25999  dvfsum2  26001  itgsubstlem  26015  itgsubst  26016  mdegcl  26034  deg1nn0clb  26055  isuc1p  26106  plyeq0lem  26175  plyco  26206  plycj  26242  plycjOLD  26244  dvply2g  26251  dvnply2  26253  plydivlem4  26262  fta1lem  26273  fta1  26274  elqaalem1  26285  elqaalem2  26286  elqaalem3  26287  elqaa  26288  ulmcau  26360  radcnv0  26381  radcnvlt1  26383  radcnvle  26385  pserdvlem2  26393  coseq1  26489  efeq1  26492  sinord  26498  efif1olem2  26507  efif1olem4  26509  lognegb  26554  logcj  26570  argimgt0  26576  logtayl  26624  2irrexpq  26695  root1eq1  26719  logrec  26727  2irrexpqALT  26764  angrteqvd  26770  angpieqvdlem  26792  atans  26894  atans2  26895  dmarea  26921  areambl  26922  rlimcnp  26929  rlimcnp2  26930  xrlimcnp  26932  harmonicbnd  26967  harmonicbnd2  26968  lgamcvglem  27003  wilthlem2  27032  wilth  27034  efnnfsumcl  27066  vmacl  27081  efvmacl  27083  efchtdvds  27122  sqff1o  27145  fsumdvdscom  27148  musumsum  27155  fsumdvdsmul  27158  fsumvma  27176  perfect  27194  dchrelbasd  27202  lgsval  27264  lgsval2lem  27270  lgsdir2lem4  27291  lgsdir2  27293  lgsqrlem1  27309  lgsdchr  27318  m1lgs  27351  2lgs  27370  mul2sq  27382  2sqlem6  27386  2sqblem  27394  2sq2  27396  rplogsumlem2  27448  dchrisumlema  27451  dchrisumlem2  27453  dchrisumlem3  27454  dchrvmasumlem2  27461  dchrvmasumlem3  27462  dchrisum0flblem2  27472  dchrisum0flb  27473  dchrisum0fno1  27474  ostthlem1  27590  nodmon  27614  noextendseq  27631  nodense  27656  madefi  27905  addsproplem1  27961  addsproplem3  27963  addsprop  27968  addsf  27974  addbdaylem  28009  negsproplem1  28020  negsproplem3  28022  negsprop  28027  negbdaylem  28048  mulsproplemcbv  28107  mulsproplem1  28108  mulsproplem10  28117  mulsprop  28122  addonbday  28271  noseqp1  28283  noseqind  28284  peano5n0s  28311  dfn0s2  28324  n0addscl  28336  n0mulscl  28337  n0bday  28344  onsfi  28348  n0s0m1  28354  n0subs  28355  n0p1nns  28363  dfnns2  28364  nn1m1nns  28366  oldfib  28369  zaddscl  28386  zmulscld  28389  elzn0s  28390  peano5uzs  28396  expscllem  28422  z12addscl  28469  z12shalf  28472  z12negsclb  28473  z12zsodd  28474  z12bdaylem  28476  z12bday  28477  bdayfin  28479  mirval  28723  perpneq  28782  isperp2  28783  isperp2d  28784  foot  28790  islnopp  28807  islnoppd  28808  outpasch  28823  hlpasch  28824  ishpg  28827  colopp  28837  colhp  28838  lmif  28853  islmib  28855  lmiinv  28860  trgcopy  28872  trgcopyeu  28874  acopyeu  28902  inaghl  28913  tgasa1  28926  f1otrgitv  28938  f1otrg  28939  isfusgr  29387  opfusgr  29392  fusgrfisbase  29397  fusgrfisstep  29398  nbupgrel  29414  nbumgrvtx  29415  nbusgreledg  29422  edgnbusgreu  29436  nb3grprlem1  29449  uvtxusgrel  29472  cusgredg  29493  cplgr2vpr  29502  cusgrexg  29513  usgredgsscusgredg  29528  fusgrn0degnn0  29568  rusgrnumwrdl2  29655  rgrx0ndm  29662  wlkcomp  29699  wlkdlem2  29750  clwlkcomp  29847  iswwlks  29904  wwlknllvtx  29914  0enwwlksnge1  29932  wlkiswwlks2lem5  29941  wwlksm1edg  29949  wwlksnred  29960  wwlksnext  29961  wwlksnextbi  29962  wwlksnredwwlkn  29963  wwlksnextfun  29966  wwlksnextinj  29967  wwlksnextsurj  29968  wwlksnextbij  29970  wwlksnfi  29974  wwlksnextproplem2  29978  wwlksnextprop  29980  2wlkdlem4  29996  rusgrnumwwlkl1  30039  rusgrnumwwlks  30045  isclwwlk  30054  clwwlk1loop  30058  clwwlkccatlem  30059  clwlkclwwlklem2a1  30062  clwlkclwwlklem2a4  30067  clwlkclwwlklem2a  30068  clwlkclwwlklem2  30070  clwlkclwwlklem3  30071  clwlkclwwlk  30072  clwlkclwwlk2  30073  clwwisshclwwslemlem  30083  clwwisshclwwslem  30084  clwwisshclwws  30085  clwwlknlbonbgr1  30109  clwwlkinwwlk  30110  clwwlkn1  30111  loopclwwlkn1b  30112  clwwlkn1loopb  30113  clwwlkn2  30114  clwwlkel  30116  clwwlkf  30117  clwwlkwwlksb  30124  clwwlkext2edg  30126  wwlksext2clwwlk  30127  wwlksubclwwlk  30128  eleclclwwlknlem2  30131  umgr2cwwk2dif  30134  s2elclwwlknon2  30174  clwwlknonwwlknonb  30176  clwwlknonex2lem2  30178  clwwlknonex2  30179  3wlkdlem4  30232  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  eupth2lem2  30289  eulerpathpr  30310  1vwmgr  30346  3vfriswmgrlem  30347  3vfriswmgr  30348  3cyclfrgrrn1  30355  vdgn1frgrv2  30366  frgrncvvdeqlem3  30371  frgrncvvdeqlem8  30376  frgrncvvdeqlem9  30377  frgrwopregasn  30386  frgrwopregbsn  30387  frgrwopreglem5ALT  30392  frgr2wwlk1  30399  frgr2wwlkeqm  30401  fusgr2wsp2nb  30404  2clwwlk2clwwlklem  30416  extwwlkfabel  30423  nvvop  30680  isnvlem  30681  sspval  30794  nmorepnf  30839  phpar  30895  siilem2  30923  bnsscmcl  30939  ubthlem1  30941  shaddcl  31288  shmulcl  31289  hsn0elch  31319  hhssablo  31334  hhssnvt  31336  hhsssh  31340  shscl  31389  shintcl  31401  chintcl  31403  shincl  31452  chincl  31570  h1datomi  31652  chscllem2  31709  sumspansn  31720  spansncvi  31723  5oalem2  31726  5oalem3  31727  pjini  31770  pjjsi  31771  eigposi  31907  nmoprepnf  31938  nmfnrepnf  31951  dmadjrnb  31977  lnophmlem1  32087  lnophm  32090  nmcopex  32100  lnconi  32104  nmbdfnlb  32121  nmcfnex  32124  imaelshi  32129  rnbra  32178  leopg  32193  pjbdlni  32220  pjhmop  32221  hmopidmch  32224  pjclem4  32270  pj3si  32278  strlem1  32321  atssma  32449  atcv0eq  32450  atcv1  32451  atomli  32453  atcvatlem  32456  cdj3lem2a  32507  cdj3lem3a  32510  xppreima  32718  fmptcof2  32730  aciunf1lem  32735  funcnv4mpt  32741  1stpreimas  32779  f1od2  32792  fpwrelmapffslem  32805  xrofsup  32840  fzspl  32862  fzsplit3  32866  nnindf  32893  fprodex01  32898  fsumiunle  32902  indf1ofs  32926  gsumhashmul  33128  fzto1st  33164  fxpsubm  33233  fxpsubg  33234  fxpsubrg  33235  isslmd  33263  slmdlema  33264  elrgspnlem2  33304  elrgspnlem4  33306  subsdrg  33359  qusker  33409  0nellinds  33430  unitprodclb  33449  nsgmgclem  33471  nsgmgc  33472  nsgqusf1olem2  33474  elrspunidl  33488  prmidlval  33497  prmidlc  33508  opprlidlabs  33545  dfufd2lem  33609  psrbasfsupp  33672  lindsunlem  33768  brfldext  33789  brfinext  33796  finextfldext  33808  finexttrb  33809  extdg1id  33810  fldextrspunlsplem  33817  constrconj  33889  constrfin  33890  trisecnconstr  33936  smatrcl  33940  submateq  33953  lmatfval  33958  lmatcl  33960  qtophaus  33980  locfinreflem  33984  locfinref  33985  zartopn  34019  zarcmplem  34025  rhmpreimacnlem  34028  xpinpreima  34050  xpinpreima2  34051  cnre2csqlem  34054  tpr2rico  34056  prsdm  34058  prsrn  34059  ordtrest2NEWlem  34066  ordtrest2NEW  34067  zrhcntr  34123  qqhval2  34126  isrrext  34144  ismntoplly  34169  esumcvg  34230  sigaval  34255  issiga  34256  0elsiga  34258  sigaclcu  34261  issgon  34267  prsiga  34275  sigaclci  34276  difelsiga  34277  unelsiga  34278  ispisys2  34297  inelpisys  34298  unelldsys  34302  sigapildsyslem  34305  sigapildsys  34306  ldgenpisyslem1  34307  ldgenpisys  34310  isros  34312  unelros  34315  difelros  34316  fiunelros  34318  inelsros  34322  diffiunisros  34323  rossros  34324  measvuni  34358  measiun  34362  voliune  34373  volfiniune  34374  brfae  34392  ismbfm  34395  mbfmcnvima  34399  mbfmcst  34403  1stmbfm  34404  2ndmbfm  34405  imambfm  34406  sitgval  34476  issibf  34477  sibfima  34482  sitgfval  34485  sitgclg  34486  eulerpartlemelr  34501  eulerpartlemsf  34503  eulerpartleme  34507  eulerpartlemt0  34513  eulerpartlemt  34515  eulerpartgbij  34516  eulerpartlemr  34518  eulerpartlemmf  34519  eulerpartlemgvv  34520  eulerpartlemgs2  34524  eulerpartlemn  34525  eulerpart  34526  cndprobprob  34582  rrvsum  34598  orvcelel  34614  ballotlemodife  34642  ballotlemsdom  34656  ballotlemrv  34664  ballotlemrv1  34665  ballotlemrv2  34666  ballotlem1ri  34679  fsum2dsub  34751  reprinfz1  34766  reprpmtf1o  34770  reprdifc  34771  breprexplema  34774  hgt750lema  34801  hgt750leme  34802  bnj149  35017  bnj222  35025  bnj1112  35125  bnj1148  35138  fissorduni  35233  fineqvrep  35258  fineqvnttrclse  35268  fineqvinfep  35269  gblacfnacd  35284  vonf1owev  35290  loop1cycl  35319  subfacp1lem3  35364  subfacp1lem6  35367  erdszelem10  35382  kur14  35398  cvxsconn  35425  cnllysconn  35427  resconn  35428  iscvm  35441  cvmliftlem5  35471  cvmliftlem15  35480  cvmlift2lem1  35484  cvmlift2lem12  35496  cvmlift2lem13  35497  sat1el2xp  35561  fmlasuc  35568  gonan0  35574  gonar  35577  satefvfmla0  35600  msubrn  35711  msubco  35713  ismfs  35731  mvtinf  35737  mclsax  35751  mppspstlem  35753  elmpps  35755  nnuni  35909  dfdm5  35955  dfrn5  35956  elima4  35958  rdgprc0  35973  pprodss4v  36064  elfuns  36095  fnimage  36109  imageval  36110  fwddifval  36344  fwddifnval  36345  fwddifnp1  36347  elhf2g  36358  hfun  36360  hfninf  36368  filnetlem4  36563  onsucconn  36620  onsucsuccmp  36626  limsucncmp  36628  onint1  36631  fveleq  36633  findreccl  36635  nndivsub  36639  weiunse  36650  mh-inf3f1  36723  mh-infprim2bi  36729  mh-infprim3bi  36730  bj-seex  37229  bj-adjg1  37350  bj-mooreset  37414  bj-ismoored0  37418  bj-ismoored  37419  bj-inftyexpitaudisj  37519  bj-inftyexpidisj  37524  bj-isvec  37601  bj-isclm  37605  csbmpo123  37647  topdifinffinlem  37663  topdifinffin  37664  csbfinxpg  37704  phpreu  37925  finixpnum  37926  lindsenlbs  37936  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem28  37969  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  poimir  37974  mblfinlem3  37980  ex-ovoliunnfl  37984  voliunnfl  37985  volsupnfl  37986  mbfresfi  37987  itgabsnc  38010  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  dvasin  38025  sdclem2  38063  fdc  38066  incsequz  38069  neificl  38074  mettrifi  38078  cntotbnd  38117  cnpwstotbnd  38118  ismtyima  38124  ismtyhmeolem  38125  heiborlem2  38133  heiborlem3  38134  heiborlem4  38135  heiborlem5  38136  heiborlem6  38137  heiborlem10  38141  isrngo  38218  isdivrngo  38271  drngoi  38272  idlval  38334  isidlc  38336  idladdcl  38340  idllmulcl  38341  idlrmulcl  38342  0idl  38346  pridlval  38354  smprngopr  38373  prnc  38388  ispridlc  38391  pridlc  38392  eqrelf  38579  iss2  38665  elcoeleqvrels  39000  elfunsALTV  39098  eldisjs  39140  eleldisjs  39149  fsumshftd  39398  riotaclbgBAD  39400  renegclALT  39409  lshpinN  39435  isopos  39626  oposlem  39628  glbconN  39823  lnnat  39873  2at0mat0  39971  islvol2aN  40038  dalawlem13  40329  pclfinclN  40396  lhpoc2N  40461  ltrncnvatb  40584  cdleme11h  40712  cdlemefr32sn2aw  40850  cdlemefs32sn1aw  40860  cdleme32fvaw  40885  cdlemg1fvawlemN  41019  dicelvalN  41624  dih1dimatlem  41775  dihlatat  41783  dihjatcclem4  41867  islpolN  41929  lpolsatN  41934  lpolpolsatN  41935  mapdordlem1a  42080  mapdordlem1  42082  mapdhcl  42173  iscsrg  42410  fzsplitnd  42421  lcmineqlem12  42479  intlewftc  42500  dvrelogpow2b  42507  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  dvle2  42511  aks4d1p8  42526  aks4d1p9  42527  isprimroot  42532  primrootsunit1  42536  primrootscoprmpow  42538  aks6d1c1p1  42546  aks6d1c1p2  42548  aks6d1c1p3  42549  evl1gprodd  42556  hashscontpow  42561  aks6d1c3  42562  aks6d1c2  42569  sticksstones1  42585  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  aks6d1c6lem1  42609  unitscyglem5  42638  retire  42751  reelznn0nn  42906  fsuppind  43023  fsuppssindlem2  43025  fsuppssind  43026  isnacs3  43142  nacsfix  43144  mzpclval  43157  mzpcl1  43161  mzpcl2  43162  mzpcl34  43163  mzpexpmpt  43177  mzpsubst  43180  diophin  43204  diophun  43205  2rexfrabdioph  43224  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  rabdiophlem2  43230  diophren  43241  fphpd  43244  fphpdo  43245  fiphp3d  43247  pellexlem1  43257  pell14qrexpclnn0  43294  pellqrex  43307  rmspecnonsq  43335  monotuz  43369  monotoddzzfi  43370  monotoddzz  43371  oddcomabszz  43372  modabsdifz  43414  rmxdioph  43444  expdiophlem2  43450  limsuc2  43469  dfac11  43490  kelac1  43491  dfac21  43494  lsmfgcl  43502  islnm  43505  lnmlssfg  43508  lmhmfgima  43512  pwslnm  43522  unxpwdom3  43523  pwfi2f1o  43524  islnr  43539  hbtlem2  43552  cnsrexpcl  43593  flcidc  43598  mendlmod  43617  proot1ex  43624  oaordnr  43724  omnord1  43733  oenord1  43744  cantnfresb  43752  onmcl  43759  tfsnfin  43780  nadd2rabtr  43812  nadd1rabtr  43816  nadd1rabex  43818  nadd1suc  43820  pwelg  43987  fipjust  43992  elnonrel  44012  elinlem  44025  elcnvlem  44028  ss2iundf  44086  dfhe3  44202  dffrege115  44405  rfovcnvf1od  44431  ntrneiel2  44513  clsneiel2  44536  neicvgel2  44547  grur1cld  44659  dvgrat  44739  cvgdvgrat  44740  radcnvrat  44741  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  orbitcl  45384  modelaxreplem1  45405  modelaxreplem2  45406  modelaxrep  45408  fnchoice  45460  fiiuncl  45496  disjf1  45613  disjinfi  45622  choicefi  45629  axccdom  45651  fmptf  45668  fmptff  45698  monoords  45730  supminfrnmpt  45873  supxrleubrnmptf  45879  supminfxr  45892  supminfxr2  45897  supminfxrrnmpt  45899  monoordxrv  45909  monoordxr  45910  monoord2xrv  45911  monoord2xr  45912  caucvgbf  45917  cvgcaule  45919  fsummulc1f  46001  fsumnncl  46002  fsumf1of  46004  fsumreclf  46006  fsumlessf  46007  fsumsermpt  46009  fmul01  46010  fmulcl  46011  fmuldfeqlem1  46012  fmuldfeq  46013  fmul01lt1lem1  46014  fmul01lt1lem2  46015  fprodexp  46024  fprodabs2  46025  mccllem  46027  mccl  46028  fprodcnlem  46029  fprodcn  46030  climmulf  46034  climsuse  46038  climrecf  46039  climaddf  46045  climf  46052  sumnnodd  46060  clim2f  46064  0ellimcdiv  46077  climsubmpt  46088  climreclf  46092  climf2  46094  fnlimcnv  46095  climeldmeqmpt  46096  clim2f2  46098  climfveqmpt  46099  fnlimfvre  46102  fnlimabslt  46107  climfveqmpt3  46110  climbddf  46115  climeldmeqmpt3  46117  climinf2mpt  46142  climinfmpt  46143  limsupequzmptf  46159  lmbr3  46175  liminfreuzlem  46230  coseq0  46292  cncfshift  46302  cncfperiod  46307  fprodcncf  46328  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvmptmulf  46365  dvnmptdivc  46366  dvnmul  46371  dvmptfprod  46373  iblspltprt  46401  itgspltprt  46407  stoweidlem2  46430  stoweidlem3  46431  stoweidlem4  46432  stoweidlem6  46434  stoweidlem8  46436  stoweidlem17  46445  stoweidlem19  46447  stoweidlem20  46448  stoweidlem21  46449  stoweidlem23  46451  stoweidlem27  46455  stoweidlem35  46463  stoweidlem42  46470  stoweidlem43  46471  stoweidlem62  46490  stoweid  46491  wallispilem3  46495  wallispi  46498  fourierdlem16  46551  fourierdlem21  46556  fourierdlem41  46576  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem51  46585  fourierdlem54  46588  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem71  46605  fourierdlem72  46606  fourierdlem73  46607  fourierdlem83  46617  fourierdlem86  46620  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem100  46634  fourierdlem103  46637  fourierdlem104  46638  fourierdlem105  46639  fourierdlem108  46642  fourierdlem109  46643  fourierdlem110  46644  fourierdlem112  46646  fourierdlem113  46647  etransclem24  46686  salunicl  46744  saluncl  46745  saldifcl  46747  sge0f1o  46810  sge0lempt  46838  sge0iunmptlemfi  46841  sge0p1  46842  sge0fodjrnlem  46844  sge0iunmpt  46846  sge0ltfirpmpt2  46854  sge0isummpt2  46860  sge0xaddlem2  46862  sge0xadd  46863  ismea  46879  nnfoctbdjlem  46883  nnfoctbdj  46884  meadjiun  46894  voliunsge0lem  46900  meaiuninclem  46908  meaiuninc3v  46912  hoidmvlelem2  47024  hoidmvlelem3  47025  vonvolmbl2  47091  hoimbl2  47093  vonhoire  47100  vonicclem2  47112  vonn0ioo2  47118  vonn0icc2  47120  salpreimagelt  47135  salpreimalegt  47137  salpreimagtge  47153  salpreimaltle  47154  issmf  47156  salpreimagtlt  47158  smfpreimalt  47159  smfpreimaltf  47164  issmfle  47173  smfpreimale  47182  issmfgt  47184  smfpreimagt  47190  issmfgelem  47197  issmfge  47198  smflimlem4  47202  smflim  47205  smfpreimage  47210  smfresal  47216  smfpimbor1lem1  47226  smfpimbor1lem2  47227  smflim2  47234  smflimmpt  47238  smflimsuplem1  47248  smflimsuplem2  47249  smflimsuplem3  47250  smflimsuplem5  47252  smflimsuplem7  47254  smflimsup  47256  smfliminf  47259  ormkglobd  47305  cjnpoly  47337  eu2ndop1stv  47573  dmfcoafv  47623  ffnaov  47647  faovcl  47648  funressndmafv2rn  47671  dfatdmfcoafv2  47702  mod2addne  47818  smonoord  47825  iccpartiltu  47882  iccpartigtl  47883  sprsymrelf1lem  47951  prproropf1olem2  47964  fmtno4prmfac193  48036  proththdlem  48076  proththd  48077  iseven  48104  isodd  48105  dfodd2  48112  evenm1odd  48115  evenp1odd  48116  enege  48121  onego  48122  epee  48181  perfectALTV  48199  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbndlem4  48284  bgoldbtbnd  48285  clnbupgrel  48310  edgusgrclnbfin  48318  grimuhgr  48363  uhgrimedgi  48366  uhgrimprop  48368  isuspgrim0  48370  isuspgrimlem  48371  grimedg  48411  grtriproplem  48415  grtrif1o  48418  isgrtri  48419  grtriclwlk3  48421  cycl3grtrilem  48422  cycl3grtri  48423  grimgrtri  48425  usgrgrtrirex  48426  isubgr3stgrlem7  48448  grlimprclnbgrvtx  48475  grlimgredgex  48476  grlimgrtri  48479  usgrexmpl1tri  48501  gpgvtxel2  48524  gpgvtx0  48529  gpgvtx1  48530  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgedgiov  48541  gpgedg2ov  48542  gpgedg2iv  48543  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  gpg3kgrtriex  48565  gpgprismgr4cycllem3  48573  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  pgnbgreunbgr  48601  grlimedgnedg  48607  uzlidlring  48711  cbvmpox2  48812  lmod1  48968  nnolog2flm1  49066  dignn0flhalflem1  49091  catprsc  49488  nelsubc3lem  49545  fucofulem2  49786  fucofvalne  49800  isthincd2lem2  49910  euendfunc  50001  cnelsubclem  50078