Theorem eleq2s 2849

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  elrabi  3643  optocl  5710  optoclOLD  5711  ssrel  5723  eldmeldmressn  5974  predel  6268  fveqdmss  7011  oprabv  7406  elmpocl  7587  el2mpocsbcl  8015  bropopvvv  8020  bropfvvvv  8022  ressuppss  8113  mpoxeldm  8141  mpoxopn0yelv  8143  mpoxopxnop0  8145  tfr2a  8314  rdgseg  8341  2oconcl  8418  ecexr  8627  ectocld  8706  ecoptocl  8731  brecop2  8735  eroveu  8736  mapfvd  8803  mapsnconst  8816  mapfienlem1  9289  mapfienlem2  9290  mapfienlem3  9291  cantnflem2  9580  r1sucg  9659  r1suc  9660  acnrcl  9930  dfac5lem4  10014  dfac5lem4OLD  10016  fin23lem29  10229  fin23lem30  10230  axcclem  10345  alephval2  10460  0tsk  10643  0nsr  10967  peano2nn  12134  uzssz  12750  peano2uzs  12797  uzsupss  12835  fzssnn  13465  prednn0  13549  fzossnn0  13587  fldiv4p1lem1div2  13736  modaddid  13811  ltweuz  13865  fzennn  13872  ser1const  13962  expp1  13972  facnn  14179  facp1  14182  bcpasc  14225  hashfzo0  14334  tpfo  14404  ccatval2  14482  ccatass  14493  swrd00  14549  swrd0  14563  pfx00  14579  pfx0  14580  wrdeqs1cat  14624  splfv2a  14660  revccat  14670  rexuz3  15253  rexanuz2  15254  r19.2uz  15256  rexuzre  15257  cau4  15261  caubnd2  15262  climrlim2  15451  climshft2  15486  climaddc1  15539  climmulc2  15541  climsubc1  15542  climsubc2  15543  climlec2  15563  isercoll2  15573  climsup  15574  climcau  15575  caurcvg  15581  caurcvg2  15582  caucvg  15583  caucvgb  15584  iseraltlem1  15586  iseralt  15589  binomlem  15733  isumshft  15743  cvgrat  15787  clim2div  15793  ntrivcvg  15801  ntrivcvgtail  15804  fprodntriv  15846  fprodeq0  15879  fprodefsum  15999  pwp1fsum  16299  3prm  16602  phicl2  16676  phibndlem  16678  dfphi2  16682  crth  16686  vdwap0  16885  prmlem1a  17015  fvprif  17462  xpsfeq  17464  oppccofval  17619  homarcl2  17939  arwrcl  17948  pleval2i  18237  letsr  18496  gsumws1  18743  smndex1mndlem  18814  mulgnngsum  18989  mulgpropd  19026  psgnunilem2  19405  psgnprfval  19431  gexid  19491  efgmnvl  19624  efgrcl  19625  efgsval  19641  efgs1  19645  efgs1b  19646  frgpuptinv  19681  frgpup3lem  19687  lt6abl  19805  eldprd  19916  isunit  20289  isirred  20335  fldhmsubc  20698  abvrcl  20726  islss  20865  lbsss  21009  lbssp  21011  lbsind  21012  cssi  21619  thlle  21632  islbs4  21767  psrbagleadd1  21863  mpfrcl  22018  psr1basf  22112  coe1tm  22185  ply1frcl  22231  mavmulsolcl  22464  marepvcl  22482  1marepvmarrepid  22488  mdet0pr  22505  m2detleiblem1  22537  cramerimplem1  22596  cramerlem1  22600  chpscmat  22755  chpscmatgsumbin  22757  chpscmatgsummon  22758  ptpjpre1  23484  fin1aufil  23845  lmflf  23918  tsmsfbas  24041  xpsxmetlem  24292  xpsmet  24295  metustsym  24468  iscmet3lem3  25215  iscmet3lem1  25216  iscmet3lem2  25217  iscmet3  25218  rrxmvallem  25329  volsup  25482  opnmblALT  25529  itg1val  25609  tdeglem2  25991  ulmcaulem  26328  ulmcau  26329  ulmss  26331  pserdvlem2  26363  eff1olem  26482  logdmnrp  26575  dvlog2lem  26586  logtayl  26594  cxpcn3lem  26682  atancl  26816  atanval  26819  chp1  27102  ppiublem2  27139  lgsdir2lem2  27262  lgsdir2lem3  27263  lgsquadlem2  27317  2lgslem1b  27328  rplogsumlem1  27420  rplogsumlem2  27421  pntlemj  27539  nnne0s  28263  1vgrex  28978  edglnl  29119  usgredg2v  29203  umgrres1lem  29286  upgrres1  29289  nbupgrres  29340  clwlkwlk  29751  wwlksnextproplem1  29885  wwlksnextproplem2  29886  wwlksnextproplem3  29887  rusgrnumwwlkb0  29947  clwlkclwwlklem2a4  29972  eleclclwwlknlem1  30035  eleclclwwlknlem2  30036  erclwwlkneqlen  30043  erclwwlknref  30044  erclwwlknsym  30045  erclwwlkntr  30046  hashecclwwlkn1  30052  umgrhashecclwwlk  30053  frgrnbnb  30268  frgrwopreglem4  30290  frgrwopreglem5  30296  frgrwopreg  30298  numclwlk1  30346  vciOLD  30536  axhcompl-zf  30973  mayete3i  31703  pj3lem1  32181  fzto1stfv1  33065  fzto1st  33067  fzto1stinvn  33068  psgnfzto1st  33069  rmfsupp2  33200  erler  33227  submat1n  33813  xrge0mulc1cn  33949  fiunelros  34182  elmbfmvol2  34275  fibp1  34409  rrvsum  34462  ballotlemfmpn  34503  reprsuc  34623  bnj529  34748  bnj923  34775  bnj570  34912  bnj594  34919  bnj1173  35009  bnj1256  35022  bnj1259  35023  bnj1296  35028  bnj1498  35068  fineqvnttrclselem1  35129  subfacp1lem1  35211  kur14lem7  35244  sat1el2xp  35411  mvrsval  35537  mvrsfpw  35538  mrsubcv  35542  mrsubccat  35550  msubff  35562  msrid  35577  msubvrs  35592  mppsval  35604  divcnvlin  35765  iprodefisumlem  35772  iprodefisum  35773  faclimlem1  35775  onsucsuccmpi  36476  bj-opelresdm  37178  bj-inftyexpitaudisj  37238  bj-inftyexpidisj  37243  bj-ccinftydisj  37246  bj-elccinfty  37247  finixpnum  37644  poimirlem5  37664  poimirlem6  37665  poimirlem7  37666  poimirlem8  37667  poimirlem9  37668  poimirlem10  37669  poimirlem11  37670  poimirlem12  37671  poimirlem13  37672  poimirlem14  37673  poimirlem15  37674  poimirlem16  37675  poimirlem17  37676  poimirlem18  37677  poimirlem19  37678  poimirlem20  37679  poimirlem21  37680  poimirlem22  37681  poimirlem29  37688  poimirlem30  37689  broucube  37693  volsupnfl  37704  dvasin  37743  dvacos  37744  sdclem2  37781  fdc  37784  heiborlem4  37853  heiborlem6  37855  smgrpismgmOLD  37901  mndoissmgrpOLD  37907  mndoisexid  37908  rngoueqz  37979  drngoi  37990  redvmptabs  42392  mhphflem  42628  prjspertr  42637  prjsperref  42638  prjspersym  42639  prjspreln0  42641  prjspvs  42642  prjsprellsp  42643  jm2.23  43028  wepwsolem  43074  omabs2  43364  omcl3g  43366  trclfvdecomr  43760  mnuprdlem1  44304  mnuprdlem2  44305  binomcxplemdvbinom  44385  binomcxplemnotnn0  44388  orbitcl  44989  ssfiunibd  45349  climinf  45645  stoweidlem15  46052  fourierdlem66  46209  etransclem37  46308  smfsupmpt  46852  smfinfmpt  46856  smflimsuplem8  46864  eldmressn  47067  afvres  47202  ndmaovrcl  47234  2ltceilhalf  47358  minusmodnep2tmod  47383  modmknepk  47392  mod2addne  47394  modm2nep1  47396  modm1nep2  47398  modm1nem2  47399  modm1p1ne  47400  sprsymrelfv  47524  fmtnofz04prm  47607  31prm  47627  stgr0  47990  stgr1  47991  gpgiedgdmellem  48076  gpgvtx1  48084  gpgedgvtx1  48092  gpgedg2iv  48097  gpg5nbgrvtx13starlem2  48102  pgnbgreunbgrlem3  48148  pgnbgreunbgrlem6  48154  2zrngamnd  48277  2zrngacmnd  48278  2zrngagrp  48279  2zrngALT  48284  2zrngnmlid  48285  2zrngnmlid2  48287  fldhmsubcALTV  48363  lincvalsng  48447  snlindsntor  48502  lincresunit3lem2  48511  lincresunit3  48512  ldepsnlinc  48539  nn0sumshdiglemA  48650  nn0sumshdiglemB  48651  rrx2pnecoorneor  48746  rrx2linest  48773  rrx2linesl  48774  isorcl  49064  catcrcl  49426  setc2othin  49497