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 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 2707

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

This theorem is referenced by:  elrabi  3666  optocl  5749  ssrel  5761  eldmeldmressn  6012  predel  6310  fveqdmss  7067  oprabv  7465  elmpocl  7646  el2mpocsbcl  8082  bropopvvv  8087  bropfvvvv  8089  ressuppss  8180  mpoxeldm  8208  mpoxopn0yelv  8210  mpoxopxnop0  8212  tfr2a  8407  rdgseg  8434  2oconcl  8513  ecexr  8722  ectocld  8796  ecoptocl  8819  brecop2  8823  eroveu  8824  mapfvd  8891  mapsnconst  8904  mapfienlem1  9415  mapfienlem2  9416  mapfienlem3  9417  cantnflem2  9702  r1sucg  9781  r1suc  9782  acnrcl  10054  dfac5lem4  10138  dfac5lem4OLD  10140  fin23lem29  10353  fin23lem30  10354  axcclem  10469  alephval2  10584  0tsk  10767  0nsr  11091  peano2nn  12250  uzssz  12871  peano2uzs  12916  uzsupss  12954  fzssnn  13583  prednn0  13667  fzossnn0  13705  fldiv4p1lem1div2  13850  ltweuz  13977  fzennn  13984  ser1const  14074  expp1  14084  facnn  14291  facp1  14294  bcpasc  14337  hashfzo0  14446  tpfo  14516  ccatval2  14594  ccatass  14604  swrd00  14660  swrd0  14674  pfx00  14690  pfx0  14691  wrdeqs1cat  14736  splfv2a  14772  revccat  14782  rexuz3  15365  rexanuz2  15366  r19.2uz  15368  rexuzre  15369  cau4  15373  caubnd2  15374  climrlim2  15561  climshft2  15596  climaddc1  15649  climmulc2  15651  climsubc1  15652  climsubc2  15653  climlec2  15673  isercoll2  15683  climsup  15684  climcau  15685  caurcvg  15691  caurcvg2  15692  caucvg  15693  caucvgb  15694  iseraltlem1  15696  iseralt  15699  binomlem  15843  isumshft  15853  cvgrat  15897  clim2div  15903  ntrivcvg  15911  ntrivcvgtail  15914  fprodntriv  15956  fprodeq0  15989  fprodefsum  16109  pwp1fsum  16408  3prm  16711  phicl2  16785  phibndlem  16787  dfphi2  16791  crth  16795  vdwap0  16994  prmlem1a  17124  fvprif  17573  xpsfeq  17575  oppccofval  17726  homarcl2  18046  arwrcl  18055  pleval2i  18344  letsr  18601  gsumws1  18814  smndex1mndlem  18885  mulgnngsum  19060  mulgpropd  19097  psgnunilem2  19474  psgnprfval  19500  gexid  19560  efgmnvl  19693  efgrcl  19694  efgsval  19710  efgs1  19714  efgs1b  19715  frgpuptinv  19750  frgpup3lem  19756  lt6abl  19874  eldprd  19985  isunit  20331  isirred  20377  fldhmsubc  20743  abvrcl  20771  islss  20889  lbsss  21033  lbssp  21035  lbsind  21036  cssi  21642  thlle  21655  islbs4  21790  psrbagleadd1  21886  mpfrcl  22041  psr1basf  22135  coe1tm  22208  ply1frcl  22254  mavmulsolcl  22487  marepvcl  22505  1marepvmarrepid  22511  mdet0pr  22528  m2detleiblem1  22560  cramerimplem1  22619  cramerlem1  22623  chpscmat  22778  chpscmatgsumbin  22780  chpscmatgsummon  22781  ptpjpre1  23507  fin1aufil  23868  lmflf  23941  tsmsfbas  24064  xpsxmetlem  24316  xpsmet  24319  metustsym  24492  iscmet3lem3  25240  iscmet3lem1  25241  iscmet3lem2  25242  iscmet3  25243  rrxmvallem  25354  volsup  25507  opnmblALT  25554  itg1val  25634  tdeglem2  26016  ulmcaulem  26353  ulmcau  26354  ulmss  26356  pserdvlem2  26388  eff1olem  26507  logdmnrp  26600  dvlog2lem  26611  logtayl  26619  cxpcn3lem  26707  atancl  26841  atanval  26844  chp1  27127  ppiublem2  27164  lgsdir2lem2  27287  lgsdir2lem3  27288  lgsquadlem2  27342  2lgslem1b  27353  rplogsumlem1  27445  rplogsumlem2  27446  pntlemj  27564  nnne0s  28257  1vgrex  28927  edglnl  29068  usgredg2v  29152  umgrres1lem  29235  upgrres1  29238  nbupgrres  29289  clwlkwlk  29703  wwlksnextproplem1  29837  wwlksnextproplem2  29838  wwlksnextproplem3  29839  rusgrnumwwlkb0  29899  clwlkclwwlklem2a4  29924  eleclclwwlknlem1  29987  eleclclwwlknlem2  29988  erclwwlkneqlen  29995  erclwwlknref  29996  erclwwlknsym  29997  erclwwlkntr  29998  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  frgrnbnb  30220  frgrwopreglem4  30242  frgrwopreglem5  30248  frgrwopreg  30250  numclwlk1  30298  vciOLD  30488  axhcompl-zf  30925  mayete3i  31655  pj3lem1  32133  fzto1stfv1  33058  fzto1st  33060  fzto1stinvn  33061  psgnfzto1st  33062  rmfsupp2  33179  erler  33206  submat1n  33782  xrge0mulc1cn  33918  fiunelros  34151  elmbfmvol2  34245  fibp1  34379  rrvsum  34432  ballotlemfmpn  34473  reprsuc  34593  bnj529  34718  bnj923  34745  bnj570  34882  bnj594  34889  bnj1173  34979  bnj1256  34992  bnj1259  34993  bnj1296  34998  bnj1498  35038  subfacp1lem1  35147  kur14lem7  35180  sat1el2xp  35347  mvrsval  35473  mvrsfpw  35474  mrsubcv  35478  mrsubccat  35486  msubff  35498  msrid  35513  msubvrs  35528  mppsval  35540  divcnvlin  35696  iprodefisumlem  35703  iprodefisum  35704  faclimlem1  35706  onsucsuccmpi  36407  bj-opelresdm  37109  bj-inftyexpitaudisj  37169  bj-inftyexpidisj  37174  bj-ccinftydisj  37177  bj-elccinfty  37178  finixpnum  37575  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem9  37599  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem13  37603  poimirlem14  37604  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem29  37619  poimirlem30  37620  broucube  37624  volsupnfl  37635  dvasin  37674  dvacos  37675  sdclem2  37712  fdc  37715  heiborlem4  37784  heiborlem6  37786  smgrpismgmOLD  37832  mndoissmgrpOLD  37838  mndoisexid  37839  rngoueqz  37910  drngoi  37921  redvmptabs  42350  mhphflem  42566  prjspertr  42575  prjsperref  42576  prjspersym  42577  prjspreln0  42579  prjspvs  42580  prjsprellsp  42581  jm2.23  42967  wepwsolem  43013  omabs2  43303  omcl3g  43305  trclfvdecomr  43699  mnuprdlem1  44244  mnuprdlem2  44245  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  orbitcl  44930  ssfiunibd  45286  climinf  45583  stoweidlem15  45992  fourierdlem66  46149  etransclem37  46248  smfsupmpt  46792  smfinfmpt  46796  smflimsuplem8  46804  eldmressn  47014  afvres  47149  ndmaovrcl  47181  2ltceilhalf  47305  minusmodnep2tmod  47330  sprsymrelfv  47456  fmtnofz04prm  47539  31prm  47559  stgr0  47920  stgr1  47921  gpgiedgdmellem  47998  gpgvtx1  48006  gpgedgvtx1  48014  gpg5nbgrvtx13starlem2  48022  2zrngamnd  48170  2zrngacmnd  48171  2zrngagrp  48172  2zrngALT  48177  2zrngnmlid  48178  2zrngnmlid2  48180  fldhmsubcALTV  48256  lincvalsng  48340  snlindsntor  48395  lincresunit3lem2  48404  lincresunit3  48405  ldepsnlinc  48432  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  rrx2pnecoorneor  48643  rrx2linest  48670  rrx2linesl  48671  setc2othin  49300