Theorem eleq1d 2897

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  eleq1  2900  eleq12d  2907  eqeltrd  2913  eqneltrd  2932  rspcimdv  3613  reuind  3744  sbcel2  4367  sbccsb2  4386  disjiun  5053  breq1  5069  breq2  5070  inex1g  5223  intex  5240  pwexg  5279  reusv2lem4  5302  reusv2  5304  reusv3  5306  rabxfrd  5318  snex  5332  prex  5333  opelopabsb  5417  csbmpt12  5444  pofun  5491  seex  5518  seinxp  5635  opabid2  5700  opeliunxp2  5709  elrn2g  5761  opeldmd  5775  opeldm  5776  elreldm  5805  elrn2  5821  elsnres  5892  iss  5903  elimasng  5955  unielrel  6125  funopg  6389  funimaexg  6440  brprcneu  6662  tz6.12f  6694  ndmfvrcl  6701  ssimaex  6748  dmfco  6757  fvmpti  6767  fvmpt3  6772  fvmptf  6789  fvmptss2  6793  respreima  6836  fvn0ssdmfun  6842  fvelrn  6844  ffnfvf  6883  ffvresb  6888  fmptco  6891  fmptcof  6892  fsn  6897  fsn2g  6900  fressnfv  6922  fvrnressn  6923  fvn0fvelrn  6925  fnex  6980  funfvima  6992  funfvima3  6998  f1mpt  7019  fliftfuns  7067  isoselem  7094  isowe2  7103  riotaclb  7155  ovrspc2v  7182  ffnov  7278  fovcl  7279  ovmpos  7298  ov2gf  7299  ovg  7313  funimassov  7325  oprssdm  7329  ndmovrcl  7334  caovclg  7340  elovmpo  7390  ofmpteq  7428  sorpsscmpl  7460  uniexg  7466  unexb  7471  abnexg  7478  difsnexi  7483  onint  7510  limsuc  7564  tfisi  7573  xpexr  7623  xpexcnv  7625  fnexALT  7652  fornex  7657  f1stres  7713  f2ndres  7714  xp1st  7721  xp2nd  7722  unielxp  7727  opiota  7757  fmpox  7765  offval22  7783  frxp  7820  fnse  7827  opeliunxp2f  7876  dftpos4  7911  fvmpocurryd  7937  undefnel2  7943  onnseq  7981  smoel  7997  smo11  8001  tfrlem8  8020  tfrlem9  8021  tfrlem15  8028  tfr2b  8032  tz7.44-2  8043  tz7.44-3  8044  oacl  8160  omcl  8161  oecl  8162  oaord1  8177  omordi  8192  oen0  8212  oeeui  8228  nnacl  8237  nnmcl  8238  nnecl  8239  nnmordi  8257  nnaordex  8264  omsmolem  8280  erexb  8314  qliftfuns  8384  ixpsnval  8464  elixp2  8465  resixp  8497  undifixp  8498  mptelixpg  8499  resixpfo  8500  elixpsn  8501  fundmen  8583  fopwdom  8625  disjen  8674  xpf1o  8679  unblem2  8771  xpfi  8789  fiint  8795  fnfi  8796  iunfi  8812  pwfi  8819  isfsupp  8837  fsuppun  8852  frnfsuppbi  8862  elfi2  8878  wdom2d  9044  ixpiunwdom  9055  dfom3  9110  cantnfvalf  9128  cantnflt  9135  cantnflem1  9152  r1fin  9202  tz9.12lem3  9218  ranksnb  9256  ranklim  9273  r1pw  9274  r1pwALT  9275  r1pwcl  9276  rankuni2b  9282  djuexb  9338  cardmin2  9427  infxpenc2lem1  9445  dfac8alem  9455  dfac8clem  9458  ac5num  9462  acni2  9472  acnlem  9474  alephon  9495  alephfplem3  9532  alephfplem4  9533  dfac4  9548  dfac5lem1  9549  dfac5lem5  9553  dfac2a  9555  dfac2b  9556  dfacacn  9567  dfac12lem2  9570  dfac12r  9572  dfac12k  9573  cofsmo  9691  cfsmolem  9692  isfin1a  9714  fin1ai  9715  isfin3  9718  infpssrlem3  9727  fin23lem7  9738  fin23lem11  9739  enfin2i  9743  isf34lem4  9799  fin1a2lem7  9828  hsmexlem9  9847  hsmexlem4  9851  hsmex  9854  axcc2lem  9858  axcc3  9860  axdc3lem2  9873  axcclem  9879  zornn0g  9927  ttukeylem3  9933  ttukeylem6  9936  ttukey2g  9938  brdom7disj  9953  brdom6disj  9954  fnct  9959  konigthlem  9990  axregndlem2  10025  axinfnd  10028  axacndlem5  10033  axacnd  10034  fpwwe2lem5  10056  fpwwe2lem13  10064  fpwwe  10068  pwfseqlem1  10080  pwfseqlem3  10082  pwfseqlem4a  10083  pwfseqlem4  10084  wununi  10128  wunpw  10129  wunpr  10131  wunr1om  10141  tskpw  10175  tskr1om  10189  inar1  10197  grupw  10217  grupr  10219  gruurn  10220  gruiun  10221  ingru  10237  grur1a  10241  grothomex  10251  grothac  10252  addnidpi  10323  indpi  10329  adderpq  10378  mulerpq  10379  addclprlem2  10439  mulclprlem  10441  distrlem4pr  10448  prlem934  10455  ltexprlem3  10460  ltexprlem4  10461  ltexprlem7  10464  ltexpri  10465  prlem936  10469  reclem2pr  10470  reclem3pr  10471  addclsr  10505  mulclsr  10506  supsrlem  10533  supsr  10534  axaddf  10567  axmulf  10568  axaddrcl  10574  axmulrcl  10576  renegcl  10949  negreb  10951  negn0  11069  negf1o  11070  ltord1  11166  leord1  11167  eqord1  11168  ltord2  11169  leord2  11170  eqord2  11171  negfi  11589  fiminreOLD  11590  infm3  11600  cju  11634  peano5nni  11641  peano2nn  11650  dfnn2  11651  nn1m1nn  11659  nnaddcl  11661  nnmulcl  11662  nnsub  11682  nndivtr  11685  un0addcl  11931  un0mulcl  11932  elnnnn0  11941  nn0sub  11948  frnnn0fsupp  11955  elz  11984  nnnegz  11985  elz2  12000  znegclb  12020  zaddcl  12023  nzadd  12031  zmulcl  12032  zneo  12066  nneo  12067  zeo  12069  peano5uzi  12072  zindd  12084  eluzsub  12275  uzp1  12280  uzaddcl  12305  ublbneg  12334  eqreznegel  12335  supminf  12336  zsupss  12338  qmulz  12352  qnegcl  12366  irradd  12373  irrmul  12374  xnn0xaddcl  12629  fzrev2  12972  injresinjlem  13158  negmod0  13247  om2uzuzi  13318  uzindi  13351  fsuppmapnn0ub  13364  mptnn0fsuppr  13368  seqexw  13386  seqcl2  13389  seqcl  13391  seqf  13392  monoord  13401  monoord2  13402  sermono  13403  seqsplit  13404  seqcaopr2  13407  seqid3  13415  seqhomo  13418  expcllem  13441  expcl2lem  13442  m1expcl2  13452  faccl  13644  facdiv  13648  facndiv  13649  bccmpl  13670  bccl  13683  focdmex  13712  hashclb  13720  hasheq0  13725  hashfn  13737  seqcoll  13823  opfi1uzind  13860  ccatalpha  13947  reuccatpfxs1lem  14108  reuccatpfxs1  14109  repswccat  14148  repswrevw  14149  2cshw  14175  2cshwcshw  14187  cshimadifsn  14191  cshco  14198  swrd2lsw  14314  wwlktovf  14320  wwlktovf1  14321  wwlktovfo  14322  wrd2f1tovbij  14324  shftlem  14427  shftf  14438  cjval  14461  cjth  14462  remim  14476  cnpart  14599  uzin2  14704  caubnd2  14717  sqreulem  14719  clim  14851  clim2  14861  lo1o12  14890  climrlim2  14904  lo1resb  14921  o1resb  14923  lo1eq  14925  climmpt2  14930  climshftlem  14931  rlimcld2  14935  climcn1  14948  climcn2  14949  o1dif  14986  iserex  15013  climub  15018  climserle  15019  isercoll  15024  climcau  15027  caurcvg2  15034  caucvgb  15036  summolem3  15071  summolem2a  15072  zsum  15075  fsum  15077  sumss2  15083  fsumcvg2  15084  fsumsplitf  15098  sumpr  15103  sumtp  15104  fsumm1  15106  fsum1p  15108  isummulc2  15117  fsum2dlem  15125  fsumcom2  15129  fsumshftm  15136  fsum0diag2  15138  fsumge1  15152  fsum00  15153  fsumabs  15156  telfsumo  15157  telfsumo2  15158  fsumparts  15161  fsumrlim  15166  fsumo1  15167  o1fsum  15168  fsumiun  15176  binomlem  15184  isumshft  15194  isum1p  15196  isumrpcl  15198  climcndslem1  15204  climcndslem2  15205  climcnds  15206  infcvgaux2i  15213  cvgrat  15239  mertens  15242  clim2prod  15244  prodfn0  15250  prodfrec  15251  prodfdiv  15252  ntrivcvgfvn0  15255  prodmolem3  15287  prodmolem2a  15288  zprod  15291  fprod  15295  prodss  15301  fprodser  15303  fprodm1  15321  fprod1p  15322  fprodm1s  15324  fprodp1s  15325  fprodabs  15328  fprodn0  15333  fprod2dlem  15334  fprodcnv  15337  fprodcom2  15338  fproddivf  15341  fprodsplitf  15342  fprodsplit1f  15344  bpolycl  15406  fprodefsum  15448  rpnnen2lem11  15577  mod2eq1n2dvds  15696  mulsucdiv2z  15702  zob  15708  nn0o1gt2  15732  nno  15733  nn0o  15734  divalglem7  15750  bitsf1  15795  sadcp1  15804  smupp1  15829  qnumdencl  16079  iserodd  16172  pcqcl  16193  pcxcl  16197  pcgcd1  16213  dvdsprmpweqle  16222  pcmpt  16228  pcmpt2  16229  pcmptdvds  16230  infpnlem2  16247  infpn2  16249  1arith  16263  elgz  16267  mul4sq  16290  4sqlem13  16293  4sqlem17  16297  4sqlem18  16298  4sqlem19  16299  vdwlem1  16317  vdwlem2  16318  vdwnn  16334  ramtcl2  16347  ramcl  16365  prmonn2  16375  prmodvdslcmf  16383  isstruct2  16493  wunress  16564  firest  16706  imasaddfnlem  16801  imasvscafn  16810  xpsfrnel2  16837  mreintcl  16866  ismred2  16874  mreexexlemd  16915  mreexexlem3d  16917  mreexexlem4d  16918  iscatd2  16952  catpropd  16979  subsubc  17123  isfunc  17134  fncnvimaeqv  17370  joindef  17614  joinval  17615  meetdef  17628  meetval  17629  oduclatb  17754  acsdrsel  17777  isacs4lem  17778  isacs5lem  17779  acsdrscl  17780  mgmsscl  17857  mgm1  17868  gsumvalx  17886  mndpropd  17936  issubm  17968  0subm  17982  insubm  17983  mhmima  17989  gsumwsubmcl  18001  gsumwspan  18011  symggrplem  18049  sursubmefmnd  18061  injsubmefmnd  18062  smndex1basss  18070  mulgsubcl  18242  issubg  18279  issubg2  18294  issubg4  18298  0subg  18304  isnsg  18307  isnsg2  18308  nsgbi  18309  isnsg3  18312  elnmz  18315  nmzbi  18316  nmzsubg  18317  eqgval  18329  eqgid  18332  cycsubgcl  18349  ghmrn  18371  ghmnsgima  18382  gass  18431  oppgsubg  18491  f1omvdconj  18574  symgfisg  18596  psgneldm  18631  odhash3  18701  sylow2blem2  18746  lsmsubm  18778  lsmsubg  18779  efgsf  18855  efgsdm  18856  efgs1b  18862  efgredlema  18866  eqgabl  18955  ablnsg  18967  cyggenod2  19004  gsumzaddlem  19041  gsummhm2  19059  gsum2dlem2  19091  gsum2d2lem  19093  gsumcom2  19095  dprdfeq0  19144  dprdsubg  19146  dprd2da  19164  ablfacrp  19188  pgpfac1lem3  19199  pgpfaclem1  19203  ablfaclem3  19209  ablfac2  19211  cycsubggenodd  19231  issrg  19257  srgfcl  19265  srgbinomlem4  19293  isring  19301  iscrng  19304  dvdsr  19396  irredrmul  19457  isrim0  19475  isdrngd  19527  issubrg  19535  issubrg2  19555  subrgpropd  19570  issdrg  19574  sdrgacs  19580  issrngd  19632  islmod  19638  lmodlema  19639  islmodd  19640  lmodprop2d  19696  rmodislmodlem  19701  rmodislmod  19702  lssset  19705  islssd  19707  lsscl  19714  lsslss  19733  lsspropd  19789  lmhmima  19819  lbsind  19852  lsmcl  19855  islvec  19876  lspsolvlem  19914  lspsolv  19915  lvecpropd  19939  isassa  20088  assapropd  20101  psrbag  20144  psrbaglefi  20152  psrbagconf1o  20154  mplsubglem  20214  mpllsslem  20215  ltbwe  20253  psrbagsn  20275  subrgasclcl  20279  mplind  20282  mpfind  20320  coe1mul2lem2  20436  gsumply1eq  20473  evl1vsd  20507  mpfpf1  20514  pf1mpf  20515  pf1ind  20518  xrsdsreclblem  20591  xrsdsreclb  20592  prmirred  20642  znunithash  20711  cofipsgn  20737  zrhpsgnelbas  20738  rzgrp  20767  isphl  20772  phllmhm  20776  ipcl  20777  isphld  20798  phlpropd  20799  phlssphl  20803  cssincl  20832  pjdm  20851  dsmmval  20878  dsmmbas2  20881  dsmmelbas  20883  frlmbas  20899  frlmup1  20942  lindfind  20960  lindsind  20961  f1lindf  20966  islindf4  20982  matecl  21034  m1detdiag  21206  mdetralt  21217  mdetralt2  21218  mdetunilem2  21222  mdetunilem9  21229  m2detleiblem3  21238  m2detleiblem4  21239  smadiadetlem0  21270  cpmatacl  21324  chpscmat  21450  uniopn  21505  inopn  21507  fiinopn  21509  istps  21542  fctop  21612  iscld  21635  isopn2  21640  mretopd  21700  iscldtop  21703  perfi  21763  tgrest  21767  restcld  21780  ordtbaslem  21796  ordtrest2lem  21811  ordtrest2  21812  iscn  21843  cnpval  21844  iscnp  21845  tgcn  21860  subbascn  21862  ssidcn  21863  lmbrf  21868  cnpnei  21872  cnima  21873  iscncl  21877  cnconst2  21891  cnrest2  21894  cnpresti  21896  cnprest  21897  cnindis  21900  lmres  21908  lmcnp  21912  iscnrm  21931  t1sncld  21934  cnrmi  21968  cncmp  22000  cmpsublem  22007  fiuncmp  22012  unconn  22037  conncompid  22039  conncompconn  22040  conncompss  22041  1stcfb  22053  2ndcrest  22062  2ndcctbss  22063  2ndcdisj  22064  1stccnp  22070  islly  22076  isnlly  22077  subislly  22089  restnlly  22090  restlly  22091  islly2  22092  hausllycmp  22102  cldllycmp  22103  dislly  22105  isptfin  22124  islocfin  22125  ptfinfin  22127  finlocfin  22128  dissnlocfin  22137  locfindis  22138  comppfsc  22140  kgenval  22143  elkgen  22144  kgeni  22145  cmpkgen  22159  1stckgenlem  22161  kgencn2  22165  ptpjpre1  22179  elpt  22180  elptr  22181  ptbasin  22185  xkobval  22194  xkoval  22195  xkoopn  22197  txbasval  22214  tx1cn  22217  tx2cn  22218  dfac14  22226  xkoccn  22227  txcnp  22228  ptcnplem  22229  txcnmpt  22232  txindislem  22241  txdis1cn  22243  txlly  22244  txnlly  22245  pthaus  22246  ptrescn  22247  hauseqlcld  22254  txlm  22256  tx2ndc  22259  txkgen  22260  xkoptsub  22262  xkopt  22263  xkoco1cn  22265  xkoco2cn  22266  xkococnlem  22267  xkococn  22268  cnmpt11  22271  cnmpt12  22275  cnmpt21  22279  cnmpt22  22282  cnmptkp  22288  cnmptk1p  22293  xkoinjcn  22295  txconn  22297  qtopval2  22304  elqtop  22305  idqtop  22314  qtopcld  22321  qtopeu  22324  qtoprest  22325  qtopomap  22326  qtopcmap  22327  ishmeo  22367  hmeoopn  22374  hmeocld  22375  ordthmeolem  22409  ptcmpfi  22421  elmptrab  22435  fgcl  22486  trfil2  22495  cfinfil  22501  uzrest  22505  ufilss  22513  trufil  22518  cfinufil  22536  ufinffr  22537  ufildr  22539  rnelfm  22561  flfcntr  22651  ptcmplem2  22661  ptcmplem3  22662  ptcmplem4  22663  ptcmplem5  22664  cnextfvval  22673  tmdcn2  22697  tmdmulg  22700  tmdgsum2  22704  symgtgp  22714  opnsubg  22716  clssubg  22717  tgpconncompeqg  22720  ghmcnp  22723  tgphaus  22725  tgpt0  22727  qustgpopn  22728  qustgplem  22729  tsmsgsum  22747  tsmssubm  22751  tsmsres  22752  tsmsf1o  22753  tsmsxplem1  22761  tsmsxplem2  22762  tsmsxp  22763  istrg  22772  istdrg  22774  istdrg2  22786  istlm  22793  istvc  22800  ustval  22811  ustincl  22816  ustdiag  22817  ustinvel  22818  ustexhalf  22819  ust0  22828  ucnima  22890  fmucndlem  22900  prdsdsf  22977  prdsxmet  22979  imasf1oxmet  22985  imasf1omet  22986  prdsxmslem2  23139  metustsym  23165  isnlm  23284  qtopbaslem  23367  xrtgioo  23414  reperflem  23426  fsumcn  23478  expcn  23480  xrhmeo  23550  cnllycmp  23560  bndth  23562  isclm  23668  lmhmclm  23691  lmmcvg  23864  fmcfil  23875  iscfil3  23876  iscau2  23880  iscau4  23882  iscmet3lem1  23894  iscmet3  23896  cfilres  23899  caussi  23900  equivcfil  23902  flimcfil  23917  bcthlem1  23927  isbn  23941  srabn  23963  ishl2  23973  cmslssbn  23975  cmscsscms  23976  minveclem3b  24031  ivthlem1  24052  ivthlem2  24053  ivthlem3  24054  ivth2  24056  ivthle  24057  ivthle2  24058  ivthicc  24059  ovolficcss  24070  ovolunlem1a  24097  ovolunlem1  24098  ovolfiniun  24102  ovoliunlem1  24103  ovoliunlem3  24105  ovoliun  24106  ovoliun2  24107  shft2rab  24109  ovolshftlem1  24110  sca2rab  24113  ovolscalem1  24114  mblsplit  24133  finiunmbl  24145  volun  24146  volfiniun  24148  voliunlem1  24151  voliunlem3  24153  iunmbl  24154  voliun  24155  volsup  24157  ioombl  24166  ioorcl  24178  vitalilem1  24209  vitalilem2  24210  vitalilem3  24211  vitalilem4  24212  vitali  24214  ismbf1  24225  mbfdm  24227  ismbf  24229  ismbfcn  24230  mbfima  24231  mbfimaicc  24232  ismbfcn2  24239  ismbfd  24240  ismbf2d  24241  mbfeqalem1  24242  mbfmax  24250  mbfposr  24253  mbfposb  24254  ismbf3d  24255  mbfimaopnlem  24256  mbfimaopn2  24258  cncombf  24259  isi1f  24275  i1fd  24282  itg1mulc  24305  mbfi1fseqlem4  24319  itg2lcl  24328  isibl  24366  iblitg  24369  iblcnlem1  24388  iblcnlem  24389  iblrelem  24391  iblpos  24393  itgeqa  24414  itgfsum  24427  itgabs  24435  limcvallem  24469  ellimc  24471  ellimc2  24475  limcmpt  24481  cnmptlimc  24488  dvbsss  24500  cpnfval  24529  elcpn  24531  dvmptfsum  24572  dvle  24604  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  dvfsumrlimf  24622  dvfsumlem1  24623  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumlem4  24626  dvfsumrlimge0  24627  dvfsumrlim  24628  dvfsumrlim2  24629  dvfsum2  24631  itgsubstlem  24645  itgsubst  24646  mdegcl  24663  deg1nn0clb  24684  isuc1p  24734  plyeq0lem  24800  plyco  24831  plycj  24867  dvnply2  24876  plydivlem4  24885  fta1lem  24896  fta1  24897  elqaalem1  24908  elqaalem2  24909  elqaalem3  24910  elqaa  24911  ulmcau  24983  radcnv0  25004  radcnvlt1  25006  radcnvle  25008  pserdvlem2  25016  coseq1  25110  efeq1  25113  sinord  25118  efif1olem2  25127  efif1olem4  25129  lognegb  25173  logcj  25189  argimgt0  25195  logtayl  25243  2irrexpq  25313  root1eq1  25336  logrec  25341  2irrexpqALT  25378  angrteqvd  25384  angpieqvdlem  25406  atans  25508  atans2  25509  dmarea  25535  areambl  25536  rlimcnp  25543  rlimcnp2  25544  xrlimcnp  25546  harmonicbnd  25581  harmonicbnd2  25582  lgamcvglem  25617  wilthlem2  25646  wilth  25648  efnnfsumcl  25680  vmacl  25695  efvmacl  25697  efchtdvds  25736  sqff1o  25759  fsumdvdscom  25762  musumsum  25769  fsumdvdsmul  25772  fsumvma  25789  perfect  25807  dchrelbasd  25815  lgsval  25877  lgsval2lem  25883  lgsdir2lem4  25904  lgsdir2  25906  lgsqrlem1  25922  lgsdchr  25931  m1lgs  25964  2lgs  25983  mul2sq  25995  2sqlem6  25999  2sqblem  26007  2sq2  26009  rplogsumlem2  26061  dchrisumlema  26064  dchrisumlem2  26066  dchrisumlem3  26067  dchrvmasumlem2  26074  dchrvmasumlem3  26075  dchrisum0flblem2  26085  dchrisum0flb  26086  dchrisum0fno1  26087  ostthlem1  26203  mirval  26441  perpneq  26500  isperp2  26501  isperp2d  26502  foot  26508  islnopp  26525  islnoppd  26526  outpasch  26541  hlpasch  26542  ishpg  26545  colopp  26555  colhp  26556  lmif  26571  islmib  26573  lmiinv  26578  trgcopy  26590  trgcopyeu  26592  acopyeu  26620  inaghl  26631  tgasa1  26644  f1otrgitv  26656  f1otrg  26657  isfusgr  27100  opfusgr  27105  fusgrfisbase  27110  fusgrfisstep  27111  nbupgrel  27127  nbumgrvtx  27128  nbusgreledg  27135  edgnbusgreu  27149  nb3grprlem1  27162  uvtxusgrel  27185  cusgredg  27206  cplgr2vpr  27215  cusgrexg  27226  usgredgsscusgredg  27241  fusgrn0degnn0  27281  rusgrnumwrdl2  27368  rgrx0ndm  27375  wlkcomp  27412  wlkdlem2  27465  clwlkcomp  27560  iswwlks  27614  wwlknllvtx  27624  0enwwlksnge1  27642  wlkiswwlks2lem5  27651  wwlksm1edg  27659  wwlksnred  27670  wwlksnext  27671  wwlksnextbi  27672  wwlksnredwwlkn  27673  wwlksnextfun  27676  wwlksnextinj  27677  wwlksnextsurj  27678  wwlksnextbij  27680  wwlksnfi  27684  wwlksnextproplem2  27689  wwlksnextprop  27691  2wlkdlem4  27707  rusgrnumwwlkl1  27747  rusgrnumwwlks  27753  isclwwlk  27762  clwwlk1loop  27766  clwwlkccatlem  27767  clwlkclwwlklem2a1  27770  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwlkclwwlklem3  27779  clwlkclwwlk  27780  clwlkclwwlk2  27781  clwwisshclwwslemlem  27791  clwwisshclwwslem  27792  clwwisshclwws  27793  clwwlknlbonbgr1  27817  clwwlkinwwlk  27818  clwwlkn1  27819  loopclwwlkn1b  27820  clwwlkn1loopb  27821  clwwlkn2  27822  clwwlkel  27825  clwwlkf  27826  clwwlkwwlksb  27833  clwwlkext2edg  27835  wwlksext2clwwlk  27836  wwlksubclwwlk  27837  eleclclwwlknlem2  27840  umgr2cwwk2dif  27843  s2elclwwlknon2  27883  clwwlknonwwlknonb  27885  clwwlknonex2lem2  27887  clwwlknonex2  27888  3wlkdlem4  27941  upgr3v3e3cycl  27959  upgr4cycl4dv4e  27964  eupth2lem2  27998  eulerpathpr  28019  1vwmgr  28055  3vfriswmgrlem  28056  3vfriswmgr  28057  3cyclfrgrrn1  28064  vdgn1frgrv2  28075  frgrncvvdeqlem3  28080  frgrncvvdeqlem8  28085  frgrncvvdeqlem9  28086  frgrwopregasn  28095  frgrwopregbsn  28096  frgrwopreglem5ALT  28101  frgr2wwlk1  28108  frgr2wwlkeqm  28110  fusgr2wsp2nb  28113  2clwwlk2clwwlklem  28125  extwwlkfabel  28132  nvvop  28386  isnvlem  28387  sspval  28500  nmorepnf  28545  phpar  28601  siilem2  28629  bnsscmcl  28645  ubthlem1  28647  shaddcl  28994  shmulcl  28995  hsn0elch  29025  hhssablo  29040  hhssnvt  29042  hhsssh  29046  shscl  29095  shintcl  29107  chintcl  29109  shincl  29158  chincl  29276  h1datomi  29358  chscllem2  29415  sumspansn  29426  spansncvi  29429  5oalem2  29432  5oalem3  29433  pjini  29476  pjjsi  29477  eigposi  29613  nmoprepnf  29644  nmfnrepnf  29657  dmadjrnb  29683  lnophmlem1  29793  lnophm  29796  nmcopex  29806  lnconi  29810  nmbdfnlb  29827  nmcfnex  29830  imaelshi  29835  rnbra  29884  leopg  29899  pjbdlni  29926  pjhmop  29927  hmopidmch  29930  pjclem4  29976  pj3si  29984  strlem1  30027  atssma  30155  atcv0eq  30156  atcv1  30157  atomli  30159  atcvatlem  30162  cdj3lem2a  30213  cdj3lem3a  30216  fovcld  30385  xppreima  30394  fmptcof2  30402  aciunf1lem  30407  funcnv4mpt  30414  1stpreimas  30441  f1od2  30457  fpwrelmapffslem  30468  xrofsup  30492  fzspl  30513  fzsplit3  30517  nnindf  30535  fprodex01  30541  fsumiunle  30545  fzto1st  30745  isslmd  30830  slmdlema  30831  qusker  30918  0nellinds  30935  prmidlval  30954  prmidlc  30964  lindsunlem  31020  brfldext  31037  brfinext  31043  finexttrb  31052  extdg1id  31053  smatrcl  31061  submateq  31074  lmatfval  31079  lmatcl  31081  qtophaus  31100  locfinreflem  31104  locfinref  31105  xpinpreima  31149  xpinpreima2  31150  cnre2csqlem  31153  tpr2rico  31155  prsdm  31157  prsrn  31158  ordtrest2NEWlem  31165  ordtrest2NEW  31166  qqhval2  31223  isrrext  31241  ismntoplly  31266  indfval  31275  indf1ofs  31285  esumcvg  31345  sigaval  31370  issiga  31371  0elsiga  31373  sigaclcu  31376  issgon  31382  prsiga  31390  sigaclci  31391  difelsiga  31392  unelsiga  31393  ispisys2  31412  unelldsys  31417  sigapildsyslem  31420  sigapildsys  31421  ldgenpisyslem1  31422  ldgenpisys  31425  isros  31427  unelros  31430  difelros  31431  fiunelros  31433  inelsros  31437  diffiunisros  31438  rossros  31439  measvuni  31473  measiun  31477  voliune  31488  volfiniune  31489  brfae  31507  ismbfm  31510  mbfmcnvima  31515  mbfmcst  31517  1stmbfm  31518  2ndmbfm  31519  imambfm  31520  sitgval  31590  issibf  31591  sibfima  31596  sitgfval  31599  sitgclg  31600  eulerpartlemelr  31615  eulerpartlemsf  31617  eulerpartleme  31621  eulerpartlemt0  31627  eulerpartlemt  31629  eulerpartgbij  31630  eulerpartlemr  31632  eulerpartlemmf  31633  eulerpartlemgvv  31634  eulerpartlemgs2  31638  eulerpartlemn  31639  eulerpart  31640  cndprobprob  31696  rrvsum  31712  orvcelel  31727  ballotlemodife  31755  ballotlemsdom  31769  ballotlemrv  31777  ballotlemrv1  31778  ballotlemrv2  31779  ballotlem1ri  31792  fsum2dsub  31878  reprinfz1  31893  reprpmtf1o  31897  reprdifc  31898  breprexplema  31901  hgt750lema  31928  hgt750leme  31929  bnj149  32147  bnj222  32155  bnj1112  32255  bnj1148  32268  loop1cycl  32384  subfacp1lem3  32429  subfacp1lem6  32432  erdszelem10  32447  kur14  32463  cvxsconn  32490  cnllysconn  32492  resconn  32493  iscvm  32506  cvmliftlem5  32536  cvmliftlem15  32545  cvmlift2lem1  32549  cvmlift2lem12  32561  cvmlift2lem13  32562  sat1el2xp  32626  fmlasuc  32633  gonan0  32639  gonar  32642  satefvfmla0  32665  msubrn  32776  msubco  32778  ismfs  32796  mvtinf  32802  mclsax  32816  mppspstlem  32818  elmpps  32820  dfdm5  33016  dfrn5  33017  elima4  33019  rdgprc0  33038  nodmon  33157  noextendseq  33174  nodense  33196  pprodss4v  33345  elfuns  33376  fnimage  33390  imageval  33391  fwddifval  33623  fwddifnval  33624  fwddifnp1  33626  elhf2g  33637  hfun  33639  hfninf  33647  filnetlem4  33729  onsucconn  33786  onsucsuccmp  33792  limsucncmp  33794  onint1  33797  fveleq  33799  findreccl  33801  nndivsub  33805  bj-seex  34244  bj-mooreset  34397  bj-ismoored0  34401  bj-ismoored  34402  bj-inftyexpitaudisj  34490  bj-inftyexpidisj  34495  bj-isvec  34572  bj-isclm  34575  csbmpo123  34615  topdifinffinlem  34631  topdifinffin  34632  csbfinxpg  34672  phpreu  34891  finixpnum  34892  lindsenlbs  34902  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem28  34935  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  poimir  34940  mblfinlem3  34946  ex-ovoliunnfl  34950  voliunnfl  34951  volsupnfl  34952  mbfresfi  34953  itgabsnc  34976  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  dvasin  34993  sdclem2  35032  fdc  35035  incsequz  35038  neificl  35043  mettrifi  35047  cntotbnd  35089  cnpwstotbnd  35090  ismtyima  35096  ismtyhmeolem  35097  heiborlem2  35105  heiborlem3  35106  heiborlem4  35107  heiborlem5  35108  heiborlem6  35109  heiborlem10  35113  isrngo  35190  isdivrngo  35243  drngoi  35244  idlval  35306  isidlc  35308  idladdcl  35312  idllmulcl  35313  idlrmulcl  35314  0idl  35318  pridlval  35326  smprngopr  35345  prnc  35360  ispridlc  35363  pridlc  35364  eqrelf  35532  ecex2  35600  imaexALTV  35602  iss2  35616  elcoeleqvrels  35845  elfunsALTV  35940  eldisjs  35970  eleldisjs  35976  fsumshftd  36103  riotaclbgBAD  36105  renegclALT  36114  lshpinN  36140  isopos  36331  oposlem  36333  glbconN  36528  lnnat  36578  2at0mat0  36676  islvol2aN  36743  dalawlem13  37034  pclfinclN  37101  lhpoc2N  37166  ltrncnvatb  37289  cdleme11h  37417  cdlemefr32sn2aw  37555  cdlemefs32sn1aw  37565  cdleme32fvaw  37590  cdlemg1fvawlemN  37724  dicelvalN  38329  dih1dimatlem  38480  dihlatat  38488  dihjatcclem4  38572  islpolN  38634  lpolsatN  38639  lpolpolsatN  38640  mapdordlem1a  38785  mapdordlem1  38787  mapdhcl  38878  lmhmlvec  39168  isnacs3  39327  nacsfix  39329  mzpclval  39342  mzpcl1  39346  mzpcl2  39347  mzpcl34  39348  mzpexpmpt  39362  mzpsubst  39365  diophin  39389  diophun  39390  2rexfrabdioph  39413  3rexfrabdioph  39414  4rexfrabdioph  39415  6rexfrabdioph  39416  7rexfrabdioph  39417  rabdiophlem2  39419  diophren  39430  fphpd  39433  fphpdo  39434  fiphp3d  39436  pellexlem1  39446  pell14qrexpclnn0  39483  pellqrex  39496  rmspecnonsq  39524  monotuz  39558  monotoddzzfi  39559  monotoddzz  39560  oddcomabszz  39561  modabsdifz  39603  rmxdioph  39633  expdiophlem2  39639  limsuc2  39661  dfac11  39682  kelac1  39683  dfac21  39686  lsmfgcl  39694  islnm  39697  lnmlssfg  39700  lmhmfgima  39704  pwslnm  39714  unxpwdom3  39715  pwfi2f1o  39716  islnr  39731  hbtlem2  39744  cnsrexpcl  39785  flcidc  39794  mendlmod  39813  proot1ex  39821  pwelg  39939  fipjust  39944  elnonrel  39965  elinlem  39978  elcnvlem  39981  ss2iundf  40024  dfhe3  40141  dffrege115  40344  rfovcnvf1od  40370  ntrneiel2  40456  clsneiel2  40479  neicvgel2  40490  grur1cld  40588  dvgrat  40664  cvgdvgrat  40665  radcnvrat  40666  binomcxplemdvsum  40707  binomcxplemnotnn0  40708  fnchoice  41306  fiiuncl  41347  disjf1  41463  disjinfi  41474  choicefi  41483  axccdom  41507  fmptf  41529  monoords  41584  supminfrnmpt  41739  supxrleubrnmptf  41747  supminfxr  41760  supminfxr2  41765  supminfxrrnmpt  41767  monoordxrv  41778  monoordxr  41779  monoord2xrv  41780  monoord2xr  41781  fsumclf  41870  fsummulc1f  41871  fsumnncl  41872  fsumsplit1  41873  fsumf1of  41875  fsumreclf  41877  fsumlessf  41878  fsumsermpt  41880  fmul01  41881  fmulcl  41882  fmuldfeqlem1  41883  fmuldfeq  41884  fmul01lt1lem1  41885  fmul01lt1lem2  41886  fprodexp  41895  fprodabs2  41896  mccllem  41898  mccl  41899  fprodcnlem  41900  fprodcn  41901  climmulf  41905  climsuse  41909  climrecf  41910  climaddf  41916  climf  41923  sumnnodd  41931  clim2f  41937  0ellimcdiv  41950  climsubmpt  41961  climreclf  41965  climf2  41967  fnlimcnv  41968  climeldmeqmpt  41969  clim2f2  41971  climfveqmpt  41972  fnlimfvre  41975  fnlimabslt  41980  climfveqmpt3  41983  climbddf  41988  climeldmeqmpt3  41990  climinf2mpt  42015  climinfmpt  42016  limsupequzmptf  42032  lmbr3  42048  liminfreuzlem  42103  coseq0  42165  cncfshift  42177  cncfperiod  42182  fprodcncf  42204  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvmptmulf  42242  dvnmptdivc  42243  dvnmul  42248  dvmptfprod  42250  iblspltprt  42278  itgspltprt  42284  stoweidlem2  42307  stoweidlem3  42308  stoweidlem4  42309  stoweidlem6  42311  stoweidlem8  42313  stoweidlem17  42322  stoweidlem19  42324  stoweidlem20  42325  stoweidlem21  42326  stoweidlem23  42328  stoweidlem27  42332  stoweidlem35  42340  stoweidlem42  42347  stoweidlem43  42348  stoweidlem62  42367  stoweid  42368  wallispilem3  42372  wallispi  42375  fourierdlem16  42428  fourierdlem21  42433  fourierdlem41  42453  fourierdlem42  42454  fourierdlem48  42459  fourierdlem49  42460  fourierdlem50  42461  fourierdlem51  42462  fourierdlem54  42465  fourierdlem63  42474  fourierdlem64  42475  fourierdlem65  42476  fourierdlem71  42482  fourierdlem72  42483  fourierdlem73  42484  fourierdlem83  42494  fourierdlem86  42497  fourierdlem89  42500  fourierdlem90  42501  fourierdlem91  42502  fourierdlem96  42507  fourierdlem97  42508  fourierdlem98  42509  fourierdlem99  42510  fourierdlem100  42511  fourierdlem103  42514  fourierdlem104  42515  fourierdlem105  42516  fourierdlem108  42519  fourierdlem109  42520  fourierdlem110  42521  fourierdlem112  42523  fourierdlem113  42524  etransclem24  42563  salunicl  42621  saluncl  42622  saldifcl  42624  sge0f1o  42684  sge0lempt  42712  sge0iunmptlemfi  42715  sge0p1  42716  sge0fodjrnlem  42718  sge0iunmpt  42720  sge0ltfirpmpt2  42728  sge0isummpt2  42734  sge0xaddlem2  42736  sge0xadd  42737  ismea  42753  nnfoctbdjlem  42757  nnfoctbdj  42758  meadjiun  42768  voliunsge0lem  42774  meaiuninclem  42782  meaiuninc3v  42786  hoidmvlelem2  42898  hoidmvlelem3  42899  vonvolmbl2  42965  hoimbl2  42967  vonhoire  42974  vonicclem2  42986  vonn0ioo2  42992  vonn0icc2  42994  salpreimagelt  43006  salpreimalegt  43008  salpreimagtge  43022  salpreimaltle  43023  issmf  43025  salpreimagtlt  43027  smfpreimalt  43028  smfpreimaltf  43033  issmfle  43042  smfpreimale  43051  issmfgt  43053  smfpreimagt  43058  issmfgelem  43065  issmfge  43066  smflimlem4  43070  smflim  43073  smfpreimage  43078  smfresal  43083  smfpimbor1lem1  43093  smfpimbor1lem2  43094  smflim2  43100  smflimmpt  43104  smflimsuplem1  43114  smflimsuplem2  43115  smflimsuplem3  43116  smflimsuplem5  43118  smflimsuplem7  43120  smflimsup  43122  smfliminf  43125  eu2ndop1stv  43344  dmfcoafv  43394  ffnaov  43418  faovcl  43419  funressndmafv2rn  43442  dfatdmfcoafv2  43473  smonoord  43551  iccpartiltu  43602  iccpartigtl  43603  sprsymrelf1lem  43673  prproropf1olem2  43686  fmtno4prmfac193  43755  proththdlem  43798  proththd  43799  iseven  43813  isodd  43814  dfodd2  43821  evenm1odd  43824  evenp1odd  43825  enege  43830  onego  43831  epee  43890  perfectALTV  43908  bgoldbtbndlem2  43991  bgoldbtbndlem3  43992  bgoldbtbndlem4  43993  bgoldbtbnd  43994  isomuspgrlem1  44012  isomuspgrlem2b  44014  isomuspgrlem2d  44016  mgmpropd  44062  issubmgm  44076  issubmgm2  44077  mgmhmima  44089  inclfusubc  44158  isrng  44167  isrngisom  44187  lidlmmgm  44216  uzlidlring  44220  cbvmpox2  44404  lmod1  44567  nnolog2flm1  44670  dignn0flhalflem1  44695