Theorem eleq2s 2908

Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
eleq2s.1	⊢ (𝐴 ∈ 𝐵 → 𝜑)
eleq2s.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eleq2s	⊢ (𝐴 ∈ 𝐶 → 𝜑)

Proof of Theorem eleq2s

Step	Hyp	Ref	Expression
1		eleq2s.2	. . 3 ⊢ 𝐶 = 𝐵
2	1	eleq2i 2881	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐵)
3		eleq2s.1	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝜑)
4	2, 3	sylbi 220	1 ⊢ (𝐴 ∈ 𝐶 → 𝜑)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  elrabi  3623  optocl  5609  eldmeldmressn  5862  predel  6133  fveqdmss  6823  oprabv  7193  elmpocl  7367  el2mpocsbcl  7763  bropopvvv  7768  bropfvvvv  7770  ressuppss  7832  mpoxeldm  7860  mpoxopn0yelv  7862  mpoxopxnop0  7864  tfr2a  8014  rdgseg  8041  2oconcl  8111  ecexr  8277  ectocld  8347  ecoptocl  8370  brecop2  8374  eroveu  8375  mapfvd  8426  mapsnconst  8439  mapfienlem1  8852  mapfienlem2  8853  mapfienlem3  8854  cantnflem2  9137  r1sucg  9182  r1suc  9183  acnrcl  9453  dfac5lem4  9537  fin23lem29  9752  fin23lem30  9753  axcclem  9868  alephval2  9983  0tsk  10166  0nsr  10490  peano2nn  11637  uzssz  12252  peano2uzs  12290  uzsupss  12328  fzssnn  12946  prednn0  13026  fzossnn0  13063  fldiv4p1lem1div2  13200  ltweuz  13324  fzennn  13331  ser1const  13422  expp1  13432  facnn  13631  facp1  13634  bcpasc  13677  hashfzo0  13787  ccatval2  13923  ccatass  13933  swrd00  13997  swrd0  14011  pfx00  14027  pfx0  14028  wrdeqs1cat  14073  splfv2a  14109  revccat  14119  rexuz3  14700  rexanuz2  14701  r19.2uz  14703  rexuzre  14704  cau4  14708  caubnd2  14709  climrlim2  14896  climshft2  14931  climaddc1  14983  climmulc2  14985  climsubc1  14986  climsubc2  14987  climlec2  15007  isercoll2  15017  climsup  15018  climcau  15019  caurcvg  15025  caurcvg2  15026  caucvg  15027  caucvgb  15028  iseraltlem1  15030  iseralt  15033  binomlem  15176  isumshft  15186  cvgrat  15231  clim2div  15237  ntrivcvg  15245  ntrivcvgtail  15248  fprodntriv  15288  fprodeq0  15321  fprodefsum  15440  pwp1fsum  15732  3prm  16028  phicl2  16095  phibndlem  16097  dfphi2  16101  crth  16105  vdwap0  16302  prmlem1a  16432  fvprif  16826  xpsfeq  16828  oppccofval  16978  homarcl2  17287  arwrcl  17296  pleval2i  17566  letsr  17829  gsumws1  17994  smndex1mndlem  18066  mulgnngsum  18225  mulgpropd  18261  psgnunilem2  18615  psgnprfval  18641  gexid  18698  efgmnvl  18832  efgrcl  18833  efgsval  18849  efgs1  18853  efgs1b  18854  frgpuptinv  18889  frgpup3lem  18895  lt6abl  19008  eldprd  19119  isunit  19403  isirred  19445  abvrcl  19585  islss  19699  lbsss  19842  lbssp  19844  lbsind  19845  cssi  20373  thlle  20386  islbs4  20521  mpfrcl  20757  psr1basf  20830  coe1tm  20902  ply1frcl  20942  mavmulsolcl  21156  marepvcl  21174  1marepvmarrepid  21180  mdet0pr  21197  m2detleiblem1  21229  cramerimplem1  21288  cramerlem1  21292  chpscmat  21447  chpscmatgsumbin  21449  chpscmatgsummon  21450  ptpjpre1  22176  fin1aufil  22537  lmflf  22610  tsmsfbas  22733  xpsxmetlem  22986  xpsmet  22989  metustsym  23162  iscmet3lem3  23894  iscmet3lem1  23895  iscmet3lem2  23896  iscmet3  23897  rrxmvallem  24008  volsup  24160  opnmblALT  24207  itg1val  24287  tdeglem2  24662  ulmcaulem  24989  ulmcau  24990  ulmss  24992  pserdvlem2  25023  eff1olem  25140  logdmnrp  25232  dvlog2lem  25243  logtayl  25251  cxpcn3lem  25336  atancl  25467  atanval  25470  chp1  25752  ppiublem2  25787  lgsdir2lem2  25910  lgsdir2lem3  25911  lgsquadlem2  25965  2lgslem1b  25976  rplogsumlem1  26068  rplogsumlem2  26069  pntlemj  26187  1vgrex  26795  edglnl  26936  usgredg2v  27017  umgrres1lem  27100  upgrres1  27103  nbupgrres  27154  clwlkwlk  27564  wwlksnextproplem1  27695  wwlksnextproplem2  27696  wwlksnextproplem3  27697  rusgrnumwwlkb0  27757  clwlkclwwlklem2a4  27782  eleclclwwlknlem1  27845  eleclclwwlknlem2  27846  erclwwlkneqlen  27853  erclwwlknref  27854  erclwwlknsym  27855  erclwwlkntr  27856  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  frgrnbnb  28078  frgrwopreglem4  28100  frgrwopreglem5  28106  frgrwopreg  28108  numclwlk1  28156  vciOLD  28344  axhcompl-zf  28781  mayete3i  29511  pj3lem1  29989  fzto1stfv1  30793  fzto1st  30795  fzto1stinvn  30796  psgnfzto1st  30797  rmfsupp2  30917  submat1n  31158  xrge0mulc1cn  31294  fiunelros  31543  elmbfmvol2  31635  fibp1  31769  rrvsum  31822  ballotlemfmpn  31862  reprsuc  31996  bnj529  32122  bnj923  32149  bnj570  32287  bnj594  32294  bnj1173  32384  bnj1256  32397  bnj1259  32398  bnj1296  32403  bnj1498  32443  subfacp1lem1  32539  kur14lem7  32572  sat1el2xp  32739  mvrsval  32865  mvrsfpw  32866  mrsubcv  32870  mrsubccat  32878  msubff  32890  msrid  32905  msubvrs  32920  mppsval  32932  divcnvlin  33077  iprodefisumlem  33085  iprodefisum  33086  faclimlem1  33088  onsucsuccmpi  33904  bj-opelresdm  34560  bj-inftyexpitaudisj  34620  bj-inftyexpidisj  34625  bj-ccinftydisj  34628  bj-elccinfty  34629  finixpnum  35042  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem9  35066  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem29  35086  poimirlem30  35087  broucube  35091  volsupnfl  35102  dvasin  35141  dvacos  35142  sdclem2  35180  fdc  35183  heiborlem4  35252  heiborlem6  35254  smgrpismgmOLD  35300  mndoissmgrpOLD  35306  mndoisexid  35307  rngoueqz  35378  drngoi  35389  prjspertr  39599  prjsperref  39600  prjspersym  39601  prjspreln0  39603  prjspvs  39604  prjsprellsp  39605  jm2.23  39937  wepwsolem  39986  trclfvdecomr  40429  mnuprdlem1  40980  mnuprdlem2  40981  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  ssfiunibd  41941  climinf  42248  stoweidlem15  42657  fourierdlem66  42814  etransclem37  42913  smflimsuplem8  43458  eldmressn  43629  afvres  43728  ndmaovrcl  43760  sprsymrelfv  44011  fmtnofz04prm  44094  31prm  44114  2zrngamnd  44565  2zrngacmnd  44566  2zrngagrp  44567  2zrngALT  44572  2zrngnmlid  44573  2zrngnmlid2  44575  fldhmsubc  44708  fldhmsubcALTV  44726  lincvalsng  44825  snlindsntor  44880  lincresunit3lem2  44889  lincresunit3  44890  ldepsnlinc  44917  nn0sumshdiglemA  45033  nn0sumshdiglemB  45034  rrx2pnecoorneor  45129  rrx2linest  45156  rrx2linesl  45157