Theorem eleq2s 2847

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  elrabi  3657  optocl  5736  ssrel  5748  eldmeldmressn  5999  predel  6297  fveqdmss  7053  oprabv  7452  elmpocl  7633  el2mpocsbcl  8067  bropopvvv  8072  bropfvvvv  8074  ressuppss  8165  mpoxeldm  8193  mpoxopn0yelv  8195  mpoxopxnop0  8197  tfr2a  8366  rdgseg  8393  2oconcl  8470  ecexr  8679  ectocld  8758  ecoptocl  8783  brecop2  8787  eroveu  8788  mapfvd  8855  mapsnconst  8868  mapfienlem1  9363  mapfienlem2  9364  mapfienlem3  9365  cantnflem2  9650  r1sucg  9729  r1suc  9730  acnrcl  10002  dfac5lem4  10086  dfac5lem4OLD  10088  fin23lem29  10301  fin23lem30  10302  axcclem  10417  alephval2  10532  0tsk  10715  0nsr  11039  peano2nn  12205  uzssz  12821  peano2uzs  12868  uzsupss  12906  fzssnn  13536  prednn0  13620  fzossnn0  13658  fldiv4p1lem1div2  13804  modaddid  13879  ltweuz  13933  fzennn  13940  ser1const  14030  expp1  14040  facnn  14247  facp1  14250  bcpasc  14293  hashfzo0  14402  tpfo  14472  ccatval2  14550  ccatass  14560  swrd00  14616  swrd0  14630  pfx00  14646  pfx0  14647  wrdeqs1cat  14692  splfv2a  14728  revccat  14738  rexuz3  15322  rexanuz2  15323  r19.2uz  15325  rexuzre  15326  cau4  15330  caubnd2  15331  climrlim2  15520  climshft2  15555  climaddc1  15608  climmulc2  15610  climsubc1  15611  climsubc2  15612  climlec2  15632  isercoll2  15642  climsup  15643  climcau  15644  caurcvg  15650  caurcvg2  15651  caucvg  15652  caucvgb  15653  iseraltlem1  15655  iseralt  15658  binomlem  15802  isumshft  15812  cvgrat  15856  clim2div  15862  ntrivcvg  15870  ntrivcvgtail  15873  fprodntriv  15915  fprodeq0  15948  fprodefsum  16068  pwp1fsum  16368  3prm  16671  phicl2  16745  phibndlem  16747  dfphi2  16751  crth  16755  vdwap0  16954  prmlem1a  17084  fvprif  17531  xpsfeq  17533  oppccofval  17684  homarcl2  18004  arwrcl  18013  pleval2i  18302  letsr  18559  gsumws1  18772  smndex1mndlem  18843  mulgnngsum  19018  mulgpropd  19055  psgnunilem2  19432  psgnprfval  19458  gexid  19518  efgmnvl  19651  efgrcl  19652  efgsval  19668  efgs1  19672  efgs1b  19673  frgpuptinv  19708  frgpup3lem  19714  lt6abl  19832  eldprd  19943  isunit  20289  isirred  20335  fldhmsubc  20701  abvrcl  20729  islss  20847  lbsss  20991  lbssp  20993  lbsind  20994  cssi  21600  thlle  21613  islbs4  21748  psrbagleadd1  21844  mpfrcl  21999  psr1basf  22093  coe1tm  22166  ply1frcl  22212  mavmulsolcl  22445  marepvcl  22463  1marepvmarrepid  22469  mdet0pr  22486  m2detleiblem1  22518  cramerimplem1  22577  cramerlem1  22581  chpscmat  22736  chpscmatgsumbin  22738  chpscmatgsummon  22739  ptpjpre1  23465  fin1aufil  23826  lmflf  23899  tsmsfbas  24022  xpsxmetlem  24274  xpsmet  24277  metustsym  24450  iscmet3lem3  25197  iscmet3lem1  25198  iscmet3lem2  25199  iscmet3  25200  rrxmvallem  25311  volsup  25464  opnmblALT  25511  itg1val  25591  tdeglem2  25973  ulmcaulem  26310  ulmcau  26311  ulmss  26313  pserdvlem2  26345  eff1olem  26464  logdmnrp  26557  dvlog2lem  26568  logtayl  26576  cxpcn3lem  26664  atancl  26798  atanval  26801  chp1  27084  ppiublem2  27121  lgsdir2lem2  27244  lgsdir2lem3  27245  lgsquadlem2  27299  2lgslem1b  27310  rplogsumlem1  27402  rplogsumlem2  27403  pntlemj  27521  nnne0s  28236  1vgrex  28936  edglnl  29077  usgredg2v  29161  umgrres1lem  29244  upgrres1  29247  nbupgrres  29298  clwlkwlk  29712  wwlksnextproplem1  29846  wwlksnextproplem2  29847  wwlksnextproplem3  29848  rusgrnumwwlkb0  29908  clwlkclwwlklem2a4  29933  eleclclwwlknlem1  29996  eleclclwwlknlem2  29997  erclwwlkneqlen  30004  erclwwlknref  30005  erclwwlknsym  30006  erclwwlkntr  30007  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  frgrnbnb  30229  frgrwopreglem4  30251  frgrwopreglem5  30257  frgrwopreg  30259  numclwlk1  30307  vciOLD  30497  axhcompl-zf  30934  mayete3i  31664  pj3lem1  32142  fzto1stfv1  33065  fzto1st  33067  fzto1stinvn  33068  psgnfzto1st  33069  rmfsupp2  33196  erler  33223  submat1n  33802  xrge0mulc1cn  33938  fiunelros  34171  elmbfmvol2  34265  fibp1  34399  rrvsum  34452  ballotlemfmpn  34493  reprsuc  34613  bnj529  34738  bnj923  34765  bnj570  34902  bnj594  34909  bnj1173  34999  bnj1256  35012  bnj1259  35013  bnj1296  35018  bnj1498  35058  subfacp1lem1  35173  kur14lem7  35206  sat1el2xp  35373  mvrsval  35499  mvrsfpw  35500  mrsubcv  35504  mrsubccat  35512  msubff  35524  msrid  35539  msubvrs  35554  mppsval  35566  divcnvlin  35727  iprodefisumlem  35734  iprodefisum  35735  faclimlem1  35737  onsucsuccmpi  36438  bj-opelresdm  37140  bj-inftyexpitaudisj  37200  bj-inftyexpidisj  37205  bj-ccinftydisj  37208  bj-elccinfty  37209  finixpnum  37606  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem9  37630  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem29  37650  poimirlem30  37651  broucube  37655  volsupnfl  37666  dvasin  37705  dvacos  37706  sdclem2  37743  fdc  37746  heiborlem4  37815  heiborlem6  37817  smgrpismgmOLD  37863  mndoissmgrpOLD  37869  mndoisexid  37870  rngoueqz  37941  drngoi  37952  redvmptabs  42355  mhphflem  42591  prjspertr  42600  prjsperref  42601  prjspersym  42602  prjspreln0  42604  prjspvs  42605  prjsprellsp  42606  jm2.23  42992  wepwsolem  43038  omabs2  43328  omcl3g  43330  trclfvdecomr  43724  mnuprdlem1  44268  mnuprdlem2  44269  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  orbitcl  44954  ssfiunibd  45314  climinf  45611  stoweidlem15  46020  fourierdlem66  46177  etransclem37  46276  smfsupmpt  46820  smfinfmpt  46824  smflimsuplem8  46832  eldmressn  47042  afvres  47177  ndmaovrcl  47209  2ltceilhalf  47333  minusmodnep2tmod  47358  modmknepk  47367  mod2addne  47369  modm2nep1  47371  modm1nep2  47373  modm1nem2  47374  modm1p1ne  47375  sprsymrelfv  47499  fmtnofz04prm  47582  31prm  47602  stgr0  47963  stgr1  47964  gpgiedgdmellem  48041  gpgvtx1  48049  gpgedgvtx1  48057  gpgedg2iv  48062  gpg5nbgrvtx13starlem2  48067  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem6  48118  2zrngamnd  48239  2zrngacmnd  48240  2zrngagrp  48241  2zrngALT  48246  2zrngnmlid  48247  2zrngnmlid2  48249  fldhmsubcALTV  48325  lincvalsng  48409  snlindsntor  48464  lincresunit3lem2  48473  lincresunit3  48474  ldepsnlinc  48501  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  rrx2pnecoorneor  48708  rrx2linest  48735  rrx2linesl  48736  isorcl  49026  catcrcl  49388  setc2othin  49459