Theorem eleq2s 2855

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  elrabi  3644  optocl  5726  optoclOLD  5727  ssrel  5740  eldmeldmressn  5992  predel  6287  fveqdmss  7032  oprabv  7428  elmpocl  7609  el2mpocsbcl  8037  bropopvvv  8042  bropfvvvv  8044  ressuppss  8135  mpoxeldm  8163  mpoxopn0yelv  8165  mpoxopxnop0  8167  tfr2a  8336  rdgseg  8363  2oconcl  8440  ecexr  8650  ectocld  8731  ecoptocl  8756  brecop2  8760  eroveu  8761  mapfvd  8829  mapsnconst  8842  mapfienlem1  9320  mapfienlem2  9321  mapfienlem3  9322  cantnflem2  9611  r1sucg  9693  r1suc  9694  acnrcl  9964  dfac5lem4  10048  dfac5lem4OLD  10050  fin23lem29  10263  fin23lem30  10264  axcclem  10379  alephval2  10495  0tsk  10678  0nsr  11002  peano2nn  12169  uzssz  12784  peano2uzs  12827  uzsupss  12865  fzssnn  13496  prednn0  13580  fzossnn0  13618  fldiv4p1lem1div2  13767  modaddid  13842  ltweuz  13896  fzennn  13903  ser1const  13993  expp1  14003  facnn  14210  facp1  14213  bcpasc  14256  hashfzo0  14365  tpfo  14435  ccatval2  14513  ccatass  14524  swrd00  14580  swrd0  14594  pfx00  14610  pfx0  14611  wrdeqs1cat  14655  splfv2a  14691  revccat  14701  rexuz3  15284  rexanuz2  15285  r19.2uz  15287  rexuzre  15288  cau4  15292  caubnd2  15293  climrlim2  15482  climshft2  15517  climaddc1  15570  climmulc2  15572  climsubc1  15573  climsubc2  15574  climlec2  15594  isercoll2  15604  climsup  15605  climcau  15606  caurcvg  15612  caurcvg2  15613  caucvg  15614  caucvgb  15615  iseraltlem1  15617  iseralt  15620  binomlem  15764  isumshft  15774  cvgrat  15818  clim2div  15824  ntrivcvg  15832  ntrivcvgtail  15835  fprodntriv  15877  fprodeq0  15910  fprodefsum  16030  pwp1fsum  16330  3prm  16633  phicl2  16707  phibndlem  16709  dfphi2  16713  crth  16717  vdwap0  16916  prmlem1a  17046  fvprif  17494  xpsfeq  17496  oppccofval  17651  homarcl2  17971  arwrcl  17980  pleval2i  18269  letsr  18528  gsumws1  18775  smndex1mndlem  18846  mulgnngsum  19021  mulgpropd  19058  psgnunilem2  19436  psgnprfval  19462  gexid  19522  efgmnvl  19655  efgrcl  19656  efgsval  19672  efgs1  19676  efgs1b  19677  frgpuptinv  19712  frgpup3lem  19718  lt6abl  19836  eldprd  19947  isunit  20321  isirred  20367  fldhmsubc  20730  abvrcl  20758  islss  20897  lbsss  21041  lbssp  21043  lbsind  21044  cssi  21651  thlle  21664  islbs4  21799  psrbagleadd1  21896  mpfrcl  22052  psr1basf  22154  coe1tm  22227  ply1frcl  22274  mavmulsolcl  22507  marepvcl  22525  1marepvmarrepid  22531  mdet0pr  22548  m2detleiblem1  22580  cramerimplem1  22639  cramerlem1  22643  chpscmat  22798  chpscmatgsumbin  22800  chpscmatgsummon  22801  ptpjpre1  23527  fin1aufil  23888  lmflf  23961  tsmsfbas  24084  xpsxmetlem  24335  xpsmet  24338  metustsym  24511  iscmet3lem3  25258  iscmet3lem1  25259  iscmet3lem2  25260  iscmet3  25261  rrxmvallem  25372  volsup  25525  opnmblALT  25572  itg1val  25652  tdeglem2  26034  ulmcaulem  26371  ulmcau  26372  ulmss  26374  pserdvlem2  26406  eff1olem  26525  logdmnrp  26618  dvlog2lem  26629  logtayl  26637  cxpcn3lem  26725  atancl  26859  atanval  26862  chp1  27145  ppiublem2  27182  lgsdir2lem2  27305  lgsdir2lem3  27306  lgsquadlem2  27360  2lgslem1b  27371  rplogsumlem1  27463  rplogsumlem2  27464  pntlemj  27582  nnne0s  28345  1vgrex  29087  edglnl  29228  usgredg2v  29312  umgrres1lem  29395  upgrres1  29398  nbupgrres  29449  clwlkwlk  29860  wwlksnextproplem1  29994  wwlksnextproplem2  29995  wwlksnextproplem3  29996  rusgrnumwwlkb0  30059  clwlkclwwlklem2a4  30084  eleclclwwlknlem1  30147  eleclclwwlknlem2  30148  erclwwlkneqlen  30155  erclwwlknref  30156  erclwwlknsym  30157  erclwwlkntr  30158  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  frgrnbnb  30380  frgrwopreglem4  30402  frgrwopreglem5  30408  frgrwopreg  30410  numclwlk1  30458  vciOLD  30648  axhcompl-zf  31085  mayete3i  31815  pj3lem1  32293  fzto1stfv1  33194  fzto1st  33196  fzto1stinvn  33197  psgnfzto1st  33198  rmfsupp2  33331  erler  33358  vieta  33756  submat1n  33982  xrge0mulc1cn  34118  fiunelros  34351  elmbfmvol2  34444  fibp1  34578  rrvsum  34631  ballotlemfmpn  34672  reprsuc  34792  bnj529  34917  bnj923  34944  bnj570  35080  bnj594  35087  bnj1173  35177  bnj1256  35190  bnj1259  35191  bnj1296  35196  bnj1498  35236  fineqvnttrclselem1  35296  subfacp1lem1  35392  kur14lem7  35425  sat1el2xp  35592  mvrsval  35718  mvrsfpw  35719  mrsubcv  35723  mrsubccat  35731  msubff  35743  msrid  35758  msubvrs  35773  mppsval  35785  divcnvlin  35946  iprodefisumlem  35953  iprodefisum  35954  faclimlem1  35956  onsucsuccmpi  36656  bj-opelresdm  37394  bj-inftyexpitaudisj  37454  bj-inftyexpidisj  37459  bj-ccinftydisj  37462  bj-elccinfty  37463  finixpnum  37850  poimirlem5  37870  poimirlem6  37871  poimirlem7  37872  poimirlem8  37873  poimirlem9  37874  poimirlem10  37875  poimirlem11  37876  poimirlem12  37877  poimirlem13  37878  poimirlem14  37879  poimirlem15  37880  poimirlem16  37881  poimirlem17  37882  poimirlem18  37883  poimirlem19  37884  poimirlem20  37885  poimirlem21  37886  poimirlem22  37887  poimirlem29  37894  poimirlem30  37895  broucube  37899  volsupnfl  37910  dvasin  37949  dvacos  37950  sdclem2  37987  fdc  37990  heiborlem4  38059  heiborlem6  38061  smgrpismgmOLD  38107  mndoissmgrpOLD  38113  mndoisexid  38114  rngoueqz  38185  drngoi  38196  dfadjliftmap2  38702  dfblockliftmap2  38706  sucpre  38742  eldisjsim2  39180  redvmptabs  42724  mhphflem  42948  prjspertr  42957  prjsperref  42958  prjspersym  42959  prjspreln0  42961  prjspvs  42962  prjsprellsp  42963  jm2.23  43347  wepwsolem  43393  omabs2  43683  omcl3g  43685  trclfvdecomr  44078  mnuprdlem1  44622  mnuprdlem2  44623  binomcxplemdvbinom  44703  binomcxplemnotnn0  44706  orbitcl  45307  ssfiunibd  45665  climinf  45960  stoweidlem15  46367  fourierdlem66  46524  etransclem37  46623  smfsupmpt  47167  smfinfmpt  47171  smflimsuplem8  47179  eldmressn  47391  afvres  47526  ndmaovrcl  47558  2ltceilhalf  47682  minusmodnep2tmod  47707  modmknepk  47716  mod2addne  47718  modm2nep1  47720  modm1nep2  47722  modm1nem2  47723  modm1p1ne  47724  sprsymrelfv  47848  fmtnofz04prm  47931  31prm  47951  stgr0  48314  stgr1  48315  gpgiedgdmellem  48400  gpgvtx1  48408  gpgedgvtx1  48416  gpgedg2iv  48421  gpg5nbgrvtx13starlem2  48426  pgnbgreunbgrlem3  48472  pgnbgreunbgrlem6  48478  2zrngamnd  48601  2zrngacmnd  48602  2zrngagrp  48603  2zrngALT  48608  2zrngnmlid  48609  2zrngnmlid2  48611  fldhmsubcALTV  48687  lincvalsng  48770  snlindsntor  48825  lincresunit3lem2  48834  lincresunit3  48835  ldepsnlinc  48862  nn0sumshdiglemA  48973  nn0sumshdiglemB  48974  rrx2pnecoorneor  49069  rrx2linest  49096  rrx2linesl  49097  isorcl  49386  catcrcl  49748  setc2othin  49819