Theorem eleq2s 2858

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2815

This theorem is referenced by:  elrabi  3632  optocl  5719  optoclOLD  5720  ssrel  5733  eldmeldmressn  5984  predel  6279  fveqdmss  7026  oprabv  7423  elmpocl  7604  el2mpocsbcl  8031  bropopvvv  8036  bropfvvvv  8038  ressuppss  8130  mpoxeldm  8158  mpoxopn0yelv  8160  mpoxopxnop0  8162  tfr2a  8331  rdgseg  8358  2oconcl  8435  ecexr  8645  ectocld  8726  ecoptocl  8751  brecop2  8755  eroveu  8756  mapfvd  8824  mapsnconst  8837  mapfienlem1  9315  mapfienlem2  9316  mapfienlem3  9317  cantnflem2  9609  r1sucg  9691  r1suc  9692  acnrcl  9962  dfac5lem4  10046  dfac5lem4OLD  10048  fin23lem29  10261  fin23lem30  10262  axcclem  10377  alephval2  10493  0tsk  10676  0nsr  11000  peano2nn  12184  uzssz  12807  peano2uzs  12850  uzsupss  12888  fzssnn  13520  prednn0  13604  fzossnn0  13643  fldiv4p1lem1div2  13792  modaddid  13867  ltweuz  13921  fzennn  13928  ser1const  14018  expp1  14028  facnn  14235  facp1  14238  bcpasc  14281  hashfzo0  14390  tpfo  14460  ccatval2  14538  ccatass  14549  swrd00  14605  swrd0  14619  pfx00  14635  pfx0  14636  wrdeqs1cat  14680  splfv2a  14716  revccat  14726  rexuz3  15309  rexanuz2  15310  r19.2uz  15312  rexuzre  15313  cau4  15317  caubnd2  15318  climrlim2  15507  climshft2  15542  climaddc1  15595  climmulc2  15597  climsubc1  15598  climsubc2  15599  climlec2  15619  isercoll2  15629  climsup  15630  climcau  15631  caurcvg  15637  caurcvg2  15638  caucvg  15639  caucvgb  15640  iseraltlem1  15642  iseralt  15645  binomlem  15792  isumshft  15802  cvgrat  15846  clim2div  15852  ntrivcvg  15860  ntrivcvgtail  15863  fprodntriv  15905  fprodeq0  15938  fprodefsum  16058  pwp1fsum  16358  3prm  16661  phicl2  16736  phibndlem  16738  dfphi2  16742  crth  16746  vdwap0  16945  prmlem1a  17075  fvprif  17523  xpsfeq  17525  oppccofval  17680  homarcl2  18000  arwrcl  18009  pleval2i  18298  letsr  18557  gsumws1  18804  smndex1mndlem  18878  mulgnngsum  19053  mulgpropd  19090  psgnunilem2  19468  psgnprfval  19494  gexid  19554  efgmnvl  19687  efgrcl  19688  efgsval  19704  efgs1  19708  efgs1b  19709  frgpuptinv  19744  frgpup3lem  19750  lt6abl  19868  eldprd  19979  isunit  20351  isirred  20397  fldhmsubc  20764  abvrcl  20792  islss  20931  lbsss  21074  lbssp  21076  lbsind  21077  cssi  21666  thlle  21679  islbs4  21814  psrbagleadd1  21910  mpfrcl  22068  psr1basf  22193  coe1tm  22266  ply1frcl  22311  mavmulsolcl  22541  marepvcl  22559  1marepvmarrepid  22565  mdet0pr  22582  m2detleiblem1  22614  cramerimplem1  22673  cramerlem1  22677  chpscmat  22832  chpscmatgsumbin  22834  chpscmatgsummon  22835  ptpjpre1  23561  fin1aufil  23922  lmflf  23995  tsmsfbas  24118  xpsxmetlem  24369  xpsmet  24372  metustsym  24545  iscmet3lem3  25282  iscmet3lem1  25283  iscmet3lem2  25284  iscmet3  25285  rrxmvallem  25396  volsup  25548  opnmblALT  25595  itg1val  25675  tdeglem2  26051  ulmcaulem  26384  ulmcau  26385  ulmss  26387  pserdvlem2  26418  eff1olem  26537  logdmnrp  26630  dvlog2lem  26641  logtayl  26649  cxpcn3lem  26736  atancl  26870  atanval  26873  chp1  27155  ppiublem2  27191  lgsdir2lem2  27314  lgsdir2lem3  27315  lgsquadlem2  27369  2lgslem1b  27380  rplogsumlem1  27472  rplogsumlem2  27473  pntlemj  27591  nnne0s  28354  1vgrex  29096  edglnl  29237  usgredg2v  29321  umgrres1lem  29404  upgrres1  29407  nbupgrres  29458  clwlkwlk  29868  wwlksnextproplem1  30002  wwlksnextproplem2  30003  wwlksnextproplem3  30004  rusgrnumwwlkb0  30067  clwlkclwwlklem2a4  30092  eleclclwwlknlem1  30155  eleclclwwlknlem2  30156  erclwwlkneqlen  30163  erclwwlknref  30164  erclwwlknsym  30165  erclwwlkntr  30166  hashecclwwlkn1  30172  umgrhashecclwwlk  30173  frgrnbnb  30388  frgrwopreglem4  30410  frgrwopreglem5  30416  frgrwopreg  30418  numclwlk1  30466  vciOLD  30657  axhcompl-zf  31094  mayete3i  31824  pj3lem1  32302  fzto1stfv1  33189  fzto1st  33191  fzto1stinvn  33192  psgnfzto1st  33193  rmfsupp2  33326  erler  33353  selvply1rhmlemb  33710  vieta  33771  submat1n  33996  xrge0mulc1cn  34132  fiunelros  34365  elmbfmvol2  34458  fibp1  34592  rrvsum  34645  ballotlemfmpn  34686  reprsuc  34806  bnj529  34931  bnj923  34958  bnj570  35094  bnj594  35101  bnj1173  35191  bnj1256  35204  bnj1259  35205  bnj1296  35210  bnj1498  35250  fineqvnttrclselem1  35309  subfacp1lem1  35414  kur14lem7  35447  sat1el2xp  35614  mvrsval  35740  mvrsfpw  35741  mrsubcv  35745  mrsubccat  35753  msubff  35765  msrid  35780  msubvrs  35795  mppsval  35807  divcnvlin  35968  iprodefisumlem  35975  iprodefisum  35976  faclimlem1  35978  onsucsuccmpi  36678  bj-opelresdm  37512  bj-inftyexpitaudisj  37572  bj-inftyexpidisj  37577  bj-ccinftydisj  37580  bj-elccinfty  37581  finixpnum  37979  poimirlem5  37999  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem9  38003  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem13  38007  poimirlem14  38008  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem18  38012  poimirlem19  38013  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem29  38023  poimirlem30  38024  broucube  38028  volsupnfl  38039  dvasin  38078  dvacos  38079  sdclem2  38116  fdc  38119  heiborlem4  38188  heiborlem6  38190  smgrpismgmOLD  38236  mndoissmgrpOLD  38242  mndoisexid  38243  rngoueqz  38314  drngoi  38325  dfadjliftmap2  38831  dfblockliftmap2  38835  sucpre  38871  eldisjsim2  39309  redvmptabs  42844  mhphflem  43053  prjspertr  43062  prjsperref  43063  prjspersym  43064  prjspreln0  43066  prjspvs  43067  prjsprellsp  43068  jm2.23  43448  wepwsolem  43494  omabs2  43784  omcl3g  43786  trclfvdecomr  44179  mnuprdlem1  44723  mnuprdlem2  44724  binomcxplemdvbinom  44804  binomcxplemnotnn0  44807  orbitcl  45408  ssfiunibd  45764  climinf  46058  stoweidlem15  46465  fourierdlem66  46622  etransclem37  46721  smfsupmpt  47265  smfinfmpt  47269  smflimsuplem8  47277  eldmressn  47507  afvres  47642  ndmaovrcl  47674  2ltceilhalf  47802  minusmodnep2tmod  47829  modmknepk  47838  mod2addne  47840  modm2nep1  47842  modm1nep2  47844  modm1nem2  47845  modm1p1ne  47846  sprsymrelfv  47976  fmtnofz04prm  48062  31prm  48082  ppivalnnnprm  48113  indprmfz  48115  stgr0  48458  stgr1  48459  gpgiedgdmellem  48544  gpgvtx1  48552  gpgedgvtx1  48560  gpgedg2iv  48565  gpg5nbgrvtx13starlem2  48570  pgnbgreunbgrlem3  48616  pgnbgreunbgrlem6  48622  2zrngamnd  48745  2zrngacmnd  48746  2zrngagrp  48747  2zrngALT  48752  2zrngnmlid  48753  2zrngnmlid2  48755  fldhmsubcALTV  48831  lincvalsng  48914  snlindsntor  48969  lincresunit3lem2  48978  lincresunit3  48979  ldepsnlinc  49006  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118  rrx2pnecoorneor  49213  rrx2linest  49240  rrx2linesl  49241  isorcl  49530  catcrcl  49892  setc2othin  49963