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  1vgrex  28262  edglnl  28403  usgredg2v  28484  umgrres1lem  28567  upgrres1  28570  nbupgrres  28621  clwlkwlk  29032  wwlksnextproplem1  29163  wwlksnextproplem2  29164  wwlksnextproplem3  29165  rusgrnumwwlkb0  29225  clwlkclwwlklem2a4  29250  eleclclwwlknlem1  29313  eleclclwwlknlem2  29314  erclwwlkneqlen  29321  erclwwlknref  29322  erclwwlknsym  29323  erclwwlkntr  29324  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  frgrnbnb  29546  frgrwopreglem4  29568  frgrwopreglem5  29574  frgrwopreg  29576  numclwlk1  29624  vciOLD  29814  axhcompl-zf  30251  mayete3i  30981  pj3lem1  31459  fzto1stfv1  32260  fzto1st  32262  fzto1stinvn  32263  psgnfzto1st  32264  rmfsupp2  32387  submat1n  32785  xrge0mulc1cn  32921  fiunelros  33172  elmbfmvol2  33266  fibp1  33400  rrvsum  33453  ballotlemfmpn  33493  reprsuc  33627  bnj529  33752  bnj923  33779  bnj570  33916  bnj594  33923  bnj1173  34013  bnj1256  34026  bnj1259  34027  bnj1296  34032  bnj1498  34072  subfacp1lem1  34170  kur14lem7  34203  sat1el2xp  34370  mvrsval  34496  mvrsfpw  34497  mrsubcv  34501  mrsubccat  34509  msubff  34521  msrid  34536  msubvrs  34551  mppsval  34563  divcnvlin  34702  iprodefisumlem  34710  iprodefisum  34711  faclimlem1  34713  onsucsuccmpi  35328  bj-opelresdm  36026  bj-inftyexpitaudisj  36086  bj-inftyexpidisj  36091  bj-ccinftydisj  36094  bj-elccinfty  36095  finixpnum  36473  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem29  36517  poimirlem30  36518  broucube  36522  volsupnfl  36533  dvasin  36572  dvacos  36573  sdclem2  36610  fdc  36613  heiborlem4  36682  heiborlem6  36684  smgrpismgmOLD  36730  mndoissmgrpOLD  36736  mndoisexid  36737  rngoueqz  36808  drngoi  36819  mhphflem  41168  prjspertr  41347  prjsperref  41348  prjspersym  41349  prjspreln0  41351  prjspvs  41352  prjsprellsp  41353  jm2.23  41735  wepwsolem  41784  omabs2  42082  omcl3g  42084  trclfvdecomr  42479  mnuprdlem1  43031  mnuprdlem2  43032  binomcxplemdvbinom  43112  binomcxplemnotnn0  43115  ssfiunibd  44019  climinf  44322  stoweidlem15  44731  fourierdlem66  44888  etransclem37  44987  smfsupmpt  45531  smflimsuplem8  45543  eldmressn  45747  afvres  45880  ndmaovrcl  45912  sprsymrelfv  46162  fmtnofz04prm  46245  31prm  46265  2zrngamnd  46839  2zrngacmnd  46840  2zrngagrp  46841  2zrngALT  46846  2zrngnmlid  46847  2zrngnmlid2  46849  fldhmsubc  46982  fldhmsubcALTV  47000  lincvalsng  47097  snlindsntor  47152  lincresunit3lem2  47161  lincresunit3  47162  ldepsnlinc  47189  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  rrx2pnecoorneor  47401  rrx2linest  47428  rrx2linesl  47429  setc2othin  47676