Theorem eleq2s 2857

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  elrabi  3611  elrabiOLD  3612  optocl  5671  eldmeldmressn  5924  predel  6212  fveqdmss  6938  oprabv  7313  elmpocl  7489  el2mpocsbcl  7896  bropopvvv  7901  bropfvvvv  7903  ressuppss  7970  mpoxeldm  7998  mpoxopn0yelv  8000  mpoxopxnop0  8002  tfr2a  8197  rdgseg  8224  2oconcl  8295  ecexr  8461  ectocld  8531  ecoptocl  8554  brecop2  8558  eroveu  8559  mapfvd  8625  mapsnconst  8638  mapfienlem1  9094  mapfienlem2  9095  mapfienlem3  9096  cantnflem2  9378  r1sucg  9458  r1suc  9459  acnrcl  9729  dfac5lem4  9813  fin23lem29  10028  fin23lem30  10029  axcclem  10144  alephval2  10259  0tsk  10442  0nsr  10766  peano2nn  11915  uzssz  12532  peano2uzs  12571  uzsupss  12609  fzssnn  13229  prednn0  13309  fzossnn0  13346  fldiv4p1lem1div2  13483  ltweuz  13609  fzennn  13616  ser1const  13707  expp1  13717  facnn  13917  facp1  13920  bcpasc  13963  hashfzo0  14073  ccatval2  14211  ccatass  14221  swrd00  14285  swrd0  14299  pfx00  14315  pfx0  14316  wrdeqs1cat  14361  splfv2a  14397  revccat  14407  rexuz3  14988  rexanuz2  14989  r19.2uz  14991  rexuzre  14992  cau4  14996  caubnd2  14997  climrlim2  15184  climshft2  15219  climaddc1  15272  climmulc2  15274  climsubc1  15275  climsubc2  15276  climlec2  15298  isercoll2  15308  climsup  15309  climcau  15310  caurcvg  15316  caurcvg2  15317  caucvg  15318  caucvgb  15319  iseraltlem1  15321  iseralt  15324  binomlem  15469  isumshft  15479  cvgrat  15523  clim2div  15529  ntrivcvg  15537  ntrivcvgtail  15540  fprodntriv  15580  fprodeq0  15613  fprodefsum  15732  pwp1fsum  16028  3prm  16327  phicl2  16397  phibndlem  16399  dfphi2  16403  crth  16407  vdwap0  16605  prmlem1a  16736  fvprif  17189  xpsfeq  17191  oppccofval  17343  homarcl2  17666  arwrcl  17675  pleval2i  17969  letsr  18226  gsumws1  18391  smndex1mndlem  18463  mulgnngsum  18624  mulgpropd  18660  psgnunilem2  19018  psgnprfval  19044  gexid  19101  efgmnvl  19235  efgrcl  19236  efgsval  19252  efgs1  19256  efgs1b  19257  frgpuptinv  19292  frgpup3lem  19298  lt6abl  19411  eldprd  19522  isunit  19814  isirred  19856  abvrcl  19996  islss  20111  lbsss  20254  lbssp  20256  lbsind  20257  cssi  20801  thlle  20814  islbs4  20949  mpfrcl  21205  psr1basf  21282  coe1tm  21354  ply1frcl  21394  mavmulsolcl  21608  marepvcl  21626  1marepvmarrepid  21632  mdet0pr  21649  m2detleiblem1  21681  cramerimplem1  21740  cramerlem1  21744  chpscmat  21899  chpscmatgsumbin  21901  chpscmatgsummon  21902  ptpjpre1  22630  fin1aufil  22991  lmflf  23064  tsmsfbas  23187  xpsxmetlem  23440  xpsmet  23443  metustsym  23617  iscmet3lem3  24359  iscmet3lem1  24360  iscmet3lem2  24361  iscmet3  24362  rrxmvallem  24473  volsup  24625  opnmblALT  24672  itg1val  24752  tdeglem2  25131  ulmcaulem  25458  ulmcau  25459  ulmss  25461  pserdvlem2  25492  eff1olem  25609  logdmnrp  25701  dvlog2lem  25712  logtayl  25720  cxpcn3lem  25805  atancl  25936  atanval  25939  chp1  26221  ppiublem2  26256  lgsdir2lem2  26379  lgsdir2lem3  26380  lgsquadlem2  26434  2lgslem1b  26445  rplogsumlem1  26537  rplogsumlem2  26538  pntlemj  26656  1vgrex  27275  edglnl  27416  usgredg2v  27497  umgrres1lem  27580  upgrres1  27583  nbupgrres  27634  clwlkwlk  28044  wwlksnextproplem1  28175  wwlksnextproplem2  28176  wwlksnextproplem3  28177  rusgrnumwwlkb0  28237  clwlkclwwlklem2a4  28262  eleclclwwlknlem1  28325  eleclclwwlknlem2  28326  erclwwlkneqlen  28333  erclwwlknref  28334  erclwwlknsym  28335  erclwwlkntr  28336  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  frgrnbnb  28558  frgrwopreglem4  28580  frgrwopreglem5  28586  frgrwopreg  28588  numclwlk1  28636  vciOLD  28824  axhcompl-zf  29261  mayete3i  29991  pj3lem1  30469  fzto1stfv1  31270  fzto1st  31272  fzto1stinvn  31273  psgnfzto1st  31274  rmfsupp2  31394  submat1n  31657  xrge0mulc1cn  31793  fiunelros  32042  elmbfmvol2  32134  fibp1  32268  rrvsum  32321  ballotlemfmpn  32361  reprsuc  32495  bnj529  32621  bnj923  32648  bnj570  32785  bnj594  32792  bnj1173  32882  bnj1256  32895  bnj1259  32896  bnj1296  32901  bnj1498  32941  subfacp1lem1  33041  kur14lem7  33074  sat1el2xp  33241  mvrsval  33367  mvrsfpw  33368  mrsubcv  33372  mrsubccat  33380  msubff  33392  msrid  33407  msubvrs  33422  mppsval  33434  divcnvlin  33604  iprodefisumlem  33612  iprodefisum  33613  faclimlem1  33615  onsucsuccmpi  34559  bj-opelresdm  35243  bj-inftyexpitaudisj  35303  bj-inftyexpidisj  35308  bj-ccinftydisj  35311  bj-elccinfty  35312  finixpnum  35689  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem29  35733  poimirlem30  35734  broucube  35738  volsupnfl  35749  dvasin  35788  dvacos  35789  sdclem2  35827  fdc  35830  heiborlem4  35899  heiborlem6  35901  smgrpismgmOLD  35947  mndoissmgrpOLD  35953  mndoisexid  35954  rngoueqz  36025  drngoi  36036  mhphflem  40207  prjspertr  40365  prjsperref  40366  prjspersym  40367  prjspreln0  40369  prjspvs  40370  prjsprellsp  40371  jm2.23  40734  wepwsolem  40783  trclfvdecomr  41225  mnuprdlem1  41779  mnuprdlem2  41780  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  ssfiunibd  42738  climinf  43037  stoweidlem15  43446  fourierdlem66  43603  etransclem37  43702  smfsupmpt  44235  smflimsuplem8  44247  eldmressn  44418  afvres  44551  ndmaovrcl  44583  sprsymrelfv  44834  fmtnofz04prm  44917  31prm  44937  2zrngamnd  45387  2zrngacmnd  45388  2zrngagrp  45389  2zrngALT  45394  2zrngnmlid  45395  2zrngnmlid2  45397  fldhmsubc  45530  fldhmsubcALTV  45548  lincvalsng  45645  snlindsntor  45700  lincresunit3lem2  45709  lincresunit3  45710  ldepsnlinc  45737  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  rrx2pnecoorneor  45949  rrx2linest  45976  rrx2linesl  45977  setc2othin  46225