Theorem eleq2s 2862

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  elrabi  3703  optocl  5794  ssrel  5806  eldmeldmressn  6054  predel  6353  fveqdmss  7112  oprabv  7510  elmpocl  7691  el2mpocsbcl  8126  bropopvvv  8131  bropfvvvv  8133  ressuppss  8224  mpoxeldm  8252  mpoxopn0yelv  8254  mpoxopxnop0  8256  tfr2a  8451  rdgseg  8478  2oconcl  8559  ecexr  8768  ectocld  8842  ecoptocl  8865  brecop2  8869  eroveu  8870  mapfvd  8937  mapsnconst  8950  mapfienlem1  9474  mapfienlem2  9475  mapfienlem3  9476  cantnflem2  9759  r1sucg  9838  r1suc  9839  acnrcl  10111  dfac5lem4  10195  dfac5lem4OLD  10197  fin23lem29  10410  fin23lem30  10411  axcclem  10526  alephval2  10641  0tsk  10824  0nsr  11148  peano2nn  12305  uzssz  12924  peano2uzs  12967  uzsupss  13005  fzssnn  13628  prednn0  13709  fzossnn0  13747  fldiv4p1lem1div2  13886  ltweuz  14012  fzennn  14019  ser1const  14109  expp1  14119  facnn  14324  facp1  14327  bcpasc  14370  hashfzo0  14479  tpfo  14549  ccatval2  14626  ccatass  14636  swrd00  14692  swrd0  14706  pfx00  14722  pfx0  14723  wrdeqs1cat  14768  splfv2a  14804  revccat  14814  rexuz3  15397  rexanuz2  15398  r19.2uz  15400  rexuzre  15401  cau4  15405  caubnd2  15406  climrlim2  15593  climshft2  15628  climaddc1  15681  climmulc2  15683  climsubc1  15684  climsubc2  15685  climlec2  15707  isercoll2  15717  climsup  15718  climcau  15719  caurcvg  15725  caurcvg2  15726  caucvg  15727  caucvgb  15728  iseraltlem1  15730  iseralt  15733  binomlem  15877  isumshft  15887  cvgrat  15931  clim2div  15937  ntrivcvg  15945  ntrivcvgtail  15948  fprodntriv  15990  fprodeq0  16023  fprodefsum  16143  pwp1fsum  16439  3prm  16741  phicl2  16815  phibndlem  16817  dfphi2  16821  crth  16825  vdwap0  17023  prmlem1a  17154  fvprif  17621  xpsfeq  17623  oppccofval  17775  homarcl2  18102  arwrcl  18111  pleval2i  18406  letsr  18663  gsumws1  18873  smndex1mndlem  18944  mulgnngsum  19119  mulgpropd  19156  psgnunilem2  19537  psgnprfval  19563  gexid  19623  efgmnvl  19756  efgrcl  19757  efgsval  19773  efgs1  19777  efgs1b  19778  frgpuptinv  19813  frgpup3lem  19819  lt6abl  19937  eldprd  20048  isunit  20399  isirred  20445  fldhmsubc  20808  abvrcl  20836  islss  20955  lbsss  21099  lbssp  21101  lbsind  21102  cssi  21725  thlle  21739  thlleOLD  21740  islbs4  21875  psrbagleadd1  21971  mpfrcl  22132  psr1basf  22224  coe1tm  22297  ply1frcl  22343  mavmulsolcl  22578  marepvcl  22596  1marepvmarrepid  22602  mdet0pr  22619  m2detleiblem1  22651  cramerimplem1  22710  cramerlem1  22714  chpscmat  22869  chpscmatgsumbin  22871  chpscmatgsummon  22872  ptpjpre1  23600  fin1aufil  23961  lmflf  24034  tsmsfbas  24157  xpsxmetlem  24410  xpsmet  24413  metustsym  24589  iscmet3lem3  25343  iscmet3lem1  25344  iscmet3lem2  25345  iscmet3  25346  rrxmvallem  25457  volsup  25610  opnmblALT  25657  itg1val  25737  tdeglem2  26120  ulmcaulem  26455  ulmcau  26456  ulmss  26458  pserdvlem2  26490  eff1olem  26608  logdmnrp  26701  dvlog2lem  26712  logtayl  26720  cxpcn3lem  26808  atancl  26942  atanval  26945  chp1  27228  ppiublem2  27265  lgsdir2lem2  27388  lgsdir2lem3  27389  lgsquadlem2  27443  2lgslem1b  27454  rplogsumlem1  27546  rplogsumlem2  27547  pntlemj  27665  nnne0s  28358  1vgrex  29037  edglnl  29178  usgredg2v  29262  umgrres1lem  29345  upgrres1  29348  nbupgrres  29399  clwlkwlk  29811  wwlksnextproplem1  29942  wwlksnextproplem2  29943  wwlksnextproplem3  29944  rusgrnumwwlkb0  30004  clwlkclwwlklem2a4  30029  eleclclwwlknlem1  30092  eleclclwwlknlem2  30093  erclwwlkneqlen  30100  erclwwlknref  30101  erclwwlknsym  30102  erclwwlkntr  30103  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  frgrnbnb  30325  frgrwopreglem4  30347  frgrwopreglem5  30353  frgrwopreg  30355  numclwlk1  30403  vciOLD  30593  axhcompl-zf  31030  mayete3i  31760  pj3lem1  32238  fzto1stfv1  33094  fzto1st  33096  fzto1stinvn  33097  psgnfzto1st  33098  rmfsupp2  33218  erler  33237  submat1n  33751  xrge0mulc1cn  33887  fiunelros  34138  elmbfmvol2  34232  fibp1  34366  rrvsum  34419  ballotlemfmpn  34459  reprsuc  34592  bnj529  34717  bnj923  34744  bnj570  34881  bnj594  34888  bnj1173  34978  bnj1256  34991  bnj1259  34992  bnj1296  34997  bnj1498  35037  subfacp1lem1  35147  kur14lem7  35180  sat1el2xp  35347  mvrsval  35473  mvrsfpw  35474  mrsubcv  35478  mrsubccat  35486  msubff  35498  msrid  35513  msubvrs  35528  mppsval  35540  divcnvlin  35695  iprodefisumlem  35702  iprodefisum  35703  faclimlem1  35705  onsucsuccmpi  36409  bj-opelresdm  37111  bj-inftyexpitaudisj  37171  bj-inftyexpidisj  37176  bj-ccinftydisj  37179  bj-elccinfty  37180  finixpnum  37565  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem9  37589  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem29  37609  poimirlem30  37610  broucube  37614  volsupnfl  37625  dvasin  37664  dvacos  37665  sdclem2  37702  fdc  37705  heiborlem4  37774  heiborlem6  37776  smgrpismgmOLD  37822  mndoissmgrpOLD  37828  mndoisexid  37829  rngoueqz  37900  drngoi  37911  mhphflem  42551  prjspertr  42560  prjsperref  42561  prjspersym  42562  prjspreln0  42564  prjspvs  42565  prjsprellsp  42566  jm2.23  42953  wepwsolem  42999  omabs2  43294  omcl3g  43296  trclfvdecomr  43690  mnuprdlem1  44241  mnuprdlem2  44242  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  ssfiunibd  45224  climinf  45527  stoweidlem15  45936  fourierdlem66  46093  etransclem37  46192  smfsupmpt  46736  smflimsuplem8  46748  eldmressn  46952  afvres  47087  ndmaovrcl  47119  sprsymrelfv  47368  fmtnofz04prm  47451  31prm  47471  uspgrimprop  47757  2zrngamnd  47970  2zrngacmnd  47971  2zrngagrp  47972  2zrngALT  47977  2zrngnmlid  47978  2zrngnmlid2  47980  fldhmsubcALTV  48056  lincvalsng  48145  snlindsntor  48200  lincresunit3lem2  48209  lincresunit3  48210  ldepsnlinc  48237  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  rrx2pnecoorneor  48449  rrx2linest  48476  rrx2linesl  48477  setc2othin  48723