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  3654  optocl  5733  ssrel  5745  eldmeldmressn  5996  predel  6294  fveqdmss  7050  oprabv  7449  elmpocl  7630  el2mpocsbcl  8064  bropopvvv  8069  bropfvvvv  8071  ressuppss  8162  mpoxeldm  8190  mpoxopn0yelv  8192  mpoxopxnop0  8194  tfr2a  8363  rdgseg  8390  2oconcl  8467  ecexr  8676  ectocld  8755  ecoptocl  8780  brecop2  8784  eroveu  8785  mapfvd  8852  mapsnconst  8865  mapfienlem1  9356  mapfienlem2  9357  mapfienlem3  9358  cantnflem2  9643  r1sucg  9722  r1suc  9723  acnrcl  9995  dfac5lem4  10079  dfac5lem4OLD  10081  fin23lem29  10294  fin23lem30  10295  axcclem  10410  alephval2  10525  0tsk  10708  0nsr  11032  peano2nn  12198  uzssz  12814  peano2uzs  12861  uzsupss  12899  fzssnn  13529  prednn0  13613  fzossnn0  13651  fldiv4p1lem1div2  13797  modaddid  13872  ltweuz  13926  fzennn  13933  ser1const  14023  expp1  14033  facnn  14240  facp1  14243  bcpasc  14286  hashfzo0  14395  tpfo  14465  ccatval2  14543  ccatass  14553  swrd00  14609  swrd0  14623  pfx00  14639  pfx0  14640  wrdeqs1cat  14685  splfv2a  14721  revccat  14731  rexuz3  15315  rexanuz2  15316  r19.2uz  15318  rexuzre  15319  cau4  15323  caubnd2  15324  climrlim2  15513  climshft2  15548  climaddc1  15601  climmulc2  15603  climsubc1  15604  climsubc2  15605  climlec2  15625  isercoll2  15635  climsup  15636  climcau  15637  caurcvg  15643  caurcvg2  15644  caucvg  15645  caucvgb  15646  iseraltlem1  15648  iseralt  15651  binomlem  15795  isumshft  15805  cvgrat  15849  clim2div  15855  ntrivcvg  15863  ntrivcvgtail  15866  fprodntriv  15908  fprodeq0  15941  fprodefsum  16061  pwp1fsum  16361  3prm  16664  phicl2  16738  phibndlem  16740  dfphi2  16744  crth  16748  vdwap0  16947  prmlem1a  17077  fvprif  17524  xpsfeq  17526  oppccofval  17677  homarcl2  17997  arwrcl  18006  pleval2i  18295  letsr  18552  gsumws1  18765  smndex1mndlem  18836  mulgnngsum  19011  mulgpropd  19048  psgnunilem2  19425  psgnprfval  19451  gexid  19511  efgmnvl  19644  efgrcl  19645  efgsval  19661  efgs1  19665  efgs1b  19666  frgpuptinv  19701  frgpup3lem  19707  lt6abl  19825  eldprd  19936  isunit  20282  isirred  20328  fldhmsubc  20694  abvrcl  20722  islss  20840  lbsss  20984  lbssp  20986  lbsind  20987  cssi  21593  thlle  21606  islbs4  21741  psrbagleadd1  21837  mpfrcl  21992  psr1basf  22086  coe1tm  22159  ply1frcl  22205  mavmulsolcl  22438  marepvcl  22456  1marepvmarrepid  22462  mdet0pr  22479  m2detleiblem1  22511  cramerimplem1  22570  cramerlem1  22574  chpscmat  22729  chpscmatgsumbin  22731  chpscmatgsummon  22732  ptpjpre1  23458  fin1aufil  23819  lmflf  23892  tsmsfbas  24015  xpsxmetlem  24267  xpsmet  24270  metustsym  24443  iscmet3lem3  25190  iscmet3lem1  25191  iscmet3lem2  25192  iscmet3  25193  rrxmvallem  25304  volsup  25457  opnmblALT  25504  itg1val  25584  tdeglem2  25966  ulmcaulem  26303  ulmcau  26304  ulmss  26306  pserdvlem2  26338  eff1olem  26457  logdmnrp  26550  dvlog2lem  26561  logtayl  26569  cxpcn3lem  26657  atancl  26791  atanval  26794  chp1  27077  ppiublem2  27114  lgsdir2lem2  27237  lgsdir2lem3  27238  lgsquadlem2  27292  2lgslem1b  27303  rplogsumlem1  27395  rplogsumlem2  27396  pntlemj  27514  nnne0s  28229  1vgrex  28929  edglnl  29070  usgredg2v  29154  umgrres1lem  29237  upgrres1  29240  nbupgrres  29291  clwlkwlk  29705  wwlksnextproplem1  29839  wwlksnextproplem2  29840  wwlksnextproplem3  29841  rusgrnumwwlkb0  29901  clwlkclwwlklem2a4  29926  eleclclwwlknlem1  29989  eleclclwwlknlem2  29990  erclwwlkneqlen  29997  erclwwlknref  29998  erclwwlknsym  29999  erclwwlkntr  30000  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  frgrnbnb  30222  frgrwopreglem4  30244  frgrwopreglem5  30250  frgrwopreg  30252  numclwlk1  30300  vciOLD  30490  axhcompl-zf  30927  mayete3i  31657  pj3lem1  32135  fzto1stfv1  33058  fzto1st  33060  fzto1stinvn  33061  psgnfzto1st  33062  rmfsupp2  33189  erler  33216  submat1n  33795  xrge0mulc1cn  33931  fiunelros  34164  elmbfmvol2  34258  fibp1  34392  rrvsum  34445  ballotlemfmpn  34486  reprsuc  34606  bnj529  34731  bnj923  34758  bnj570  34895  bnj594  34902  bnj1173  34992  bnj1256  35005  bnj1259  35006  bnj1296  35011  bnj1498  35051  subfacp1lem1  35166  kur14lem7  35199  sat1el2xp  35366  mvrsval  35492  mvrsfpw  35493  mrsubcv  35497  mrsubccat  35505  msubff  35517  msrid  35532  msubvrs  35547  mppsval  35559  divcnvlin  35720  iprodefisumlem  35727  iprodefisum  35728  faclimlem1  35730  onsucsuccmpi  36431  bj-opelresdm  37133  bj-inftyexpitaudisj  37193  bj-inftyexpidisj  37198  bj-ccinftydisj  37201  bj-elccinfty  37202  finixpnum  37599  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem29  37643  poimirlem30  37644  broucube  37648  volsupnfl  37659  dvasin  37698  dvacos  37699  sdclem2  37736  fdc  37739  heiborlem4  37808  heiborlem6  37810  smgrpismgmOLD  37856  mndoissmgrpOLD  37862  mndoisexid  37863  rngoueqz  37934  drngoi  37945  redvmptabs  42348  mhphflem  42584  prjspertr  42593  prjsperref  42594  prjspersym  42595  prjspreln0  42597  prjspvs  42598  prjsprellsp  42599  jm2.23  42985  wepwsolem  43031  omabs2  43321  omcl3g  43323  trclfvdecomr  43717  mnuprdlem1  44261  mnuprdlem2  44262  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  orbitcl  44947  ssfiunibd  45307  climinf  45604  stoweidlem15  46013  fourierdlem66  46170  etransclem37  46269  smfsupmpt  46813  smfinfmpt  46817  smflimsuplem8  46825  eldmressn  47038  afvres  47173  ndmaovrcl  47205  2ltceilhalf  47329  minusmodnep2tmod  47354  modmknepk  47363  mod2addne  47365  modm2nep1  47367  modm1nep2  47369  modm1nem2  47370  modm1p1ne  47371  sprsymrelfv  47495  fmtnofz04prm  47578  31prm  47598  stgr0  47959  stgr1  47960  gpgiedgdmellem  48037  gpgvtx1  48045  gpgedgvtx1  48053  gpgedg2iv  48058  gpg5nbgrvtx13starlem2  48063  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem6  48114  2zrngamnd  48235  2zrngacmnd  48236  2zrngagrp  48237  2zrngALT  48242  2zrngnmlid  48243  2zrngnmlid2  48245  fldhmsubcALTV  48321  lincvalsng  48405  snlindsntor  48460  lincresunit3lem2  48469  lincresunit3  48470  ldepsnlinc  48497  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  rrx2pnecoorneor  48704  rrx2linest  48731  rrx2linesl  48732  isorcl  49022  catcrcl  49384  setc2othin  49455