Theorem eleq2s 2844

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-clel 2803

This theorem is referenced by:  elrabi  3675  elrabiOLD  3676  optocl  5767  ssrel  5779  eldmeldmressn  6025  predel  6324  fveqdmss  7082  oprabv  7475  elmpocl  7657  el2mpocsbcl  8089  bropopvvv  8094  bropfvvvv  8096  ressuppss  8187  mpoxeldm  8216  mpoxopn0yelv  8218  mpoxopxnop0  8220  tfr2a  8415  rdgseg  8442  2oconcl  8523  ecexr  8729  ectocld  8803  ecoptocl  8826  brecop2  8830  eroveu  8831  mapfvd  8898  mapsnconst  8911  mapfienlem1  9439  mapfienlem2  9440  mapfienlem3  9441  cantnflem2  9724  r1sucg  9803  r1suc  9804  acnrcl  10076  dfac5lem4  10160  fin23lem29  10373  fin23lem30  10374  axcclem  10489  alephval2  10604  0tsk  10787  0nsr  11111  peano2nn  12268  uzssz  12887  peano2uzs  12930  uzsupss  12968  fzssnn  13591  prednn0  13671  fzossnn0  13709  fldiv4p1lem1div2  13847  ltweuz  13973  fzennn  13980  ser1const  14070  expp1  14080  facnn  14285  facp1  14288  bcpasc  14331  hashfzo0  14440  ccatval2  14579  ccatass  14589  swrd00  14645  swrd0  14659  pfx00  14675  pfx0  14676  wrdeqs1cat  14721  splfv2a  14757  revccat  14767  rexuz3  15346  rexanuz2  15347  r19.2uz  15349  rexuzre  15350  cau4  15354  caubnd2  15355  climrlim2  15542  climshft2  15577  climaddc1  15630  climmulc2  15632  climsubc1  15633  climsubc2  15634  climlec2  15656  isercoll2  15666  climsup  15667  climcau  15668  caurcvg  15674  caurcvg2  15675  caucvg  15676  caucvgb  15677  iseraltlem1  15679  iseralt  15682  binomlem  15826  isumshft  15836  cvgrat  15880  clim2div  15886  ntrivcvg  15894  ntrivcvgtail  15897  fprodntriv  15937  fprodeq0  15970  fprodefsum  16090  pwp1fsum  16386  3prm  16688  phicl2  16763  phibndlem  16765  dfphi2  16769  crth  16773  vdwap0  16971  prmlem1a  17102  fvprif  17569  xpsfeq  17571  oppccofval  17723  homarcl2  18050  arwrcl  18059  pleval2i  18354  letsr  18611  gsumws1  18821  smndex1mndlem  18892  mulgnngsum  19067  mulgpropd  19104  psgnunilem2  19487  psgnprfval  19513  gexid  19573  efgmnvl  19706  efgrcl  19707  efgsval  19723  efgs1  19727  efgs1b  19728  frgpuptinv  19763  frgpup3lem  19769  lt6abl  19887  eldprd  19998  isunit  20349  isirred  20395  fldhmsubc  20758  abvrcl  20786  islss  20905  lbsss  21049  lbssp  21051  lbsind  21052  cssi  21674  thlle  21688  thlleOLD  21689  islbs4  21824  psrbagleadd1  21927  mpfrcl  22094  psr1basf  22185  coe1tm  22258  ply1frcl  22304  mavmulsolcl  22539  marepvcl  22557  1marepvmarrepid  22563  mdet0pr  22580  m2detleiblem1  22612  cramerimplem1  22671  cramerlem1  22675  chpscmat  22830  chpscmatgsumbin  22832  chpscmatgsummon  22833  ptpjpre1  23561  fin1aufil  23922  lmflf  23995  tsmsfbas  24118  xpsxmetlem  24371  xpsmet  24374  metustsym  24550  iscmet3lem3  25304  iscmet3lem1  25305  iscmet3lem2  25306  iscmet3  25307  rrxmvallem  25418  volsup  25571  opnmblALT  25618  itg1val  25698  tdeglem2  26083  ulmcaulem  26418  ulmcau  26419  ulmss  26421  pserdvlem2  26453  eff1olem  26570  logdmnrp  26663  dvlog2lem  26674  logtayl  26682  cxpcn3lem  26770  atancl  26904  atanval  26907  chp1  27190  ppiublem2  27227  lgsdir2lem2  27350  lgsdir2lem3  27351  lgsquadlem2  27405  2lgslem1b  27416  rplogsumlem1  27508  rplogsumlem2  27509  pntlemj  27627  nnne0s  28303  1vgrex  28933  edglnl  29074  usgredg2v  29158  umgrres1lem  29241  upgrres1  29244  nbupgrres  29295  clwlkwlk  29707  wwlksnextproplem1  29838  wwlksnextproplem2  29839  wwlksnextproplem3  29840  rusgrnumwwlkb0  29900  clwlkclwwlklem2a4  29925  eleclclwwlknlem1  29988  eleclclwwlknlem2  29989  erclwwlkneqlen  29996  erclwwlknref  29997  erclwwlknsym  29998  erclwwlkntr  29999  hashecclwwlkn1  30005  umgrhashecclwwlk  30006  frgrnbnb  30221  frgrwopreglem4  30243  frgrwopreglem5  30249  frgrwopreg  30251  numclwlk1  30299  vciOLD  30489  axhcompl-zf  30926  mayete3i  31656  pj3lem1  32134  fzto1stfv1  32981  fzto1st  32983  fzto1stinvn  32984  psgnfzto1st  32985  rmfsupp2  33106  erler  33123  submat1n  33631  xrge0mulc1cn  33767  fiunelros  34018  elmbfmvol2  34112  fibp1  34246  rrvsum  34299  ballotlemfmpn  34339  reprsuc  34472  bnj529  34597  bnj923  34624  bnj570  34761  bnj594  34768  bnj1173  34858  bnj1256  34871  bnj1259  34872  bnj1296  34877  bnj1498  34917  subfacp1lem1  35018  kur14lem7  35051  sat1el2xp  35218  mvrsval  35344  mvrsfpw  35345  mrsubcv  35349  mrsubccat  35357  msubff  35369  msrid  35384  msubvrs  35399  mppsval  35411  divcnvlin  35566  iprodefisumlem  35573  iprodefisum  35574  faclimlem1  35576  onsucsuccmpi  36166  bj-opelresdm  36863  bj-inftyexpitaudisj  36923  bj-inftyexpidisj  36928  bj-ccinftydisj  36931  bj-elccinfty  36932  finixpnum  37317  poimirlem5  37337  poimirlem6  37338  poimirlem7  37339  poimirlem8  37340  poimirlem9  37341  poimirlem10  37342  poimirlem11  37343  poimirlem12  37344  poimirlem13  37345  poimirlem14  37346  poimirlem15  37347  poimirlem16  37348  poimirlem17  37349  poimirlem18  37350  poimirlem19  37351  poimirlem20  37352  poimirlem21  37353  poimirlem22  37354  poimirlem29  37361  poimirlem30  37362  broucube  37366  volsupnfl  37377  dvasin  37416  dvacos  37417  sdclem2  37454  fdc  37457  heiborlem4  37526  heiborlem6  37528  smgrpismgmOLD  37574  mndoissmgrpOLD  37580  mndoisexid  37581  rngoueqz  37652  drngoi  37663  mhphflem  42284  prjspertr  42293  prjsperref  42294  prjspersym  42295  prjspreln0  42297  prjspvs  42298  prjsprellsp  42299  jm2.23  42689  wepwsolem  42738  omabs2  43033  omcl3g  43035  trclfvdecomr  43430  mnuprdlem1  43981  mnuprdlem2  43982  binomcxplemdvbinom  44062  binomcxplemnotnn0  44065  ssfiunibd  44958  climinf  45261  stoweidlem15  45670  fourierdlem66  45827  etransclem37  45926  smfsupmpt  46470  smflimsuplem8  46482  eldmressn  46686  afvres  46819  ndmaovrcl  46851  sprsymrelfv  47100  fmtnofz04prm  47183  31prm  47203  uspgrimprop  47486  2zrngamnd  47658  2zrngacmnd  47659  2zrngagrp  47660  2zrngALT  47665  2zrngnmlid  47666  2zrngnmlid2  47668  fldhmsubcALTV  47744  lincvalsng  47833  snlindsntor  47888  lincresunit3lem2  47897  lincresunit3  47898  ldepsnlinc  47925  nn0sumshdiglemA  48041  nn0sumshdiglemB  48042  rrx2pnecoorneor  48137  rrx2linest  48164  rrx2linesl  48165  setc2othin  48411