Theorem eleq2s 2856

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  elrabi  3689  optocl  5782  ssrel  5794  eldmeldmressn  6044  predel  6343  fveqdmss  7097  oprabv  7492  elmpocl  7673  el2mpocsbcl  8108  bropopvvv  8113  bropfvvvv  8115  ressuppss  8206  mpoxeldm  8234  mpoxopn0yelv  8236  mpoxopxnop0  8238  tfr2a  8433  rdgseg  8460  2oconcl  8539  ecexr  8748  ectocld  8822  ecoptocl  8845  brecop2  8849  eroveu  8850  mapfvd  8917  mapsnconst  8930  mapfienlem1  9442  mapfienlem2  9443  mapfienlem3  9444  cantnflem2  9727  r1sucg  9806  r1suc  9807  acnrcl  10079  dfac5lem4  10163  dfac5lem4OLD  10165  fin23lem29  10378  fin23lem30  10379  axcclem  10494  alephval2  10609  0tsk  10792  0nsr  11116  peano2nn  12275  uzssz  12896  peano2uzs  12941  uzsupss  12979  fzssnn  13604  prednn0  13688  fzossnn0  13726  fldiv4p1lem1div2  13871  ltweuz  13998  fzennn  14005  ser1const  14095  expp1  14105  facnn  14310  facp1  14313  bcpasc  14356  hashfzo0  14465  tpfo  14535  ccatval2  14612  ccatass  14622  swrd00  14678  swrd0  14692  pfx00  14708  pfx0  14709  wrdeqs1cat  14754  splfv2a  14790  revccat  14800  rexuz3  15383  rexanuz2  15384  r19.2uz  15386  rexuzre  15387  cau4  15391  caubnd2  15392  climrlim2  15579  climshft2  15614  climaddc1  15667  climmulc2  15669  climsubc1  15670  climsubc2  15671  climlec2  15691  isercoll2  15701  climsup  15702  climcau  15703  caurcvg  15709  caurcvg2  15710  caucvg  15711  caucvgb  15712  iseraltlem1  15714  iseralt  15717  binomlem  15861  isumshft  15871  cvgrat  15915  clim2div  15921  ntrivcvg  15929  ntrivcvgtail  15932  fprodntriv  15974  fprodeq0  16007  fprodefsum  16127  pwp1fsum  16424  3prm  16727  phicl2  16801  phibndlem  16803  dfphi2  16807  crth  16811  vdwap0  17009  prmlem1a  17140  fvprif  17607  xpsfeq  17609  oppccofval  17761  homarcl2  18088  arwrcl  18097  pleval2i  18393  letsr  18650  gsumws1  18863  smndex1mndlem  18934  mulgnngsum  19109  mulgpropd  19146  psgnunilem2  19527  psgnprfval  19553  gexid  19613  efgmnvl  19746  efgrcl  19747  efgsval  19763  efgs1  19767  efgs1b  19768  frgpuptinv  19803  frgpup3lem  19809  lt6abl  19927  eldprd  20038  isunit  20389  isirred  20435  fldhmsubc  20802  abvrcl  20830  islss  20949  lbsss  21093  lbssp  21095  lbsind  21096  cssi  21719  thlle  21733  thlleOLD  21734  islbs4  21869  psrbagleadd1  21965  mpfrcl  22126  psr1basf  22218  coe1tm  22291  ply1frcl  22337  mavmulsolcl  22572  marepvcl  22590  1marepvmarrepid  22596  mdet0pr  22613  m2detleiblem1  22645  cramerimplem1  22704  cramerlem1  22708  chpscmat  22863  chpscmatgsumbin  22865  chpscmatgsummon  22866  ptpjpre1  23594  fin1aufil  23955  lmflf  24028  tsmsfbas  24151  xpsxmetlem  24404  xpsmet  24407  metustsym  24583  iscmet3lem3  25337  iscmet3lem1  25338  iscmet3lem2  25339  iscmet3  25340  rrxmvallem  25451  volsup  25604  opnmblALT  25651  itg1val  25731  tdeglem2  26114  ulmcaulem  26451  ulmcau  26452  ulmss  26454  pserdvlem2  26486  eff1olem  26604  logdmnrp  26697  dvlog2lem  26708  logtayl  26716  cxpcn3lem  26804  atancl  26938  atanval  26941  chp1  27224  ppiublem2  27261  lgsdir2lem2  27384  lgsdir2lem3  27385  lgsquadlem2  27439  2lgslem1b  27450  rplogsumlem1  27542  rplogsumlem2  27543  pntlemj  27661  nnne0s  28354  1vgrex  29033  edglnl  29174  usgredg2v  29258  umgrres1lem  29341  upgrres1  29344  nbupgrres  29395  clwlkwlk  29807  wwlksnextproplem1  29938  wwlksnextproplem2  29939  wwlksnextproplem3  29940  rusgrnumwwlkb0  30000  clwlkclwwlklem2a4  30025  eleclclwwlknlem1  30088  eleclclwwlknlem2  30089  erclwwlkneqlen  30096  erclwwlknref  30097  erclwwlknsym  30098  erclwwlkntr  30099  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  frgrnbnb  30321  frgrwopreglem4  30343  frgrwopreglem5  30349  frgrwopreg  30351  numclwlk1  30399  vciOLD  30589  axhcompl-zf  31026  mayete3i  31756  pj3lem1  32234  fzto1stfv1  33103  fzto1st  33105  fzto1stinvn  33106  psgnfzto1st  33107  rmfsupp2  33227  erler  33251  submat1n  33765  xrge0mulc1cn  33901  fiunelros  34154  elmbfmvol2  34248  fibp1  34382  rrvsum  34435  ballotlemfmpn  34475  reprsuc  34608  bnj529  34733  bnj923  34760  bnj570  34897  bnj594  34904  bnj1173  34994  bnj1256  35007  bnj1259  35008  bnj1296  35013  bnj1498  35053  subfacp1lem1  35163  kur14lem7  35196  sat1el2xp  35363  mvrsval  35489  mvrsfpw  35490  mrsubcv  35494  mrsubccat  35502  msubff  35514  msrid  35529  msubvrs  35544  mppsval  35556  divcnvlin  35712  iprodefisumlem  35719  iprodefisum  35720  faclimlem1  35722  onsucsuccmpi  36425  bj-opelresdm  37127  bj-inftyexpitaudisj  37187  bj-inftyexpidisj  37192  bj-ccinftydisj  37195  bj-elccinfty  37196  finixpnum  37591  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem9  37615  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem29  37635  poimirlem30  37636  broucube  37640  volsupnfl  37651  dvasin  37690  dvacos  37691  sdclem2  37728  fdc  37731  heiborlem4  37800  heiborlem6  37802  smgrpismgmOLD  37848  mndoissmgrpOLD  37854  mndoisexid  37855  rngoueqz  37926  drngoi  37937  redvmptabs  42368  mhphflem  42582  prjspertr  42591  prjsperref  42592  prjspersym  42593  prjspreln0  42595  prjspvs  42596  prjsprellsp  42597  jm2.23  42984  wepwsolem  43030  omabs2  43321  omcl3g  43323  trclfvdecomr  43717  mnuprdlem1  44267  mnuprdlem2  44268  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  ssfiunibd  45259  climinf  45561  stoweidlem15  45970  fourierdlem66  46127  etransclem37  46226  smfsupmpt  46770  smfinfmpt  46774  smflimsuplem8  46782  eldmressn  46986  afvres  47121  ndmaovrcl  47153  minusmodnep2tmod  47292  sprsymrelfv  47418  fmtnofz04prm  47501  31prm  47521  uspgrimprop  47810  stgr0  47862  stgr1  47863  gpgedgel  47942  gpgvtx1  47944  2ltceilhalf  47949  gpgedgvtx1  47954  gpg5nbgrvtx13starlem2  47962  2zrngamnd  48090  2zrngacmnd  48091  2zrngagrp  48092  2zrngALT  48097  2zrngnmlid  48098  2zrngnmlid2  48100  fldhmsubcALTV  48176  lincvalsng  48261  snlindsntor  48316  lincresunit3lem2  48325  lincresunit3  48326  ldepsnlinc  48353  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  rrx2pnecoorneor  48564  rrx2linest  48591  rrx2linesl  48592  setc2othin  48856