Theorem eleq2s 2934

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

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

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-clel 2896

This theorem is referenced by:  elrabi  3678  epelgOLD  5470  elxpi  5580  optocl  5648  eldmeldmressn  5899  predel  6168  fveqdmss  6849  oprabv  7217  elmpocl  7390  el2mpocsbcl  7783  bropopvvv  7788  bropfvvvv  7790  ressuppss  7852  mpoxeldm  7880  mpoxopn0yelv  7882  mpoxopxnop0  7884  tfr2a  8034  rdgseg  8061  2oconcl  8131  ecexr  8297  ectocld  8367  ecoptocl  8390  brecop2  8394  eroveu  8395  mapfvd  8446  mapsnconst  8459  mapfienlem1  8871  mapfienlem2  8872  mapfienlem3  8873  cantnflem2  9156  r1sucg  9201  r1suc  9202  acnrcl  9471  dfac5lem4  9555  fin23lem29  9766  fin23lem30  9767  axcclem  9882  alephval2  9997  0tsk  10180  0nsr  10504  peano2nn  11653  uzssz  12267  peano2uzs  12305  uzsupss  12343  fzssnn  12954  prednn0  13034  fzossnn0  13071  fldiv4p1lem1div2  13208  ltweuz  13332  fzennn  13339  ser1const  13429  expp1  13439  facnn  13638  facp1  13641  bcpasc  13684  hashfzo0  13794  ccatval2  13935  ccatass  13945  swrd00  14009  swrd0  14023  pfx00  14039  pfx0  14040  wrdeqs1cat  14085  splfv2a  14121  revccat  14131  rexuz3  14711  rexanuz2  14712  r19.2uz  14714  rexuzre  14715  cau4  14719  caubnd2  14720  climrlim2  14907  climshft2  14942  climaddc1  14994  climmulc2  14996  climsubc1  14997  climsubc2  14998  climlec2  15018  isercoll2  15028  climsup  15029  climcau  15030  caurcvg  15036  caurcvg2  15037  caucvg  15038  caucvgb  15039  iseraltlem1  15041  iseralt  15044  binomlem  15187  isumshft  15197  cvgrat  15242  clim2div  15248  ntrivcvg  15256  ntrivcvgtail  15259  fprodntriv  15299  fprodeq0  15332  fprodefsum  15451  pwp1fsum  15745  3prm  16041  phicl2  16108  phibndlem  16110  dfphi2  16114  crth  16118  vdwap0  16315  prmlem1a  16443  fvprif  16837  xpsfeq  16839  oppccofval  16989  homarcl2  17298  arwrcl  17307  pleval2i  17577  letsr  17840  gsumws1  18005  smndex1mndlem  18077  mulgnngsum  18236  mulgpropd  18272  psgnunilem2  18626  psgnprfval  18652  gexid  18709  efgmnvl  18843  efgrcl  18844  efgsval  18860  efgs1  18864  efgs1b  18865  frgpuptinv  18900  frgpup3lem  18906  lt6abl  19018  eldprd  19129  isunit  19410  isirred  19452  abvrcl  19595  islss  19709  lbsss  19852  lbssp  19854  lbsind  19855  mpfrcl  20301  psr1basf  20372  coe1tm  20444  ply1frcl  20484  cssi  20831  thlle  20844  islbs4  20979  mavmulsolcl  21163  marepvcl  21181  1marepvmarrepid  21187  mdet0pr  21204  m2detleiblem1  21236  cramerimplem1  21295  cramerlem1  21299  chpscmat  21453  chpscmatgsumbin  21455  chpscmatgsummon  21456  ptpjpre1  22182  fin1aufil  22543  lmflf  22616  tsmsfbas  22739  xpsxmetlem  22992  xpsmet  22995  metustsym  23168  iscmet3lem3  23896  iscmet3lem1  23897  iscmet3lem2  23898  iscmet3  23899  rrxmvallem  24010  volsup  24160  opnmblALT  24207  itg1val  24287  tdeglem2  24658  ulmcaulem  24985  ulmcau  24986  ulmss  24988  pserdvlem2  25019  eff1olem  25135  logdmnrp  25227  dvlog2lem  25238  logtayl  25246  cxpcn3lem  25331  atancl  25462  atanval  25465  chp1  25747  ppiublem2  25782  lgsdir2lem2  25905  lgsdir2lem3  25906  lgsquadlem2  25960  2lgslem1b  25971  rplogsumlem1  26063  rplogsumlem2  26064  pntlemj  26182  1vgrex  26790  edglnl  26931  usgredg2v  27012  umgrres1lem  27095  upgrres1  27098  nbupgrres  27149  clwlkwlk  27559  wwlksnextproplem1  27691  wwlksnextproplem2  27692  wwlksnextproplem3  27693  rusgrnumwwlkb0  27753  clwlkclwwlklem2a4  27778  eleclclwwlknlem1  27842  eleclclwwlknlem2  27843  erclwwlkneqlen  27850  erclwwlknref  27851  erclwwlknsym  27852  erclwwlkntr  27853  hashecclwwlkn1  27859  umgrhashecclwwlk  27860  frgrnbnb  28075  frgrwopreglem4  28097  frgrwopreglem5  28103  frgrwopreg  28105  numclwlk1  28153  vciOLD  28341  axhcompl-zf  28778  mayete3i  29508  pj3lem1  29986  fzto1stfv1  30747  fzto1st  30749  fzto1stinvn  30750  psgnfzto1st  30751  rmfsupp2  30870  submat1n  31074  xrge0mulc1cn  31188  fiunelros  31437  elmbfmvol2  31529  fibp1  31663  rrvsum  31716  ballotlemfmpn  31756  reprsuc  31890  bnj529  32016  bnj923  32043  bnj570  32181  bnj594  32188  bnj1173  32278  bnj1256  32291  bnj1259  32292  bnj1296  32297  bnj1498  32337  subfacp1lem1  32430  kur14lem7  32463  sat1el2xp  32630  mvrsval  32756  mvrsfpw  32757  mrsubcv  32761  mrsubccat  32769  msubff  32781  msrid  32796  msubvrs  32811  mppsval  32823  divcnvlin  32968  iprodefisumlem  32976  iprodefisum  32977  faclimlem1  32979  onsucsuccmpi  33795  bj-opelresdm  34441  bj-inftyexpitaudisj  34491  bj-inftyexpidisj  34496  bj-ccinftydisj  34499  bj-elccinfty  34500  finixpnum  34881  poimirlem5  34901  poimirlem6  34902  poimirlem7  34903  poimirlem8  34904  poimirlem9  34905  poimirlem10  34906  poimirlem11  34907  poimirlem12  34908  poimirlem13  34909  poimirlem14  34910  poimirlem15  34911  poimirlem16  34912  poimirlem17  34913  poimirlem18  34914  poimirlem19  34915  poimirlem20  34916  poimirlem21  34917  poimirlem22  34918  poimirlem29  34925  poimirlem30  34926  broucube  34930  volsupnfl  34941  dvasin  34982  dvacos  34983  sdclem2  35021  fdc  35024  heiborlem4  35096  heiborlem6  35098  smgrpismgmOLD  35144  mndoissmgrpOLD  35150  mndoisexid  35151  rngoueqz  35222  drngoi  35233  prjspertr  39261  prjsperref  39262  prjspersym  39263  prjspreln0  39265  prjspvs  39266  prjsprellsp  39267  jm2.23  39599  wepwsolem  39648  trclfvdecomr  40079  mnuprdlem1  40614  mnuprdlem2  40615  binomcxplemdvbinom  40691  binomcxplemnotnn0  40694  ssfiunibd  41582  climinf  41893  stoweidlem15  42307  fourierdlem66  42464  etransclem37  42563  smflimsuplem8  43108  eldmressn  43279  afvres  43378  ndmaovrcl  43410  sprsymrelfv  43663  fmtnofz04prm  43746  31prm  43767  2zrngamnd  44219  2zrngacmnd  44220  2zrngagrp  44221  2zrngALT  44226  2zrngnmlid  44227  2zrngnmlid2  44229  fldhmsubc  44362  fldhmsubcALTV  44380  lincvalsng  44478  snlindsntor  44533  lincresunit3lem2  44542  lincresunit3  44543  ldepsnlinc  44570  nn0sumshdiglemA  44686  nn0sumshdiglemB  44687  rrx2pnecoorneor  44709  rrx2linest  44736  rrx2linesl  44737