Theorem eleq2s 2846

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  elrabi  3645  optocl  5717  optoclOLD  5718  ssrel  5730  eldmeldmressn  5980  predel  6273  fveqdmss  7016  oprabv  7413  elmpocl  7594  el2mpocsbcl  8025  bropopvvv  8030  bropfvvvv  8032  ressuppss  8123  mpoxeldm  8151  mpoxopn0yelv  8153  mpoxopxnop0  8155  tfr2a  8324  rdgseg  8351  2oconcl  8428  ecexr  8637  ectocld  8716  ecoptocl  8741  brecop2  8745  eroveu  8746  mapfvd  8813  mapsnconst  8826  mapfienlem1  9314  mapfienlem2  9315  mapfienlem3  9316  cantnflem2  9605  r1sucg  9684  r1suc  9685  acnrcl  9955  dfac5lem4  10039  dfac5lem4OLD  10041  fin23lem29  10254  fin23lem30  10255  axcclem  10370  alephval2  10485  0tsk  10668  0nsr  10992  peano2nn  12158  uzssz  12774  peano2uzs  12821  uzsupss  12859  fzssnn  13489  prednn0  13573  fzossnn0  13611  fldiv4p1lem1div2  13757  modaddid  13832  ltweuz  13886  fzennn  13893  ser1const  13983  expp1  13993  facnn  14200  facp1  14203  bcpasc  14246  hashfzo0  14355  tpfo  14425  ccatval2  14503  ccatass  14513  swrd00  14569  swrd0  14583  pfx00  14599  pfx0  14600  wrdeqs1cat  14644  splfv2a  14680  revccat  14690  rexuz3  15274  rexanuz2  15275  r19.2uz  15277  rexuzre  15278  cau4  15282  caubnd2  15283  climrlim2  15472  climshft2  15507  climaddc1  15560  climmulc2  15562  climsubc1  15563  climsubc2  15564  climlec2  15584  isercoll2  15594  climsup  15595  climcau  15596  caurcvg  15602  caurcvg2  15603  caucvg  15604  caucvgb  15605  iseraltlem1  15607  iseralt  15610  binomlem  15754  isumshft  15764  cvgrat  15808  clim2div  15814  ntrivcvg  15822  ntrivcvgtail  15825  fprodntriv  15867  fprodeq0  15900  fprodefsum  16020  pwp1fsum  16320  3prm  16623  phicl2  16697  phibndlem  16699  dfphi2  16703  crth  16707  vdwap0  16906  prmlem1a  17036  fvprif  17483  xpsfeq  17485  oppccofval  17640  homarcl2  17960  arwrcl  17969  pleval2i  18258  letsr  18517  gsumws1  18730  smndex1mndlem  18801  mulgnngsum  18976  mulgpropd  19013  psgnunilem2  19392  psgnprfval  19418  gexid  19478  efgmnvl  19611  efgrcl  19612  efgsval  19628  efgs1  19632  efgs1b  19633  frgpuptinv  19668  frgpup3lem  19674  lt6abl  19792  eldprd  19903  isunit  20276  isirred  20322  fldhmsubc  20688  abvrcl  20716  islss  20855  lbsss  20999  lbssp  21001  lbsind  21002  cssi  21609  thlle  21622  islbs4  21757  psrbagleadd1  21853  mpfrcl  22008  psr1basf  22102  coe1tm  22175  ply1frcl  22221  mavmulsolcl  22454  marepvcl  22472  1marepvmarrepid  22478  mdet0pr  22495  m2detleiblem1  22527  cramerimplem1  22586  cramerlem1  22590  chpscmat  22745  chpscmatgsumbin  22747  chpscmatgsummon  22748  ptpjpre1  23474  fin1aufil  23835  lmflf  23908  tsmsfbas  24031  xpsxmetlem  24283  xpsmet  24286  metustsym  24459  iscmet3lem3  25206  iscmet3lem1  25207  iscmet3lem2  25208  iscmet3  25209  rrxmvallem  25320  volsup  25473  opnmblALT  25520  itg1val  25600  tdeglem2  25982  ulmcaulem  26319  ulmcau  26320  ulmss  26322  pserdvlem2  26354  eff1olem  26473  logdmnrp  26566  dvlog2lem  26577  logtayl  26585  cxpcn3lem  26673  atancl  26807  atanval  26810  chp1  27093  ppiublem2  27130  lgsdir2lem2  27253  lgsdir2lem3  27254  lgsquadlem2  27308  2lgslem1b  27319  rplogsumlem1  27411  rplogsumlem2  27412  pntlemj  27530  nnne0s  28252  1vgrex  28965  edglnl  29106  usgredg2v  29190  umgrres1lem  29273  upgrres1  29276  nbupgrres  29327  clwlkwlk  29738  wwlksnextproplem1  29872  wwlksnextproplem2  29873  wwlksnextproplem3  29874  rusgrnumwwlkb0  29934  clwlkclwwlklem2a4  29959  eleclclwwlknlem1  30022  eleclclwwlknlem2  30023  erclwwlkneqlen  30030  erclwwlknref  30031  erclwwlknsym  30032  erclwwlkntr  30033  hashecclwwlkn1  30039  umgrhashecclwwlk  30040  frgrnbnb  30255  frgrwopreglem4  30277  frgrwopreglem5  30283  frgrwopreg  30285  numclwlk1  30333  vciOLD  30523  axhcompl-zf  30960  mayete3i  31690  pj3lem1  32168  fzto1stfv1  33056  fzto1st  33058  fzto1stinvn  33059  psgnfzto1st  33060  rmfsupp2  33188  erler  33215  submat1n  33771  xrge0mulc1cn  33907  fiunelros  34140  elmbfmvol2  34234  fibp1  34368  rrvsum  34421  ballotlemfmpn  34462  reprsuc  34582  bnj529  34707  bnj923  34734  bnj570  34871  bnj594  34878  bnj1173  34968  bnj1256  34981  bnj1259  34982  bnj1296  34987  bnj1498  35027  subfacp1lem1  35151  kur14lem7  35184  sat1el2xp  35351  mvrsval  35477  mvrsfpw  35478  mrsubcv  35482  mrsubccat  35490  msubff  35502  msrid  35517  msubvrs  35532  mppsval  35544  divcnvlin  35705  iprodefisumlem  35712  iprodefisum  35713  faclimlem1  35715  onsucsuccmpi  36416  bj-opelresdm  37118  bj-inftyexpitaudisj  37178  bj-inftyexpidisj  37183  bj-ccinftydisj  37186  bj-elccinfty  37187  finixpnum  37584  poimirlem5  37604  poimirlem6  37605  poimirlem7  37606  poimirlem8  37607  poimirlem9  37608  poimirlem10  37609  poimirlem11  37610  poimirlem12  37611  poimirlem13  37612  poimirlem14  37613  poimirlem15  37614  poimirlem16  37615  poimirlem17  37616  poimirlem18  37617  poimirlem19  37618  poimirlem20  37619  poimirlem21  37620  poimirlem22  37621  poimirlem29  37628  poimirlem30  37629  broucube  37633  volsupnfl  37644  dvasin  37683  dvacos  37684  sdclem2  37721  fdc  37724  heiborlem4  37793  heiborlem6  37795  smgrpismgmOLD  37841  mndoissmgrpOLD  37847  mndoisexid  37848  rngoueqz  37919  drngoi  37930  redvmptabs  42333  mhphflem  42569  prjspertr  42578  prjsperref  42579  prjspersym  42580  prjspreln0  42582  prjspvs  42583  prjsprellsp  42584  jm2.23  42969  wepwsolem  43015  omabs2  43305  omcl3g  43307  trclfvdecomr  43701  mnuprdlem1  44245  mnuprdlem2  44246  binomcxplemdvbinom  44326  binomcxplemnotnn0  44329  orbitcl  44931  ssfiunibd  45291  climinf  45588  stoweidlem15  45997  fourierdlem66  46154  etransclem37  46253  smfsupmpt  46797  smfinfmpt  46801  smflimsuplem8  46809  eldmressn  47022  afvres  47157  ndmaovrcl  47189  2ltceilhalf  47313  minusmodnep2tmod  47338  modmknepk  47347  mod2addne  47349  modm2nep1  47351  modm1nep2  47353  modm1nem2  47354  modm1p1ne  47355  sprsymrelfv  47479  fmtnofz04prm  47562  31prm  47582  stgr0  47945  stgr1  47946  gpgiedgdmellem  48031  gpgvtx1  48039  gpgedgvtx1  48047  gpgedg2iv  48052  gpg5nbgrvtx13starlem2  48057  pgnbgreunbgrlem3  48103  pgnbgreunbgrlem6  48109  2zrngamnd  48232  2zrngacmnd  48233  2zrngagrp  48234  2zrngALT  48239  2zrngnmlid  48240  2zrngnmlid2  48242  fldhmsubcALTV  48318  lincvalsng  48402  snlindsntor  48457  lincresunit3lem2  48466  lincresunit3  48467  ldepsnlinc  48494  nn0sumshdiglemA  48605  nn0sumshdiglemB  48606  rrx2pnecoorneor  48701  rrx2linest  48728  rrx2linesl  48729  isorcl  49019  catcrcl  49381  setc2othin  49452