Theorem eleq2s 2852

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 2826	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐵)
3		eleq2s.1	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝜑)
4	2, 3	sylbi 216	1 ⊢ (𝐴 ∈ 𝐶 → 𝜑)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  elrabi  3678  elrabiOLD  3679  optocl  5771  ssrel  5783  eldmeldmressn  6026  predel  6322  fveqdmss  7081  oprabv  7469  elmpocl  7648  el2mpocsbcl  8071  bropopvvv  8076  bropfvvvv  8078  ressuppss  8168  mpoxeldm  8196  mpoxopn0yelv  8198  mpoxopxnop0  8200  tfr2a  8395  rdgseg  8422  2oconcl  8503  ecexr  8708  ectocld  8778  ecoptocl  8801  brecop2  8805  eroveu  8806  mapfvd  8873  mapsnconst  8886  mapfienlem1  9400  mapfienlem2  9401  mapfienlem3  9402  cantnflem2  9685  r1sucg  9764  r1suc  9765  acnrcl  10037  dfac5lem4  10121  fin23lem29  10336  fin23lem30  10337  axcclem  10452  alephval2  10567  0tsk  10750  0nsr  11074  peano2nn  12224  uzssz  12843  peano2uzs  12886  uzsupss  12924  fzssnn  13545  prednn0  13625  fzossnn0  13663  fldiv4p1lem1div2  13800  ltweuz  13926  fzennn  13933  ser1const  14024  expp1  14034  facnn  14235  facp1  14238  bcpasc  14281  hashfzo0  14390  ccatval2  14528  ccatass  14538  swrd00  14594  swrd0  14608  pfx00  14624  pfx0  14625  wrdeqs1cat  14670  splfv2a  14706  revccat  14716  rexuz3  15295  rexanuz2  15296  r19.2uz  15298  rexuzre  15299  cau4  15303  caubnd2  15304  climrlim2  15491  climshft2  15526  climaddc1  15579  climmulc2  15581  climsubc1  15582  climsubc2  15583  climlec2  15605  isercoll2  15615  climsup  15616  climcau  15617  caurcvg  15623  caurcvg2  15624  caucvg  15625  caucvgb  15626  iseraltlem1  15628  iseralt  15631  binomlem  15775  isumshft  15785  cvgrat  15829  clim2div  15835  ntrivcvg  15843  ntrivcvgtail  15846  fprodntriv  15886  fprodeq0  15919  fprodefsum  16038  pwp1fsum  16334  3prm  16631  phicl2  16701  phibndlem  16703  dfphi2  16707  crth  16711  vdwap0  16909  prmlem1a  17040  fvprif  17507  xpsfeq  17509  oppccofval  17661  homarcl2  17985  arwrcl  17994  pleval2i  18289  letsr  18546  gsumws1  18719  smndex1mndlem  18790  mulgnngsum  18959  mulgpropd  18996  psgnunilem2  19363  psgnprfval  19389  gexid  19449  efgmnvl  19582  efgrcl  19583  efgsval  19599  efgs1  19603  efgs1b  19604  frgpuptinv  19639  frgpup3lem  19645  lt6abl  19763  eldprd  19874  isunit  20187  isirred  20233  abvrcl  20429  islss  20545  lbsss  20688  lbssp  20690  lbsind  20691  cssi  21237  thlle  21251  thlleOLD  21252  islbs4  21387  mpfrcl  21648  psr1basf  21725  coe1tm  21795  ply1frcl  21837  mavmulsolcl  22053  marepvcl  22071  1marepvmarrepid  22077  mdet0pr  22094  m2detleiblem1  22126  cramerimplem1  22185  cramerlem1  22189  chpscmat  22344  chpscmatgsumbin  22346  chpscmatgsummon  22347  ptpjpre1  23075  fin1aufil  23436  lmflf  23509  tsmsfbas  23632  xpsxmetlem  23885  xpsmet  23888  metustsym  24064  iscmet3lem3  24807  iscmet3lem1  24808  iscmet3lem2  24809  iscmet3  24810  rrxmvallem  24921  volsup  25073  opnmblALT  25120  itg1val  25200  tdeglem2  25579  ulmcaulem  25906  ulmcau  25907  ulmss  25909  pserdvlem2  25940  eff1olem  26057  logdmnrp  26149  dvlog2lem  26160  logtayl  26168  cxpcn3lem  26255  atancl  26386  atanval  26389  chp1  26671  ppiublem2  26706  lgsdir2lem2  26829  lgsdir2lem3  26830  lgsquadlem2  26884  2lgslem1b  26895  rplogsumlem1  26987  rplogsumlem2  26988  pntlemj  27106  peano2n0s  27704  1vgrex  28293  edglnl  28434  usgredg2v  28515  umgrres1lem  28598  upgrres1  28601  nbupgrres  28652  clwlkwlk  29063  wwlksnextproplem1  29194  wwlksnextproplem2  29195  wwlksnextproplem3  29196  rusgrnumwwlkb0  29256  clwlkclwwlklem2a4  29281  eleclclwwlknlem1  29344  eleclclwwlknlem2  29345  erclwwlkneqlen  29352  erclwwlknref  29353  erclwwlknsym  29354  erclwwlkntr  29355  hashecclwwlkn1  29361  umgrhashecclwwlk  29362  frgrnbnb  29577  frgrwopreglem4  29599  frgrwopreglem5  29605  frgrwopreg  29607  numclwlk1  29655  vciOLD  29845  axhcompl-zf  30282  mayete3i  31012  pj3lem1  31490  fzto1stfv1  32291  fzto1st  32293  fzto1stinvn  32294  psgnfzto1st  32295  rmfsupp2  32418  submat1n  32816  xrge0mulc1cn  32952  fiunelros  33203  elmbfmvol2  33297  fibp1  33431  rrvsum  33484  ballotlemfmpn  33524  reprsuc  33658  bnj529  33783  bnj923  33810  bnj570  33947  bnj594  33954  bnj1173  34044  bnj1256  34057  bnj1259  34058  bnj1296  34063  bnj1498  34103  subfacp1lem1  34201  kur14lem7  34234  sat1el2xp  34401  mvrsval  34527  mvrsfpw  34528  mrsubcv  34532  mrsubccat  34540  msubff  34552  msrid  34567  msubvrs  34582  mppsval  34594  divcnvlin  34733  iprodefisumlem  34741  iprodefisum  34742  faclimlem1  34744  onsucsuccmpi  35376  bj-opelresdm  36074  bj-inftyexpitaudisj  36134  bj-inftyexpidisj  36139  bj-ccinftydisj  36142  bj-elccinfty  36143  finixpnum  36521  poimirlem5  36541  poimirlem6  36542  poimirlem7  36543  poimirlem8  36544  poimirlem9  36545  poimirlem10  36546  poimirlem11  36547  poimirlem12  36548  poimirlem13  36549  poimirlem14  36550  poimirlem15  36551  poimirlem16  36552  poimirlem17  36553  poimirlem18  36554  poimirlem19  36555  poimirlem20  36556  poimirlem21  36557  poimirlem22  36558  poimirlem29  36565  poimirlem30  36566  broucube  36570  volsupnfl  36581  dvasin  36620  dvacos  36621  sdclem2  36658  fdc  36661  heiborlem4  36730  heiborlem6  36732  smgrpismgmOLD  36778  mndoissmgrpOLD  36784  mndoisexid  36785  rngoueqz  36856  drngoi  36867  mhphflem  41216  prjspertr  41395  prjsperref  41396  prjspersym  41397  prjspreln0  41399  prjspvs  41400  prjsprellsp  41401  jm2.23  41783  wepwsolem  41832  omabs2  42130  omcl3g  42132  trclfvdecomr  42527  mnuprdlem1  43079  mnuprdlem2  43080  binomcxplemdvbinom  43160  binomcxplemnotnn0  43163  ssfiunibd  44067  climinf  44370  stoweidlem15  44779  fourierdlem66  44936  etransclem37  45035  smfsupmpt  45579  smflimsuplem8  45591  eldmressn  45795  afvres  45928  ndmaovrcl  45960  sprsymrelfv  46210  fmtnofz04prm  46293  31prm  46313  2zrngamnd  46887  2zrngacmnd  46888  2zrngagrp  46889  2zrngALT  46894  2zrngnmlid  46895  2zrngnmlid2  46897  fldhmsubc  47030  fldhmsubcALTV  47048  lincvalsng  47145  snlindsntor  47200  lincresunit3lem2  47209  lincresunit3  47210  ldepsnlinc  47237  nn0sumshdiglemA  47353  nn0sumshdiglemB  47354  rrx2pnecoorneor  47449  rrx2linest  47476  rrx2linesl  47477  setc2othin  47724