Theorem eleq2s 2859

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816

This theorem is referenced by:  elrabi  3687  optocl  5780  ssrel  5792  eldmeldmressn  6043  predel  6342  fveqdmss  7098  oprabv  7493  elmpocl  7674  el2mpocsbcl  8110  bropopvvv  8115  bropfvvvv  8117  ressuppss  8208  mpoxeldm  8236  mpoxopn0yelv  8238  mpoxopxnop0  8240  tfr2a  8435  rdgseg  8462  2oconcl  8541  ecexr  8750  ectocld  8824  ecoptocl  8847  brecop2  8851  eroveu  8852  mapfvd  8919  mapsnconst  8932  mapfienlem1  9445  mapfienlem2  9446  mapfienlem3  9447  cantnflem2  9730  r1sucg  9809  r1suc  9810  acnrcl  10082  dfac5lem4  10166  dfac5lem4OLD  10168  fin23lem29  10381  fin23lem30  10382  axcclem  10497  alephval2  10612  0tsk  10795  0nsr  11119  peano2nn  12278  uzssz  12899  peano2uzs  12944  uzsupss  12982  fzssnn  13608  prednn0  13692  fzossnn0  13730  fldiv4p1lem1div2  13875  ltweuz  14002  fzennn  14009  ser1const  14099  expp1  14109  facnn  14314  facp1  14317  bcpasc  14360  hashfzo0  14469  tpfo  14539  ccatval2  14616  ccatass  14626  swrd00  14682  swrd0  14696  pfx00  14712  pfx0  14713  wrdeqs1cat  14758  splfv2a  14794  revccat  14804  rexuz3  15387  rexanuz2  15388  r19.2uz  15390  rexuzre  15391  cau4  15395  caubnd2  15396  climrlim2  15583  climshft2  15618  climaddc1  15671  climmulc2  15673  climsubc1  15674  climsubc2  15675  climlec2  15695  isercoll2  15705  climsup  15706  climcau  15707  caurcvg  15713  caurcvg2  15714  caucvg  15715  caucvgb  15716  iseraltlem1  15718  iseralt  15721  binomlem  15865  isumshft  15875  cvgrat  15919  clim2div  15925  ntrivcvg  15933  ntrivcvgtail  15936  fprodntriv  15978  fprodeq0  16011  fprodefsum  16131  pwp1fsum  16428  3prm  16731  phicl2  16805  phibndlem  16807  dfphi2  16811  crth  16815  vdwap0  17014  prmlem1a  17144  fvprif  17606  xpsfeq  17608  oppccofval  17759  homarcl2  18080  arwrcl  18089  pleval2i  18381  letsr  18638  gsumws1  18851  smndex1mndlem  18922  mulgnngsum  19097  mulgpropd  19134  psgnunilem2  19513  psgnprfval  19539  gexid  19599  efgmnvl  19732  efgrcl  19733  efgsval  19749  efgs1  19753  efgs1b  19754  frgpuptinv  19789  frgpup3lem  19795  lt6abl  19913  eldprd  20024  isunit  20373  isirred  20419  fldhmsubc  20786  abvrcl  20814  islss  20932  lbsss  21076  lbssp  21078  lbsind  21079  cssi  21702  thlle  21716  thlleOLD  21717  islbs4  21852  psrbagleadd1  21948  mpfrcl  22109  psr1basf  22203  coe1tm  22276  ply1frcl  22322  mavmulsolcl  22557  marepvcl  22575  1marepvmarrepid  22581  mdet0pr  22598  m2detleiblem1  22630  cramerimplem1  22689  cramerlem1  22693  chpscmat  22848  chpscmatgsumbin  22850  chpscmatgsummon  22851  ptpjpre1  23579  fin1aufil  23940  lmflf  24013  tsmsfbas  24136  xpsxmetlem  24389  xpsmet  24392  metustsym  24568  iscmet3lem3  25324  iscmet3lem1  25325  iscmet3lem2  25326  iscmet3  25327  rrxmvallem  25438  volsup  25591  opnmblALT  25638  itg1val  25718  tdeglem2  26100  ulmcaulem  26437  ulmcau  26438  ulmss  26440  pserdvlem2  26472  eff1olem  26590  logdmnrp  26683  dvlog2lem  26694  logtayl  26702  cxpcn3lem  26790  atancl  26924  atanval  26927  chp1  27210  ppiublem2  27247  lgsdir2lem2  27370  lgsdir2lem3  27371  lgsquadlem2  27425  2lgslem1b  27436  rplogsumlem1  27528  rplogsumlem2  27529  pntlemj  27647  nnne0s  28340  1vgrex  29019  edglnl  29160  usgredg2v  29244  umgrres1lem  29327  upgrres1  29330  nbupgrres  29381  clwlkwlk  29795  wwlksnextproplem1  29929  wwlksnextproplem2  29930  wwlksnextproplem3  29931  rusgrnumwwlkb0  29991  clwlkclwwlklem2a4  30016  eleclclwwlknlem1  30079  eleclclwwlknlem2  30080  erclwwlkneqlen  30087  erclwwlknref  30088  erclwwlknsym  30089  erclwwlkntr  30090  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  frgrnbnb  30312  frgrwopreglem4  30334  frgrwopreglem5  30340  frgrwopreg  30342  numclwlk1  30390  vciOLD  30580  axhcompl-zf  31017  mayete3i  31747  pj3lem1  32225  fzto1stfv1  33121  fzto1st  33123  fzto1stinvn  33124  psgnfzto1st  33125  rmfsupp2  33242  erler  33269  submat1n  33804  xrge0mulc1cn  33940  fiunelros  34175  elmbfmvol2  34269  fibp1  34403  rrvsum  34456  ballotlemfmpn  34497  reprsuc  34630  bnj529  34755  bnj923  34782  bnj570  34919  bnj594  34926  bnj1173  35016  bnj1256  35029  bnj1259  35030  bnj1296  35035  bnj1498  35075  subfacp1lem1  35184  kur14lem7  35217  sat1el2xp  35384  mvrsval  35510  mvrsfpw  35511  mrsubcv  35515  mrsubccat  35523  msubff  35535  msrid  35550  msubvrs  35565  mppsval  35577  divcnvlin  35733  iprodefisumlem  35740  iprodefisum  35741  faclimlem1  35743  onsucsuccmpi  36444  bj-opelresdm  37146  bj-inftyexpitaudisj  37206  bj-inftyexpidisj  37211  bj-ccinftydisj  37214  bj-elccinfty  37215  finixpnum  37612  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem29  37656  poimirlem30  37657  broucube  37661  volsupnfl  37672  dvasin  37711  dvacos  37712  sdclem2  37749  fdc  37752  heiborlem4  37821  heiborlem6  37823  smgrpismgmOLD  37869  mndoissmgrpOLD  37875  mndoisexid  37876  rngoueqz  37947  drngoi  37958  redvmptabs  42390  mhphflem  42606  prjspertr  42615  prjsperref  42616  prjspersym  42617  prjspreln0  42619  prjspvs  42620  prjsprellsp  42621  jm2.23  43008  wepwsolem  43054  omabs2  43345  omcl3g  43347  trclfvdecomr  43741  mnuprdlem1  44291  mnuprdlem2  44292  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  ssfiunibd  45321  climinf  45621  stoweidlem15  46030  fourierdlem66  46187  etransclem37  46286  smfsupmpt  46830  smfinfmpt  46834  smflimsuplem8  46842  eldmressn  47049  afvres  47184  ndmaovrcl  47216  minusmodnep2tmod  47355  sprsymrelfv  47481  fmtnofz04prm  47564  31prm  47584  uspgrimprop  47873  stgr0  47927  stgr1  47928  gpgedgel  48007  gpgvtx1  48009  2ltceilhalf  48015  gpgedgvtx1  48020  gpg5nbgrvtx13starlem2  48028  2zrngamnd  48163  2zrngacmnd  48164  2zrngagrp  48165  2zrngALT  48170  2zrngnmlid  48171  2zrngnmlid2  48173  fldhmsubcALTV  48249  lincvalsng  48333  snlindsntor  48388  lincresunit3lem2  48397  lincresunit3  48398  ldepsnlinc  48425  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  rrx2pnecoorneor  48636  rrx2linest  48663  rrx2linesl  48664  setc2othin  49113