Theorem eleq2s 2876

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

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2769  df-clel 2773

This theorem is referenced by:  elrabi  3566  epelg  5267  elxpi  5377  optocl  5443  eldmeldmressn  5690  predel  5950  fveqdmss  6618  oprabv  6980  elmpt2cl  7153  el2mpt2csbcl  7530  bropopvvv  7536  bropfvvvv  7538  ressuppss  7595  mpt2xeldm  7619  mpt2xopn0yelv  7621  mpt2xopxnop0  7623  tfr2a  7774  rdgseg  7801  2oconcl  7867  ecexr  8031  ectocld  8097  ecoptocl  8120  brecop2  8124  brecop2OLD  8125  eroveu  8126  mapfvd  8177  mapsnconst  8189  mapfienlem1  8598  mapfienlem2  8599  mapfienlem3  8600  cantnflem2  8884  r1sucg  8929  r1suc  8930  acnrcl  9198  dfac5lem4  9282  fin23lem29  9498  fin23lem30  9499  axcclem  9614  alephval2  9729  0tsk  9912  0nsr  10236  peano2nn  11388  uzssz  12012  peano2uzs  12048  uzsupss  12087  fzssnn  12702  prednn0  12782  fzossnn0  12818  fldiv4p1lem1div2  12955  ltweuz  13079  fzennn  13086  ser1const  13175  expp1  13185  facnn  13380  facp1  13383  bcpasc  13426  hashfzo0  13531  ccatval2  13668  ccatass  13678  swrd00  13734  swrd0  13753  pfx00  13783  pfx0  13784  wrdeqs1cat  13839  wrdeqs1catOLD  13840  splfv2a  13900  splfv2aOLD  13901  revccat  13912  rexuz3  14495  rexanuz2  14496  r19.2uz  14498  rexuzre  14499  cau4  14503  caubnd2  14504  climrlim2  14686  climshft2  14721  climaddc1  14773  climmulc2  14775  climsubc1  14776  climsubc2  14777  climlec2  14797  isercoll2  14807  climsup  14808  climcau  14809  caurcvg  14815  caurcvg2  14816  caucvg  14817  caucvgb  14818  iseraltlem1  14820  iseralt  14823  binomlem  14965  isumshft  14975  cvgrat  15018  clim2div  15024  ntrivcvg  15032  ntrivcvgtail  15035  fprodntriv  15075  fprodeq0  15108  fprodefsum  15227  pwp1fsum  15521  3prm  15811  phicl2  15877  phibndlem  15879  dfphi2  15883  crth  15887  vdwap0  16084  prmlem1a  16212  xpscfv  16608  xpsfeq  16610  oppccofval  16761  homarcl2  17070  arwrcl  17079  pleval2i  17350  letsr  17613  gsumws1  17762  mulgpropd  17968  psgnunilem2  18299  psgnprfval  18325  gexid  18380  efgmnvl  18511  efgrcl  18512  efgsval  18528  efgs1  18532  efgs1b  18533  frgpuptinv  18570  frgpup3lem  18576  lt6abl  18682  eldprd  18790  isunit  19044  isirred  19086  abvrcl  19213  islss  19327  lbsss  19472  lbssp  19474  lbsind  19475  mpfrcl  19914  psr1basf  19967  coe1tm  20039  ply1frcl  20079  cssi  20427  thlle  20440  islbs4  20575  mavmulsolcl  20762  marepvcl  20780  1marepvmarrepid  20786  mdet0pr  20803  m2detleiblem1  20835  cramerimplem1  20895  cramerimplem1OLD  20896  cramerlem1  20900  chpscmat  21054  chpscmatgsumbin  21056  chpscmatgsummon  21057  ptpjpre1  21783  fin1aufil  22144  lmflf  22217  tsmsfbas  22339  xpsxmetlem  22592  xpsmet  22595  metustsym  22768  iscmet3lem3  23496  iscmet3lem1  23497  iscmet3lem2  23498  iscmet3  23499  rrxmvallem  23610  volsup  23760  opnmblALT  23807  itg1val  23887  tdeglem2  24258  ulmcaulem  24585  ulmcau  24586  ulmss  24588  pserdvlem2  24619  eff1olem  24732  logdmnrp  24824  dvlog2lem  24835  logtayl  24843  cxpcn3lem  24928  atancl  25059  atanval  25062  chp1  25345  ppiublem2  25380  lgsdir2lem2  25503  lgsdir2lem3  25504  lgsquadlem2  25558  2lgslem1b  25569  rplogsumlem1  25625  rplogsumlem2  25626  pntlemj  25744  1vgrex  26350  edglnl  26492  usgredg2v  26573  umgrres1lem  26657  upgrres1  26660  nbupgrres  26711  clwlkwlk  27127  wwlksnextproplem1  27283  wwlksnextproplem1OLD  27284  wwlksnextproplem2  27285  wwlksnextproplem2OLD  27286  wwlksnextproplem3  27287  wwlksnextproplem3OLD  27288  rusgrnumwwlkb0  27351  clwlkclwwlklem2a4  27377  eleclclwwlknlem1  27458  eleclclwwlknlem2  27459  erclwwlkneqlen  27466  erclwwlknref  27467  erclwwlknsym  27468  erclwwlkntr  27469  hashecclwwlkn1  27475  umgrhashecclwwlk  27476  frgrnbnb  27701  frgrwopreglem4  27723  frgrwopreglem5  27729  frgrwopreg  27731  numclwlk1  27799  vciOLD  27988  axhcompl-zf  28427  mayete3i  29159  pj3lem1  29637  fzto1stfv1  30449  fzto1st  30451  fzto1stinvn  30452  psgnfzto1st  30453  submat1n  30469  xrge0mulc1cn  30585  fiunelros  30835  elmbfmvol2  30927  fibp1  31062  rrvsum  31115  ballotlemfmpn  31155  reprsuc  31295  bnj529  31410  bnj923  31437  bnj570  31574  bnj594  31581  bnj1173  31669  bnj1256  31682  bnj1259  31683  bnj1296  31688  bnj1498  31728  subfacp1lem1  31760  kur14lem7  31793  mvrsval  32001  mvrsfpw  32002  mrsubcv  32006  mrsubccat  32014  msubff  32026  msrid  32041  msubvrs  32056  mppsval  32068  divcnvlin  32212  iprodefisumlem  32220  iprodefisum  32221  faclimlem1  32223  onsucsuccmpi  33025  bj-inftyexpitaudisj  33682  bj-inftyexpidisj  33687  bj-ccinftydisj  33690  bj-elccinfty  33691  finixpnum  34003  poimirlem5  34024  poimirlem6  34025  poimirlem7  34026  poimirlem8  34027  poimirlem9  34028  poimirlem10  34029  poimirlem11  34030  poimirlem12  34031  poimirlem13  34032  poimirlem14  34033  poimirlem15  34034  poimirlem16  34035  poimirlem17  34036  poimirlem18  34037  poimirlem19  34038  poimirlem20  34039  poimirlem21  34040  poimirlem22  34041  poimirlem29  34048  poimirlem30  34049  broucube  34053  volsupnfl  34064  dvasin  34105  dvacos  34106  sdclem2  34146  fdc  34149  heiborlem4  34221  heiborlem6  34223  smgrpismgmOLD  34269  mndoissmgrpOLD  34275  mndoisexid  34276  rngoueqz  34347  drngoi  34358  jm2.23  38504  wepwsolem  38553  trclfvdecomr  38959  binomcxplemdvbinom  39490  binomcxplemnotnn0  39493  ssfiunibd  40414  climinf  40728  stoweidlem15  41141  fourierdlem66  41298  etransclem37  41397  smflimsuplem8  41942  eldmressn  42083  afvres  42195  ndmaovrcl  42227  sprsymrelfv  42415  fmtnofz04prm  42492  31prm  42515  2zrngamnd  42938  2zrngacmnd  42939  2zrngagrp  42940  2zrngALT  42945  2zrngnmlid  42946  2zrngnmlid2  42948  fldhmsubc  43081  fldhmsubcALTV  43099  lincvalsng  43202  snlindsntor  43257  lincresunit3lem2  43266  lincresunit3  43267  ldepsnlinc  43294  nn0sumshdiglemA  43410  nn0sumshdiglemB  43411  rrx2pnecoorneor  43433  rrx2linest  43460  rrx2linesl  43461