Theorem eleq1d 2851

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-clel 2841

This theorem is used by:  eleq1  2854  eleq12d  2860  eqeltrd  2866  eqneltrd  2886  rspcimdv  3574  reuind  3719  sbcel2  4386  sbccsb2  4405  disjiun  5102  breq1  5117  breq2  5118  axrep6g  5256  inex1g  5293  intex  5319  pwexg  5354  reusv2lem4  5377  reusv2  5379  reusv3  5381  rabxfrd  5393  prexOLD  5419  opelopabsb  5519  csbmpt12  5547  pofun  5592  seex  5625  seinxp  5750  opabid2  5820  opeliunxp2  5829  elrn2g  5885  opeldmd  5901  opeldm  5902  elreldm  5930  elsnres  6025  iss  6042  unielrel  6281  onunel  6475  funopg  6577  brprcneu  6878  brprcneuALT  6879  tz6.12f  6913  ndmfvrcl  6921  ssimaex  6973  dmfco  6984  fvmpti  6995  fvmpt3  7001  fvmptf  7018  fvmptss2  7023  respreima  7068  fvn0ssdmfun  7076  fvelrn  7078  ffnfvf  7122  ffvresb  7128  fmptco  7132  fmptcof  7133  fsn  7138  fsn2g  7141  fressnfv  7164  fvrnressn  7165  fnex  7222  funfvima  7235  funfvima3  7241  f1mpt  7266  fliftfuns  7323  isoselem  7350  isowe2  7359  riotaclb  7421  ovrspc2v  7449  ffnov  7549  fovcld  7550  ovmpos  7571  ov2gf  7572  ovg  7588  funimassov  7600  oprssdm  7604  ndmovrcl  7609  caovclg  7615  elovmpo  7668  ofmpteq  7710  sorpsscmpl  7744  uniexg  7751  abnexg  7764  difsnexi  7769  onint  7798  limsuc  7854  tfisi  7864  peano5  7899  xpexr  7924  xpexcnv  7926  fnexALT  7957  focdmex  7962  f1stres  8019  f2ndres  8020  xp1st  8027  xp2nd  8028  unielxp  8033  opiota  8065  fmpox  8073  offval22  8092  frxp  8131  fnse  8138  frxp2  8149  sexp2  8151  frxp3  8156  sexp3  8158  opeliunxp2f  8215  dftpos4  8250  fvmpocurryd  8276  undefnel2  8283  onnseq  8340  smoel  8356  smo11  8360  tfrlem8  8380  tfrlem9  8381  tfrlem15  8388  tfr2b  8392  tz7.44-2  8403  tz7.44-3  8404  oacl  8529  omcl  8530  oecl  8531  oaord1  8545  omordi  8560  oen0  8581  oeeui  8597  nnacl  8606  nnmcl  8607  nnecl  8608  nnmordi  8626  nnaordex  8633  omsmolem  8652  naddcllem  8671  naddov2  8674  naddf  8677  naddssim  8681  naddelim  8682  naddasslem1  8690  naddasslem2  8691  naddsuc2  8697  erexb  8729  elecex  8754  qliftfuns  8811  ixpsnval  8907  elixp2  8908  resixp  8940  undifixp  8941  mptelixpg  8942  resixpfo  8943  elixpsn  8944  fundmen  9038  fopwdom  9083  disjen  9132  xpf1o  9137  unfi  9165  cnvfi  9170  fnfi  9172  f1oenfirn  9174  f1domfi  9175  unblem2  9263  pwfi  9288  fiint  9296  iunfi  9310  tfsnfin2  9330  isfsupp  9335  fsuppun  9357  ffsuppbi  9368  elfi2  9384  wdom2d  9552  ixpiunwdom  9562  dfom3  9626  cantnfvalf  9644  cantnflt  9651  cantnflem1  9668  r1fin  9755  tz9.12lem3  9771  ranksnb  9809  ranklim  9826  r1pw  9827  r1pwALT  9828  r1pwcl  9829  rankuni2b  9835  djuexb  9914  cardmin2  10004  infxpenc2lem1  10022  dfac8alem  10032  dfac8clem  10035  ac5num  10039  acni2  10049  acnlem  10051  alephon  10072  alephfplem3  10109  alephfplem4  10110  dfac4  10125  dfac5lem1  10126  dfac5lem5  10130  dfac2a  10132  dfac2b  10133  dfacacn  10144  dfac12lem2  10147  dfac12r  10149  dfac12k  10150  cofsmo  10271  cfsmolem  10272  isfin1a  10294  fin1ai  10295  isfin3  10298  infpssrlem3  10307  fin23lem7  10318  fin23lem11  10319  enfin2i  10323  isf34lem4  10379  fin1a2lem7  10408  hsmexlem9  10427  hsmexlem4  10431  hsmex  10434  axcc2lem  10438  axcc3  10440  axdc3lem2  10453  axcclem  10459  zornn0g  10507  ttukeylem3  10513  ttukeylem6  10516  ttukey2g  10518  brdom7disj  10533  brdom6disj  10534  fnct  10539  konigthlem  10571  axregndlem2  10606  axinfnd  10609  axacndlem5  10614  axacnd  10615  fpwwe2lem4  10637  fpwwe2lem12  10645  fpwwe  10649  pwfseqlem1  10661  pwfseqlem3  10663  pwfseqlem4a  10664  pwfseqlem4  10665  wununi  10709  wunpw  10710  wunpr  10712  wunr1om  10722  tskpw  10756  tskr1om  10770  inar1  10778  grupw  10798  grupr  10800  gruurn  10801  gruiun  10802  ingru  10818  grur1a  10822  grothomex  10832  grothac  10833  addnidpi  10904  indpi  10910  adderpq  10959  mulerpq  10960  addclprlem2  11020  mulclprlem  11022  distrlem4pr  11029  prlem934  11036  ltexprlem3  11041  ltexprlem4  11042  ltexprlem7  11045  ltexpri  11046  prlem936  11050  reclem2pr  11051  reclem3pr  11052  addclsr  11086  mulclsr  11087  supsrlem  11114  supsr  11115  axaddf  11148  axmulf  11149  axaddrcl  11155  axmulrcl  11157  renegcl  11539  negreb  11541  negn0  11661  negf1o  11662  ltord1  11758  leord1  11759  eqord1  11760  ltord2  11761  leord2  11762  eqord2  11763  negfi  12182  infm3  12192  cju  12232  indfval  12243  peano5nni  12254  peano2nn  12263  dfnn2  12264  nn1m1nn  12272  nnaddcl  12274  nnmulcl  12275  nnsub  12298  nndivtr  12301  un0addcl  12555  un0mulcl  12556  elnnnn0  12565  nn0sub  12572  fcdmnn0fsuppg  12582  elz  12611  nnnegz  12612  elz2  12627  znegclb  12649  zaddcl  12652  nzadd  12660  zmulcl  12661  zneo  12697  nneo  12698  zeo  12700  peano5uzi  12703  zindd  12715  uzp1  12917  uzaddcl  12946  ublbneg  12975  eqreznegel  12976  supminf  12977  zsupss  12979  qmulz  12993  qnegcl  13008  irradd  13015  irrmul  13016  xnn0xaddcl  13279  fzrev2  13635  injresinjlem  13838  negmod0  13931  om2uzuzi  14005  uzindi  14038  fsuppmapnn0ub  14051  mptnn0fsuppr  14055  seqexw  14073  seqcl2  14076  seqcl  14078  seqf  14079  monoord  14088  monoord2  14089  sermono  14090  seqsplit  14091  seqcaopr2  14094  seqid3  14102  seqhomo  14105  expcllem  14128  expcl2lem  14129  m1expcl2  14141  faccl  14339  facdiv  14343  facndiv  14344  bccmpl  14365  bccl  14378  hashclb  14414  hasheq0  14419  hashfn  14431  seqcoll  14521  opfi1uzind  14568  ccatalpha  14652  reuccatpfxs1lem  14807  reuccatpfxs1  14808  repswccat  14849  repswrevw  14850  2cshw  14876  2cshwcshw  14888  cshimadifsn  14892  cshco  14899  swrd2lsw  15015  wwlktovf  15019  wwlktovf1  15020  wwlktovfo  15021  wrd2f1tovbij  15023  shftlem  15131  shftf  15142  cjval  15179  cjth  15180  remim  15194  cnpart  15317  uzin2  15422  caubnd2  15435  sqreulem  15437  clim  15571  clim2  15581  lo1o12  15610  climrlim2  15624  lo1resb  15641  o1resb  15643  lo1eq  15645  climmpt2  15650  climshftlem  15651  rlimcld2  15655  climcn1  15669  climcn2  15670  o1dif  15707  iserex  15734  climub  15739  climserle  15740  isercoll  15745  climcau  15748  caurcvg2  15755  caucvgb  15757  summolem3  15791  summolem2a  15792  zsum  15795  fsum  15797  sumss2  15803  fsumcvg2  15804  fsumclf  15815  fsumsplitf  15819  fsumsplit1  15822  sumpr  15825  sumtp  15826  fsumm1  15828  fsum1p  15830  isummulc2  15839  fsum2dlem  15847  fsumcom2  15851  fsumshftm  15858  fsum0diag2  15860  fsumge1  15875  fsum00  15876  fsumabs  15879  telfsumo  15880  telfsumo2  15881  fsumparts  15884  fsumrlim  15889  fsumo1  15890  o1fsum  15891  fsumiun  15899  binomlem  15909  isumshft  15919  isum1p  15921  isumrpcl  15923  climcndslem1  15929  climcndslem2  15930  climcnds  15931  infcvgaux2i  15938  cvgrat  15963  mertens  15966  clim2prod  15968  prodfn0  15974  prodfrec  15975  prodfdiv  15976  ntrivcvgfvn0  15979  prodmolem3  16013  prodmolem2a  16014  zprod  16017  fprod  16021  prodss  16027  fprodser  16029  fprodm1  16047  fprod1p  16048  fprodm1s  16050  fprodp1s  16051  fprodabs  16054  fprodn0  16059  fprod2dlem  16060  fprodcnv  16063  fprodcom2  16064  fproddivf  16067  fprodsplitf  16068  fprodsplit1f  16070  bpolycl  16131  fprodefsum  16174  rpnnen2lem11  16305  mod2eq1n2dvds  16430  mulsucdiv2z  16436  zob  16442  nn0o1gt2  16464  nno  16465  nn0o  16466  divalglem7  16482  bitsf1  16529  sadcp1  16538  smupp1  16563  qnumdencl  16823  iserodd  16920  pcqcl  16941  pcxnn0cl  16945  pcxcl  16946  pcgcd1  16962  dvdsprmpweqle  16971  pcmpt  16977  pcmpt2  16978  pcmptdvds  16979  infpnlem2  16996  infpn2  16998  1arith  17012  elgz  17016  mul4sq  17039  4sqlem13  17042  4sqlem17  17046  4sqlem18  17047  4sqlem19  17048  vdwlem1  17066  vdwlem2  17067  vdwnn  17083  ramtcl2  17096  ramcl  17114  prmonn2  17124  prmodvdslcmf  17132  isstruct2  17234  wunress  17334  firest  17510  imasaddfnlem  17607  imasvscafn  17616  xpsfrnel2  17643  mreintcl  17672  ismred2  17680  mreexexlemd  17725  mreexexlem3d  17727  mreexexlem4d  17728  iscatd2  17762  catpropd  17790  subsubc  17935  isfunc  17946  inclfusubc  18025  fncnvimaeqv  18201  joindef  18455  joinval  18456  meetdef  18469  meetval  18470  oduclatb  18588  acsdrsel  18624  isacs4lem  18625  isacs5lem  18626  acsdrscl  18627  mgmsscl  18728  mgmpropd  18734  mgm1  18741  gsumvalx  18759  issubmgm  18785  issubmgm2  18786  mgmhmima  18798  sgrppropd  18814  mndpropd  18842  issubm  18886  0subm  18901  insubm  18902  mhmimalem  18908  gsumwsubmcl  18921  gsumwspan  18930  symggrplem  18968  sursubmefmnd  18980  injsubmefmnd  18981  smndex1basss  18992  mulgsubcl  19179  issubg  19217  issubg2  19233  issubg4  19237  0subg  19243  isnsg  19246  isnsg2  19247  nsgbi  19248  isnsg3  19251  elnmz  19254  nmzbi  19255  nmzsubg  19256  eqgval  19270  eqgid  19273  cycsubgcl  19302  ghmrn  19324  ghmnsgima  19335  gass  19396  oppgsubg  19458  f1omvdconj  19541  symgfisg  19563  psgneldm  19598  0subgALT  19663  odhash3  19671  sylow2blem2  19716  lsmsubm  19748  lsmsubg  19749  efgsf  19824  efgsdm  19825  efgs1b  19831  efgredlema  19835  eqgabl  19929  ablnsg  19942  cyggenod2  19980  gsumzaddlem  20016  gsummhm2  20034  gsum2dlem2  20066  gsum2d2lem  20068  gsumcom2  20070  dprdfeq0  20119  dprdsubg  20121  dprd2da  20139  ablfacrp  20163  pgpfac1lem3  20174  pgpfaclem1  20178  ablfaclem3  20184  ablfac2  20186  cycsubggenodd  20206  isrng  20257  issrg  20295  srgfcl  20303  rglcom4d  20318  srgbinomlem4  20336  isring  20344  iscrng  20347  dvdsr  20470  irredrmul  20535  isrngim  20553  isrim0  20591  issubrng  20676  subrngringnsg  20682  issubrng2  20687  rhmimasubrnglem  20694  issubrg  20700  issubrg2  20721  subrgpropd  20737  isdrngd  20898  isdrngdOLD  20900  issdrg  20921  sdrgacs  20934  issrngd  20988  islmod  21015  lmodlema  21016  islmodd  21017  lmodprop2d  21075  rmodislmodlem  21080  rmodislmod  21081  lssset  21084  islssd  21086  lsscl  21093  lsslss  21112  lsspropd  21168  lmhmima  21198  lbsind  21231  lsmcl  21234  islvec  21255  lmhmlvec  21261  lspsolvlem  21296  lspsolv  21297  lvecpropd  21321  rnglidlmcl  21371  rnglidl0  21385  rnglidlmmgm  21409  df2idl2crng  21451  rngqiprngimf1lem  21464  rngqiprngimf1  21470  ring2idlqus  21479  prmidlval  21492  prmidlc  21503  prmidlprop  21506  xrsdsreclblem  21593  xrsdsreclb  21594  cnsubrglem  21597  prmirred  21654  pzriprnglem4  21664  pzriprnglem8  21668  pzriprngALT  21675  znunithash  21744  cofipsgn  21773  zrhpsgnelbas  21774  rzgrp  21803  isphl  21808  phllmhm  21812  ipcl  21813  isphld  21834  phlpropd  21835  phlssphl  21839  cssincl  21868  pjdm  21887  dsmmval  21914  dsmmbas2  21917  dsmmelbas  21919  frlmbas  21935  frlmup1  21978  lindfind  21996  lindsind  21997  f1lindf  22002  islindf4  22018  psrbag  22097  psrbaglefi  22106  mplsubglem  22178  mpllsslem  22179  ltbwe  22225  psrbagsn  22244  subrgasclcl  22248  mplind  22251  mpfind  22296  psdmul  22359  coe1mul2lem2  22459  gsumply1eq  22499  evl1vsd  22534  mpfpf1  22541  pf1mpf  22542  pf1ind  22545  matecl  22612  m1detdiag  22784  mdetralt  22795  mdetralt2  22796  mdetunilem2  22800  mdetunilem9  22807  m2detleiblem3  22816  m2detleiblem4  22817  smadiadetlem0  22848  cpmatacl  22903  chpscmat  23029  uniopn  23084  inopn  23086  fiinopn  23088  istps  23121  fctop  23191  iscld  23214  isopn2  23219  mretopd  23279  iscldtop  23282  perfi  23342  tgrest  23346  restcld  23359  ordtbaslem  23375  ordtrest2lem  23390  ordtrest2  23391  iscn  23422  cnpval  23423  iscnp  23424  tgcn  23439  subbascn  23441  ssidcn  23442  lmbrf  23447  cnpnei  23451  cnima  23452  iscncl  23456  cnconst2  23470  cnrest2  23473  cnpresti  23475  cnprest  23476  cnindis  23479  lmres  23487  lmcnp  23491  iscnrm  23510  t1sncld  23513  cnrmi  23547  cncmp  23579  cmpsublem  23586  fiuncmp  23591  unconn  23616  conncompid  23618  conncompconn  23619  conncompss  23620  1stcfb  23632  2ndcrest  23641  2ndcctbss  23642  2ndcdisj  23643  1stccnp  23649  islly  23655  isnlly  23656  subislly  23668  restnlly  23669  restlly  23670  islly2  23671  hausllycmp  23681  cldllycmp  23682  dislly  23684  isptfin  23703  islocfin  23704  ptfinfin  23706  finlocfin  23707  dissnlocfin  23716  locfindis  23717  comppfsc  23719  kgenval  23722  elkgen  23723  kgeni  23724  cmpkgen  23738  1stckgenlem  23740  kgencn2  23744  ptpjpre1  23758  elpt  23759  elptr  23760  ptbasin  23764  xkobval  23773  xkoval  23774  xkoopn  23776  txbasval  23793  tx1cn  23796  tx2cn  23797  dfac14  23805  xkoccn  23806  txcnp  23807  ptcnplem  23808  txcnmpt  23811  txindislem  23820  txdis1cn  23822  txlly  23823  txnlly  23824  pthaus  23825  ptrescn  23826  hauseqlcld  23833  txlm  23835  tx2ndc  23838  txkgen  23839  xkoptsub  23841  xkopt  23842  xkoco1cn  23844  xkoco2cn  23845  xkococnlem  23846  xkococn  23847  cnmpt11  23850  cnmpt12  23854  cnmpt21  23858  cnmpt22  23861  cnmptkp  23867  cnmptk1p  23872  xkoinjcn  23874  txconn  23876  qtopval2  23883  elqtop  23884  idqtop  23893  qtopcld  23900  qtopeu  23903  qtoprest  23904  qtopomap  23905  qtopcmap  23906  ishmeo  23946  hmeoopn  23953  hmeocld  23954  ordthmeolem  23988  ptcmpfi  24000  elmptrab  24014  fgcl  24065  trfil2  24074  cfinfil  24080  uzrest  24084  ufilss  24092  trufil  24097  cfinufil  24115  ufinffr  24116  ufildr  24118  rnelfm  24140  flfcntr  24230  ptcmplem2  24240  ptcmplem3  24241  ptcmplem4  24242  ptcmplem5  24243  cnextfvval  24252  tmdcn2  24276  tmdmulg  24279  tmdgsum2  24283  symgtgp  24293  opnsubg  24295  clssubg  24296  tgpconncompeqg  24299  ghmcnp  24302  tgphaus  24304  tgpt0  24306  qustgpopn  24307  qustgplem  24308  tsmsgsum  24326  tsmssubm  24330  tsmsres  24331  tsmsf1o  24332  tsmsxplem1  24340  tsmsxplem2  24341  tsmsxp  24342  istrg  24351  istdrg  24353  istdrg2  24365  istlm  24372  istvc  24379  ustval  24390  ustincl  24395  ustdiag  24396  ustinvel  24397  ustexhalf  24398  ust0  24407  ucnima  24467  fmucndlem  24477  prdsdsf  24554  prdsxmet  24556  imasf1oxmet  24562  imasf1omet  24563  prdsxmslem2  24716  metustsym  24742  isnlm  24862  qtopbaslem  24945  xrtgioo  24994  reperflem  25006  fsumcn  25059  expcn  25061  xrhmeo  25135  cnllycmp  25145  bndth  25147  isclm  25253  lmhmclm  25276  lmmcvg  25450  fmcfil  25461  iscfil3  25462  iscau2  25466  iscau4  25468  iscmet3lem1  25480  iscmet3  25482  cfilres  25485  caussi  25486  equivcfil  25488  flimcfil  25503  bcthlem1  25513  isbn  25527  srabn  25549  ishl2  25559  cmslssbn  25561  cmscsscms  25562  minveclem3b  25617  ivthlem1  25640  ivthlem2  25641  ivthlem3  25642  ivth2  25644  ivthle  25645  ivthle2  25646  ivthicc  25647  ovolficcss  25658  ovolunlem1a  25685  ovolunlem1  25686  ovolfiniun  25690  ovoliunlem1  25691  ovoliunlem3  25693  ovoliun  25694  ovoliun2  25695  shft2rab  25697  ovolshftlem1  25698  sca2rab  25701  ovolscalem1  25702  mblsplit  25721  finiunmbl  25733  volun  25734  volfiniun  25736  voliunlem1  25739  voliunlem3  25741  iunmbl  25742  voliun  25743  volsup  25745  ioombl  25754  ioorcl  25766  vitalilem1  25797  vitalilem2  25798  vitalilem3  25799  vitalilem4  25800  vitali  25802  ismbf1  25813  mbfdm  25815  ismbf  25817  ismbfcn  25818  mbfima  25819  mbfimaicc  25820  ismbfcn2  25827  ismbfd  25828  ismbf2d  25829  mbfeqalem1  25830  mbfmax  25838  mbfposr  25841  mbfposb  25842  ismbf3d  25843  mbfimaopnlem  25844  mbfimaopn2  25846  cncombf  25847  isi1f  25863  i1fd  25870  itg1mulc  25893  mbfi1fseqlem4  25907  itg2lcl  25916  isibl  25954  iblitg  25957  iblcnlem1  25977  iblcnlem  25978  iblrelem  25980  iblpos  25982  itgeqa  26003  itgfsum  26016  itgabs  26024  limcvallem  26060  ellimc  26062  ellimc2  26066  limcmpt  26072  cnmptlimc  26079  dvbsss  26091  cpnfval  26121  elcpn  26123  dvmptfsum  26164  dvle  26196  dvfsumle  26210  dvfsumge  26211  dvfsumabs  26212  dvfsumrlimf  26214  dvfsumlem1  26215  dvfsumlem2  26216  dvfsumlem3  26217  dvfsumlem4  26218  dvfsumrlimge0  26219  dvfsumrlim  26220  dvfsumrlim2  26221  dvfsum2  26223  itgsubstlem  26237  itgsubst  26238  mdegcl  26256  deg1nn0clb  26277  isuc1p  26328  plyeq0lem  26397  plyco  26428  plycj  26464  plycjOLD  26466  dvply2g  26476  dvnply2  26478  plydivlem4  26487  fta1lem  26498  fta1  26499  elqaalem1  26510  elqaalem2  26511  elqaalem3  26512  elqaa  26513  ulmcau  26588  radcnv0  26609  radcnvlt1  26611  radcnvle  26613  pserdvlem2  26621  coseq1  26720  efeq1  26723  sinord  26729  efif1olem2  26738  efif1olem4  26740  lognegb  26785  logcj  26801  argimgt0  26807  logtayl  26855  2irrexpq  26926  root1eq1  26950  logrec  26958  2irrexpqALT  26995  angrteqvd  27001  angpieqvdlem  27023  atans  27125  atans2  27126  dmarea  27152  areambl  27153  rlimcnp  27160  rlimcnp2  27161  xrlimcnp  27163  harmonicbnd  27198  harmonicbnd2  27199  lgamcvglem  27234  wilthlem2  27263  wilth  27265  efnnfsumcl  27297  vmacl  27312  efvmacl  27314  efchtdvds  27353  sqff1o  27376  fsumdvdscom  27379  musumsum  27386  fsumdvdsmul  27389  fsumvma  27407  perfect  27425  dchrelbasd  27433  lgsval  27495  lgsval2lem  27501  lgsdir2lem4  27522  lgsdir2  27524  lgsqrlem1  27540  lgsdchr  27549  m1lgs  27582  2lgs  27601  mul2sq  27613  2sqlem6  27617  2sqblem  27625  2sq2  27627  rplogsumlem2  27679  dchrisumlema  27682  dchrisumlem2  27684  dchrisumlem3  27685  dchrvmasumlem2  27692  dchrvmasumlem3  27693  dchrisum0flblem2  27703  dchrisum0flb  27704  dchrisum0fno1  27705  ostthlem1  27821  nodmon  27844  noextendseq  27861  nodense  27886  madefi  28136  addsproplem1  28192  addsproplem3  28194  addsprop  28199  addsf  28205  addbdaylem  28240  negsproplem1  28251  negsproplem3  28253  negsprop  28258  negbdaylem  28279  mulsproplemcbv  28338  mulsproplem1  28339  mulsproplem10  28348  mulsprop  28353  addonbday  28502  noseqp1  28514  noseqind  28515  peano5n0s  28542  dfn0s2  28555  n0addscl  28567  n0mulscl  28568  n0bday  28575  onsfi  28579  n0s0m1  28585  n0subs  28586  n0p1nns  28594  dfnns2  28595  nn1m1nns  28597  oldfib  28600  zaddscl  28617  zmulscld  28620  elzn0s  28621  peano5uzs  28627  expscllem  28653  z12addscl  28700  z12shalf  28703  z12negsclb  28704  z12zsodd  28705  z12bdaylem  28707  z12bday  28708  bdayfin  28710  mirval  28962  perpneq  29024  isperp2  29025  isperp2d  29026  foot  29032  islnopp  29050  islnoppd  29051  outpasch  29067  hlpasch  29068  ishpg  29071  colopp  29081  colhp  29082  lmif  29124  islmib  29126  lmiinv  29131  trgcopy  29145  trgcopyeu  29147  acopyeu  29175  inaghl  29192  tgasa1  29205  f1otrgitv  29249  f1otrg  29250  isfusgr  29698  opfusgr  29703  fusgrfisbase  29708  fusgrfisstep  29709  nbupgrel  29725  nbumgrvtx  29726  nbusgreledg  29733  edgnbusgreu  29747  nb3grprlem1  29760  uvtxusgrel  29783  cusgredg  29804  cplgr2vpr  29813  cusgrexg  29824  usgredgsscusgredg  29839  fusgrn0degnn0  29879  rusgrnumwrdl2  29966  rgrx0ndm  29973  wlkcomp  30010  wlkdlem2  30061  clwlkcomp  30158  iswwlks  30215  wwlknllvtx  30225  0enwwlksnge1  30243  wlkiswwlks2lem5  30252  wwlksm1edg  30260  wwlksnred  30271  wwlksnext  30272  wwlksnextbi  30273  wwlksnredwwlkn  30274  wwlksnextfun  30277  wwlksnextinj  30278  wwlksnextsurj  30279  wwlksnextbij  30281  wwlksnfi  30285  wwlksnextproplem2  30289  wwlksnextprop  30291  2wlkdlem4  30307  rusgrnumwwlkl1  30350  rusgrnumwwlks  30356  isclwwlk  30365  clwwlk1loop  30369  clwwlkccatlem  30370  clwlkclwwlklem2a1  30373  clwlkclwwlklem2a4  30378  clwlkclwwlklem2a  30379  clwlkclwwlklem2  30381  clwlkclwwlklem3  30382  clwlkclwwlk  30383  clwlkclwwlk2  30384  clwwisshclwwslemlem  30394  clwwisshclwwslem  30395  clwwisshclwws  30396  clwwlknlbonbgr1  30420  clwwlkinwwlk  30421  clwwlkn1  30422  loopclwwlkn1b  30423  clwwlkn1loopb  30424  clwwlkn2  30425  clwwlkel  30427  clwwlkf  30428  clwwlkwwlksb  30435  clwwlkext2edg  30437  wwlksext2clwwlk  30438  wwlksubclwwlk  30439  eleclclwwlknlem2  30442  umgr2cwwk2dif  30445  s2elclwwlknon2  30485  clwwlknonwwlknonb  30487  clwwlknonex2lem2  30489  clwwlknonex2  30490  3wlkdlem4  30543  upgr3v3e3cycl  30561  upgr4cycl4dv4e  30566  eupth2lem2  30600  eulerpathpr  30621  1vwmgr  30657  3vfriswmgrlem  30658  3vfriswmgr  30659  3cyclfrgrrn1  30666  vdgn1frgrv2  30677  frgrncvvdeqlem3  30682  frgrncvvdeqlem8  30687  frgrncvvdeqlem9  30688  frgrwopregasn  30697  frgrwopregbsn  30698  frgrwopreglem5ALT  30703  frgr2wwlk1  30710  frgr2wwlkeqm  30712  fusgr2wsp2nb  30715  2clwwlk2clwwlklem  30727  extwwlkfabel  30734  nvvop  30991  isnvlem  30992  sspval  31105  nmorepnf  31150  phpar  31206  siilem2  31234  bnsscmcl  31250  ubthlem1  31252  shaddcl  31599  shmulcl  31600  hsn0elch  31630  hhssablo  31645  hhssnvt  31647  hhsssh  31651  shscl  31700  shintcl  31712  chintcl  31714  shincl  31763  chincl  31881  h1datomi  31963  chscllem2  32020  sumspansn  32031  spansncvi  32034  5oalem2  32037  5oalem3  32038  pjini  32081  pjjsi  32082  eigposi  32218  nmoprepnf  32249  nmfnrepnf  32262  dmadjrnb  32288  lnophmlem1  32398  lnophm  32401  nmcopex  32411  lnconi  32415  nmbdfnlb  32432  nmcfnex  32435  imaelshi  32440  rnbra  32489  leopg  32504  pjbdlni  32531  pjhmop  32532  hmopidmch  32535  pjclem4  32581  pj3si  32589  strlem1  32632  atssma  32760  atcv0eq  32761  atcv1  32762  atomli  32764  atcvatlem  32767  cdj3lem2a  32818  cdj3lem3a  32821  xppreima  33020  fmptcof2  33032  aciunf1lem  33037  funcnv4mpt  33043  1stpreimas  33081  f1od2  33094  fpwrelmapffslem  33107  xrofsup  33142  fzspl  33164  fzsplit3  33168  nnindf  33194  fprodex01  33199  fsumiunle  33203  indf1ofs  33216  gsumhashmul  33411  fzto1st  33447  fxpsubm  33516  fxpsubg  33517  fxpsubrg  33518  isslmd  33546  slmdlema  33547  elrgspnlem2  33587  elrgspnlem4  33589  rlocisunit  33620  subsdrg  33643  qusker  33693  0nellinds  33709  unitprodclb  33726  nsgmgclem  33744  nsgmgc  33745  nsgqusf1olem2  33747  elrspunidl  33760  opprlidlabs  33791  dfufd2lem  33863  psrbasfsupp  33925  selvply1rhmlemb  33933  mplidomlem  33941  lindsunlem  34038  brfldext  34059  brfinext  34066  finextfldext  34078  finexttrb  34079  extdg1id  34080  fldextrspunlsplem  34087  constrconj  34159  constrfin  34160  trisecnconstr  34206  smatrcl  34210  submateq  34223  lmatfval  34228  lmatcl  34230  qtophaus  34250  locfinreflem  34254  locfinref  34255  zartopn  34289  zarcmplem  34295  rhmpreimacnlem  34298  xpinpreima  34320  xpinpreima2  34321  cnre2csqlem  34324  tpr2rico  34326  prsdm  34328  prsrn  34329  ordtrest2NEWlem  34336  ordtrest2NEW  34337  zrhcntr  34393  qqhval2  34396  isrrext  34414  ismntoplly  34439  esumcvg  34500  sigaval  34525  issiga  34526  0elsiga  34528  sigaclcu  34531  issgon  34537  prsiga  34545  sigaclci  34546  difelsiga  34547  unelsiga  34548  ispisys2  34567  inelpisys  34568  unelldsys  34572  sigapildsyslem  34575  sigapildsys  34576  ldgenpisyslem1  34577  ldgenpisys  34580  isros  34582  unelros  34585  difelros  34586  fiunelros  34588  inelsros  34592  diffiunisros  34593  rossros  34594  measvuni  34628  measiun  34632  voliune  34643  volfiniune  34644  brfae  34662  ismbfm  34665  mbfmcnvima  34669  mbfmcst  34673  1stmbfm  34674  2ndmbfm  34675  imambfm  34676  sitgval  34746  issibf  34747  sibfima  34752  sitgfval  34755  sitgclg  34756  eulerpartlemelr  34771  eulerpartlemsf  34773  eulerpartleme  34777  eulerpartlemt0  34783  eulerpartlemt  34785  eulerpartgbij  34786  eulerpartlemr  34788  eulerpartlemmf  34789  eulerpartlemgvv  34790  eulerpartlemgs2  34794  eulerpartlemn  34795  eulerpart  34796  cndprobprob  34852  rrvsum  34868  orvcelel  34884  ballotlemodife  34912  ballotlemsdom  34926  ballotlemrv  34934  ballotlemrv1  34935  ballotlemrv2  34936  ballotlem1ri  34949  fsum2dsub  35018  reprinfz1  35033  reprpmtf1o  35037  reprdifc  35038  breprexplema  35041  hgt750lema  35068  hgt750leme  35069  bnj149  35287  bnj222  35295  bnj1112  35395  bnj1148  35408  fissorduni  35497  fineqvrep  35543  fineqvnttrclse  35553  fineqvinfep  35554  kardnnfi  35598  gblacfnacd  35602  vonf1wev  35608  vonf1owevOLD  35610  vonf1osev  35612  vonf1oonfo  35615  loop1cycl  35642  subfacp1lem3  35687  subfacp1lem6  35690  erdszelem10  35705  kur14  35721  cvxsconn  35748  cnllysconn  35750  resconn  35751  iscvm  35764  cvmliftlem5  35794  cvmliftlem15  35803  cvmlift2lem1  35807  cvmlift2lem12  35819  cvmlift2lem13  35820  sat1el2xp  35884  fmlasuc  35891  gonan0  35897  gonar  35900  satefvfmla0  35923  msubrn  36034  msubco  36036  ismfs  36054  mvtinf  36060  mclsax  36074  mppspstlem  36076  elmpps  36078  nnuni  36232  dfdm5  36278  dfrn5  36279  elima4  36281  rdgprc0  36296  pprodss4v  36387  elfuns  36418  fnimage  36432  imageval  36433  fwddifval  36667  fwddifnval  36668  fwddifnp1  36670  elhf2g  36681  hfun  36683  hfninf  36691  nmulprop  36695  filnetlem4  36925  onsucconn  36982  onsucsuccmp  36988  limsucncmp  36990  onint1  36993  fveleq  36995  findreccl  36997  nndivsub  37001  weiunse  37012  mh-inf3f1  37085  mh-infprim2bi  37091  mh-infprim3bi  37092  bj-seex  37590  bj-adjg1  37712  bj-mooreset  37777  bj-ismoored0  37781  bj-ismoored  37782  bj-inftyexpitaudisj  37882  bj-inftyexpidisj  37887  bj-isvec  37964  bj-isclm  37968  csbmpo123  38010  topdifinffinlem  38026  topdifinffin  38027  csbfinxpg  38067  phpreu  38288  finixpnum  38289  lindsenlbs  38299  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem22  38326  poimirlem23  38327  poimirlem24  38328  poimirlem25  38329  poimirlem26  38330  poimirlem28  38332  poimirlem29  38333  poimirlem30  38334  poimirlem31  38335  poimirlem32  38336  poimir  38337  mblfinlem3  38343  ex-ovoliunnfl  38347  voliunnfl  38348  volsupnfl  38349  mbfresfi  38350  itgabsnc  38373  ftc1anclem6  38382  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  dvasin  38388  sdclem2  38426  fdc  38429  incsequz  38432  neificl  38437  mettrifi  38441  cntotbnd  38480  cnpwstotbnd  38481  ismtyima  38487  ismtyhmeolem  38488  heiborlem2  38496  heiborlem3  38497  heiborlem4  38498  heiborlem5  38499  heiborlem6  38500  heiborlem10  38504  isrngo  38581  isdivrngo  38634  drngoi  38635  idlval  38697  isidlc  38699  idladdcl  38703  idllmulcl  38704  idlrmulcl  38705  0idl  38709  pridlval  38717  smprngopr  38736  prnc  38751  ispridlc  38754  pridlc  38755  eqrelf  38940  iss2  39026  elcoeleqvrels  39361  elfunsALTV  39459  eldisjs  39501  eleldisjs  39510  fsumshftd  39759  riotaclbgBAD  39761  renegclALT  39770  lshpinN  39796  isopos  39987  oposlem  39989  glbconN  40184  lnnat  40234  2at0mat0  40332  islvol2aN  40399  dalawlem13  40690  pclfinclN  40757  lhpoc2N  40822  ltrncnvatb  40945  cdleme11h  41073  cdlemefr32sn2aw  41211  cdlemefs32sn1aw  41221  cdleme32fvaw  41246  cdlemg1fvawlemN  41380  dicelvalN  41985  dih1dimatlem  42136  dihlatat  42144  dihjatcclem4  42228  islpolN  42290  lpolsatN  42295  lpolpolsatN  42296  mapdordlem1a  42441  mapdordlem1  42443  mapdhcl  42534  iscsrg  42771  fzsplitnd  42782  lcmineqlem12  42840  intlewftc  42861  dvrelogpow2b  42868  aks4d1p1p3  42869  aks4d1p1p2  42870  aks4d1p1p4  42871  dvle2  42872  aks4d1p8  42887  aks4d1p9  42888  isprimroot  42893  primrootsunit1  42897  primrootscoprmpow  42899  aks6d1c1p1  42907  aks6d1c1p2  42909  aks6d1c1p3  42910  evl1gprodd  42917  hashscontpow  42922  aks6d1c3  42923  aks6d1c2  42930  sticksstones1  42946  sticksstones10  42955  sticksstones11  42956  sticksstones12a  42957  aks6d1c6lem1  42970  unitscyglem5  42999  retire  43113  reelznn0nn  43268  fsuppind  43355  fsuppssindlem2  43357  fsuppssind  43358  isnacs3  43474  nacsfix  43476  mzpclval  43489  mzpcl1  43493  mzpcl2  43494  mzpcl34  43495  mzpexpmpt  43509  mzpsubst  43512  diophin  43536  diophun  43537  2rexfrabdioph  43556  3rexfrabdioph  43557  4rexfrabdioph  43558  6rexfrabdioph  43559  7rexfrabdioph  43560  rabdiophlem2  43562  diophren  43573  fphpd  43576  fphpdo  43577  fiphp3d  43579  pellexlem1  43589  pell14qrexpclnn0  43626  pellqrex  43639  rmspecnonsq  43667  monotuz  43701  monotoddzzfi  43702  monotoddzz  43703  oddcomabszz  43704  modabsdifz  43746  rmxdioph  43776  expdiophlem2  43782  limsuc2  43801  dfac11  43822  kelac1  43823  dfac21  43826  lsmfgcl  43834  islnm  43837  lnmlssfg  43840  lmhmfgima  43844  pwslnm  43854  unxpwdom3  43855  pwfi2f1o  43856  islnr  43871  hbtlem2  43884  cnsrexpcl  43925  flcidc  43930  mendlmod  43949  proot1ex  43956  oaordnr  44056  omnord1  44065  oenord1  44076  cantnfresb  44084  onmcl  44091  tfsnfin  44112  nadd2rabtr  44144  nadd1rabtr  44148  nadd1rabex  44150  nadd1suc  44152  pwelg  44319  fipjust  44324  elnonrel  44344  elinlem  44357  elcnvlem  44360  ss2iundf  44418  dfhe3  44534  dffrege115  44737  rfovcnvf1od  44763  ntrneiel2  44845  clsneiel2  44868  neicvgel2  44879  grur1cld  44989  dvgrat  45055  cvgdvgrat  45056  radcnvrat  45057  binomcxplemdvsum  45098  binomcxplemnotnn0  45099  orbitcl  45699  modelaxreplem1  45720  modelaxreplem2  45721  modelaxrep  45723  fnchoice  45782  fiiuncl  45818  disjf1  45934  disjinfi  45943  choicefi  45950  axccdom  45971  fmptf  45987  fmptff  46017  monoords  46049  supminfrnmpt  46192  supxrleubrnmptf  46198  supminfxr  46211  supminfxr2  46216  supminfxrrnmpt  46218  monoordxrv  46228  monoordxr  46229  monoord2xrv  46230  monoord2xr  46231  caucvgbf  46236  cvgcaule  46238  fsummulc1f  46320  fsumnncl  46321  fsumf1of  46323  fsumreclf  46325  fsumlessf  46326  fsumsermpt  46328  fmul01  46329  fmulcl  46330  fmuldfeqlem1  46331  fmuldfeq  46332  fmul01lt1lem1  46333  fmul01lt1lem2  46334  fprodexp  46343  fprodabs2  46344  mccllem  46346  mccl  46347  fprodcnlem  46348  fprodcn  46349  climmulf  46353  climsuse  46357  climrecf  46358  climaddf  46364  climf  46371  sumnnodd  46379  clim2f  46383  0ellimcdiv  46396  climsubmpt  46407  climreclf  46411  climf2  46413  fnlimcnv  46414  climeldmeqmpt  46415  clim2f2  46417  climfveqmpt  46418  fnlimfvre  46421  fnlimabslt  46426  climfveqmpt3  46429  climbddf  46434  climeldmeqmpt3  46436  climinf2mpt  46461  climinfmpt  46462  limsupequzmptf  46478  lmbr3  46494  liminfreuzlem  46549  coseq0  46611  cncfshift  46621  cncfperiod  46626  fprodcncf  46647  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  dvmptmulf  46684  dvnmptdivc  46685  dvnmul  46690  dvmptfprod  46692  iblspltprt  46720  itgspltprt  46726  stoweidlem2  46749  stoweidlem3  46750  stoweidlem4  46751  stoweidlem6  46753  stoweidlem8  46755  stoweidlem17  46764  stoweidlem19  46766  stoweidlem20  46767  stoweidlem21  46768  stoweidlem23  46770  stoweidlem27  46774  stoweidlem35  46782  stoweidlem42  46789  stoweidlem43  46790  stoweidlem62  46809  stoweid  46810  wallispilem3  46814  wallispi  46817  fourierdlem16  46870  fourierdlem21  46875  fourierdlem41  46895  fourierdlem42  46896  fourierdlem48  46901  fourierdlem49  46902  fourierdlem50  46903  fourierdlem51  46904  fourierdlem54  46907  fourierdlem63  46916  fourierdlem64  46917  fourierdlem65  46918  fourierdlem71  46924  fourierdlem72  46925  fourierdlem73  46926  fourierdlem83  46936  fourierdlem86  46939  fourierdlem89  46942  fourierdlem90  46943  fourierdlem91  46944  fourierdlem96  46949  fourierdlem97  46950  fourierdlem98  46951  fourierdlem99  46952  fourierdlem100  46953  fourierdlem103  46956  fourierdlem104  46957  fourierdlem105  46958  fourierdlem108  46961  fourierdlem109  46962  fourierdlem110  46963  fourierdlem112  46965  fourierdlem113  46966  etransclem24  47005  salunicl  47063  saluncl  47064  saldifcl  47066  sge0f1o  47129  sge0lempt  47157  sge0iunmptlemfi  47160  sge0p1  47161  sge0fodjrnlem  47163  sge0iunmpt  47165  sge0ltfirpmpt2  47173  sge0isummpt2  47179  sge0xaddlem2  47181  sge0xadd  47182  ismea  47198  nnfoctbdjlem  47202  nnfoctbdj  47203  meadjiun  47213  voliunsge0lem  47219  meaiuninclem  47227  meaiuninc3v  47231  hoidmvlelem2  47343  hoidmvlelem3  47344  vonvolmbl2  47410  hoimbl2  47412  vonhoire  47419  vonicclem2  47431  vonn0ioo2  47437  vonn0icc2  47439  salpreimagelt  47454  salpreimalegt  47456  salpreimagtge  47472  salpreimaltle  47473  issmf  47475  salpreimagtlt  47477  smfpreimalt  47478  smfpreimaltf  47483  issmfle  47492  smfpreimale  47501  issmfgt  47503  smfpreimagt  47509  issmfgelem  47516  issmfge  47517  smflimlem4  47521  smflim  47524  smfpreimage  47529  smfresal  47535  smfpimbor1lem1  47545  smfpimbor1lem2  47546  smflim2  47553  smflimmpt  47557  smflimsuplem1  47567  smflimsuplem2  47568  smflimsuplem3  47569  smflimsuplem5  47571  smflimsuplem7  47573  smflimsup  47575  smfliminf  47578  ormkglobd  47624  cjnpoly  47659  eu2ndop1stv  47895  dmfcoafv  47945  ffnaov  47969  faovcl  47970  funressndmafv2rn  47993  dfatdmfcoafv2  48024  mod2addne  48140  smonoord  48147  iccpartiltu  48204  iccpartigtl  48205  sprsymrelf1lem  48273  prproropf1olem2  48286  fmtno4prmfac193  48358  proththdlem  48398  proththd  48399  iseven  48426  isodd  48427  dfodd2  48434  evenm1odd  48437  evenp1odd  48438  enege  48443  onego  48444  epee  48503  perfectALTV  48521  bgoldbtbndlem2  48604  bgoldbtbndlem3  48605  bgoldbtbndlem4  48606  bgoldbtbnd  48607  clnbupgrel  48632  edgusgrclnbfin  48640  grimuhgr  48685  uhgrimedgi  48688  uhgrimprop  48690  isuspgrim0  48692  isuspgrimlem  48693  grimedg  48733  grtriproplem  48737  grtrif1o  48740  isgrtri  48741  grtriclwlk3  48743  cycl3grtrilem  48744  cycl3grtri  48745  grimgrtri  48747  usgrgrtrirex  48748  isubgr3stgrlem7  48770  grlimprclnbgrvtx  48797  grlimgredgex  48798  grlimgrtri  48801  usgrexmpl1tri  48823  gpgvtxel2  48846  gpgvtx0  48851  gpgvtx1  48852  gpgedgvtx0  48859  gpgedgvtx1  48860  gpgedgiov  48863  gpgedg2ov  48864  gpgedg2iv  48865  gpgnbgrvtx0  48872  gpgnbgrvtx1  48873  gpg3kgrtriex  48887  gpgprismgr4cycllem3  48895  pgnbgreunbgrlem1  48911  pgnbgreunbgrlem2lem1  48912  pgnbgreunbgrlem2lem2  48913  pgnbgreunbgrlem2lem3  48914  pgnbgreunbgrlem4  48917  pgnbgreunbgrlem5lem1  48918  pgnbgreunbgrlem5lem2  48919  pgnbgreunbgrlem5lem3  48920  pgnbgreunbgr  48923  grlimedgnedg  48929  uzlidlring  49033  smprngprmrng  49137  cbvmpox2  49149  lmod1  49305  nnolog2flm1  49403  dignn0flhalflem1  49428  catprsc  49824  nelsubc3lem  49881  fucofulem2  50122  fucofvalne  50136  isthincd2lem2  50246  euendfunc  50337  cnelsubclem  50414