Theorem eleq2s 2881

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  elrabi  3647  optocl  5757  optoclOLD  5758  ssrel  5771  eldmeldmressn  6026  imadifssran  6204  predel  6324  fveqdmss  7075  oprabv  7472  elmpocl  7653  el2mpocsbcl  8081  bropopvvv  8086  bropfvvvv  8088  ressuppss  8180  mpoxeldm  8208  mpoxopn0yelv  8210  mpoxopxnop0  8212  tfr2a  8383  rdgseg  8410  2oconcl  8489  ecexr  8700  ectocld  8781  ecoptocl  8806  brecop2  8810  eroveu  8811  mapfvd  8878  mapsnconst  8891  mapfienlem1  9366  mapfienlem2  9367  mapfienlem3  9368  cantnflem2  9660  r1sucg  9742  r1suc  9743  acnrcl  10027  dfac5lem4  10111  fin23lem29  10326  fin23lem30  10327  axcclem  10442  alephval2  10558  0tsk  10741  0nsr  11065  peano2nn  12246  uzssz  12884  peano2uzs  12927  uzsupss  12965  fzssnn  13598  prednn0  13682  fzossnn0  13721  fldiv4p1lem1div2  13870  modaddid  13945  ltweuz  13999  fzennn  14006  ser1const  14096  expp1  14106  facnn  14313  facp1  14316  bcpasc  14359  hashfzo0  14469  tpfo  14539  ccatval2  14617  ccatass  14628  swrd00  14684  swrd0  14698  pfx00  14714  pfx0  14715  wrdeqs1cat  14759  splfv2a  14795  revccat  14805  rexuz3  15402  rexanuz2  15403  r19.2uz  15405  rexuzre  15406  cau4  15410  caubnd2  15411  climrlim2  15600  climshft2  15635  climaddc1  15688  climmulc2  15690  climsubc1  15691  climsubc2  15692  climlec2  15712  isercoll2  15722  climsup  15723  climcau  15724  caurcvg  15730  caurcvg2  15731  caucvg  15732  caucvgb  15733  iseraltlem1  15735  iseralt  15738  binomlem  15885  isumshft  15895  cvgrat  15939  clim2div  15945  ntrivcvg  15953  ntrivcvgtail  15956  fprodntriv  15998  fprodeq0  16031  fprodefsum  16150  pwp1fsum  16450  3prm  16753  phicl2  16828  phibndlem  16830  dfphi2  16834  crth  16838  vdwap0  17037  prmlem1a  17167  fvprif  17616  xpsfeq  17618  oppccofval  17773  homarcl2  18093  arwrcl  18102  pleval2i  18391  letsr  18650  gsumws1  18898  smndex1mndlem  18972  mulgnngsum  19146  mulgpropd  19183  psgnunilem2  19566  psgnprfval  19592  gexid  19652  efgmnvl  19785  efgrcl  19786  efgsval  19802  efgs1  19806  efgs1b  19807  frgpuptinv  19842  frgpup3lem  19848  lt6abl  19966  eldprd  20077  isunit  20456  isirred  20502  fldhmsubc  20869  abvrcl  20897  islss  21036  lbsss  21179  lbssp  21181  lbsind  21182  cssi  21815  thlle  21828  islbs4  21963  psrbagleadd1  22059  mpfrcl  22217  psr1basf  22342  coe1tm  22415  ply1frcl  22459  mavmulsolcl  22689  marepvcl  22707  1marepvmarrepid  22713  mdet0pr  22730  m2detleiblem1  22762  cramerimplem1  22821  cramerlem1  22825  chpscmat  22980  chpscmatgsumbin  22982  chpscmatgsummon  22983  ptpjpre1  23709  fin1aufil  24070  lmflf  24143  tsmsfbas  24266  xpsxmetlem  24517  xpsmet  24520  metustsym  24693  iscmet3lem3  25430  iscmet3lem1  25431  iscmet3lem2  25432  iscmet3  25433  rrxmvallem  25544  volsup  25696  opnmblALT  25743  itg1val  25823  tdeglem2  26199  ulmcaulem  26538  ulmcau  26539  ulmss  26541  pserdvlem2  26572  eff1olem  26694  logdmnrp  26787  dvlog2lem  26798  logtayl  26806  cxpcn3lem  26893  atancl  27027  atanval  27030  chp1  27312  ppiublem2  27348  lgsdir2lem2  27471  lgsdir2lem3  27472  lgsquadlem2  27526  2lgslem1b  27537  rplogsumlem1  27629  rplogsumlem2  27630  pntlemj  27748  nnne0s  28511  1vgrex  29333  edglnl  29474  usgredg2v  29558  umgrres1lem  29641  upgrres1  29644  nbupgrres  29695  clwlkwlk  30105  wwlksnextproplem1  30239  wwlksnextproplem2  30240  wwlksnextproplem3  30241  rusgrnumwwlkb0  30304  clwlkclwwlklem2a4  30329  eleclclwwlknlem1  30392  eleclclwwlknlem2  30393  erclwwlkneqlen  30400  erclwwlknref  30401  erclwwlknsym  30402  erclwwlkntr  30403  hashecclwwlkn1  30409  umgrhashecclwwlk  30410  frgrnbnb  30625  frgrwopreglem4  30647  frgrwopreglem5  30653  frgrwopreg  30655  numclwlk1  30703  vciOLD  30894  axhcompl-zf  31331  mayete3i  32061  pj3lem1  32539  fzto1stfv1  33402  fzto1st  33404  fzto1stinvn  33405  psgnfzto1st  33406  rmfsupp2  33538  erler  33566  selvply1rhmlemb  33890  vieta  33951  submat1n  34176  xrge0mulc1cn  34312  fiunelros  34545  elmbfmvol2  34638  fibp1  34772  rrvsum  34825  ballotlemfmpn  34866  reprsuc  34983  bnj529  35111  bnj923  35138  bnj570  35274  bnj594  35281  bnj1173  35371  bnj1256  35384  bnj1259  35385  bnj1296  35390  bnj1498  35430  rankfo  35486  fineqvnttrclselem1  35515  subfacp1lem1  35652  kur14lem7  35685  sat1el2xp  35852  mvrsval  35978  mvrsfpw  35979  mrsubcv  35983  mrsubccat  35991  msubff  36003  msrid  36018  msubvrs  36033  mppsval  36045  divcnvlin  36206  iprodefisumlem  36213  iprodefisum  36214  faclimlem1  36216  onsucsuccmpi  36935  bj-opelresdm  37770  bj-inftyexpitaudisj  37830  bj-inftyexpidisj  37835  bj-ccinftydisj  37838  bj-elccinfty  37839  finixpnum  38237  poimirlem5  38257  poimirlem6  38258  poimirlem7  38259  poimirlem8  38260  poimirlem9  38261  poimirlem10  38262  poimirlem11  38263  poimirlem12  38264  poimirlem13  38265  poimirlem14  38266  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem18  38270  poimirlem19  38271  poimirlem20  38272  poimirlem21  38273  poimirlem22  38274  poimirlem29  38281  poimirlem30  38282  broucube  38286  volsupnfl  38297  dvasin  38336  dvacos  38337  sdclem2  38374  fdc  38377  heiborlem4  38446  heiborlem6  38448  smgrpismgmOLD  38494  mndoissmgrpOLD  38500  mndoisexid  38501  rngoueqz  38572  drngoi  38583  dfadjliftmap2  39087  dfblockliftmap2  39091  sucpre  39127  eldisjsim2  39565  redvmptabs  43102  mhphflem  43311  prjspertr  43320  prjsperref  43321  prjspersym  43322  prjspreln0  43324  prjspvs  43325  prjsprellsp  43326  jm2.23  43706  wepwsolem  43752  omabs2  44042  omcl3g  44044  trclfvdecomr  44437  mnuprdlem1  44965  mnuprdlem2  44966  binomcxplemdvbinom  45046  binomcxplemnotnn0  45049  orbitcl  45649  ssfiunibd  46011  climinf  46305  stoweidlem15  46712  fourierdlem66  46869  etransclem37  46968  smfsupmpt  47512  smfinfmpt  47516  smflimsuplem8  47524  eldmressn  47757  afvres  47892  ndmaovrcl  47924  2ltceilhalf  48052  minusmodnep2tmod  48079  modmknepk  48088  mod2addne  48090  modm2nep1  48092  modm1nep2  48094  modm1nem2  48095  modm1p1ne  48096  sprsymrelfv  48226  fmtnofz04prm  48312  31prm  48332  ppivalnnnprm  48363  indprmfz  48365  stgr0  48708  stgr1  48709  gpgiedgdmellem  48794  gpgvtx1  48802  gpgedgvtx1  48810  gpgedg2iv  48815  gpg5nbgrvtx13starlem2  48820  pgnbgreunbgrlem3  48866  pgnbgreunbgrlem6  48872  2zrngamnd  48995  2zrngacmnd  48996  2zrngagrp  48997  2zrngALT  49002  2zrngnmlid  49003  2zrngnmlid2  49005  fldhmsubcALTV  49081  lincvalsng  49179  snlindsntor  49234  lincresunit3lem2  49243  lincresunit3  49244  ldepsnlinc  49271  nn0sumshdiglemA  49382  nn0sumshdiglemB  49383  rrx2pnecoorneor  49478  rrx2linest  49505  rrx2linesl  49506  isorcl  49794  catcrcl  50156  setc2othin  50227