Theorem eleq2s 2879

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836

This theorem is referenced by:  elrabi  3646  optocl  5739  optoclOLD  5740  ssrel  5753  eldmeldmressn  6009  predel  6304  fveqdmss  7055  oprabv  7452  elmpocl  7633  el2mpocsbcl  8059  bropopvvv  8064  bropfvvvv  8066  ressuppss  8158  mpoxeldm  8186  mpoxopn0yelv  8188  mpoxopxnop0  8190  tfr2a  8361  rdgseg  8388  2oconcl  8467  ecexr  8678  ectocld  8759  ecoptocl  8784  brecop2  8788  eroveu  8789  mapfvd  8857  mapsnconst  8870  mapfienlem1  9348  mapfienlem2  9349  mapfienlem3  9350  cantnflem2  9642  r1sucg  9724  r1suc  9725  acnrcl  9995  dfac5lem4  10079  dfac5lem4OLD  10081  fin23lem29  10295  fin23lem30  10296  axcclem  10411  alephval2  10527  0tsk  10710  0nsr  11034  peano2nn  12219  uzssz  12857  peano2uzs  12900  uzsupss  12938  fzssnn  13570  prednn0  13654  fzossnn0  13693  fldiv4p1lem1div2  13842  modaddid  13917  ltweuz  13971  fzennn  13978  ser1const  14068  expp1  14078  facnn  14285  facp1  14288  bcpasc  14331  hashfzo0  14440  tpfo  14510  ccatval2  14588  ccatass  14599  swrd00  14655  swrd0  14669  pfx00  14685  pfx0  14686  wrdeqs1cat  14730  splfv2a  14766  revccat  14776  rexuz3  15359  rexanuz2  15360  r19.2uz  15362  rexuzre  15363  cau4  15367  caubnd2  15368  climrlim2  15557  climshft2  15592  climaddc1  15645  climmulc2  15647  climsubc1  15648  climsubc2  15649  climlec2  15669  isercoll2  15679  climsup  15680  climcau  15681  caurcvg  15687  caurcvg2  15688  caucvg  15689  caucvgb  15690  iseraltlem1  15692  iseralt  15695  binomlem  15842  isumshft  15852  cvgrat  15896  clim2div  15902  ntrivcvg  15910  ntrivcvgtail  15913  fprodntriv  15955  fprodeq0  15988  fprodefsum  16108  pwp1fsum  16408  3prm  16711  phicl2  16786  phibndlem  16788  dfphi2  16792  crth  16796  vdwap0  16995  prmlem1a  17125  fvprif  17574  xpsfeq  17576  oppccofval  17731  homarcl2  18051  arwrcl  18060  pleval2i  18349  letsr  18608  gsumws1  18855  smndex1mndlem  18929  mulgnngsum  19104  mulgpropd  19141  psgnunilem2  19518  psgnprfval  19544  gexid  19604  efgmnvl  19737  efgrcl  19738  efgsval  19754  efgs1  19758  efgs1b  19759  frgpuptinv  19794  frgpup3lem  19800  lt6abl  19918  eldprd  20029  isunit  20401  isirred  20447  fldhmsubc  20814  abvrcl  20842  islss  20981  lbsss  21124  lbssp  21126  lbsind  21127  cssi  21716  thlle  21729  islbs4  21864  psrbagleadd1  21960  mpfrcl  22118  psr1basf  22243  coe1tm  22316  ply1frcl  22361  mavmulsolcl  22591  marepvcl  22609  1marepvmarrepid  22615  mdet0pr  22632  m2detleiblem1  22664  cramerimplem1  22723  cramerlem1  22727  chpscmat  22882  chpscmatgsumbin  22884  chpscmatgsummon  22885  ptpjpre1  23611  fin1aufil  23972  lmflf  24045  tsmsfbas  24168  xpsxmetlem  24419  xpsmet  24422  metustsym  24595  iscmet3lem3  25332  iscmet3lem1  25333  iscmet3lem2  25334  iscmet3  25335  rrxmvallem  25446  volsup  25598  opnmblALT  25645  itg1val  25725  tdeglem2  26101  ulmcaulem  26434  ulmcau  26435  ulmss  26437  pserdvlem2  26468  eff1olem  26590  logdmnrp  26683  dvlog2lem  26694  logtayl  26702  cxpcn3lem  26789  atancl  26923  atanval  26926  chp1  27208  ppiublem2  27244  lgsdir2lem2  27367  lgsdir2lem3  27368  lgsquadlem2  27422  2lgslem1b  27433  rplogsumlem1  27525  rplogsumlem2  27526  pntlemj  27644  nnne0s  28407  1vgrex  29149  edglnl  29290  usgredg2v  29374  umgrres1lem  29457  upgrres1  29460  nbupgrres  29511  clwlkwlk  29921  wwlksnextproplem1  30055  wwlksnextproplem2  30056  wwlksnextproplem3  30057  rusgrnumwwlkb0  30120  clwlkclwwlklem2a4  30145  eleclclwwlknlem1  30208  eleclclwwlknlem2  30209  erclwwlkneqlen  30216  erclwwlknref  30217  erclwwlknsym  30218  erclwwlkntr  30219  hashecclwwlkn1  30225  umgrhashecclwwlk  30226  frgrnbnb  30441  frgrwopreglem4  30463  frgrwopreglem5  30469  frgrwopreg  30471  numclwlk1  30519  vciOLD  30710  axhcompl-zf  31147  mayete3i  31877  pj3lem1  32355  fzto1stfv1  33242  fzto1st  33244  fzto1stinvn  33245  psgnfzto1st  33246  rmfsupp2  33379  erler  33407  selvply1rhmlemb  33777  vieta  33838  submat1n  34063  xrge0mulc1cn  34199  fiunelros  34432  elmbfmvol2  34525  fibp1  34659  rrvsum  34712  ballotlemfmpn  34753  reprsuc  34873  bnj529  35001  bnj923  35028  bnj570  35164  bnj594  35171  bnj1173  35261  bnj1256  35274  bnj1259  35275  bnj1296  35280  bnj1498  35320  fineqvnttrclselem1  35381  subfacp1lem1  35493  kur14lem7  35526  sat1el2xp  35693  mvrsval  35819  mvrsfpw  35820  mrsubcv  35824  mrsubccat  35832  msubff  35844  msrid  35859  msubvrs  35874  mppsval  35886  divcnvlin  36047  iprodefisumlem  36054  iprodefisum  36055  faclimlem1  36057  onsucsuccmpi  36767  bj-opelresdm  37601  bj-inftyexpitaudisj  37661  bj-inftyexpidisj  37666  bj-ccinftydisj  37669  bj-elccinfty  37670  finixpnum  38068  poimirlem5  38088  poimirlem6  38089  poimirlem7  38090  poimirlem8  38091  poimirlem9  38092  poimirlem10  38093  poimirlem11  38094  poimirlem12  38095  poimirlem13  38096  poimirlem14  38097  poimirlem15  38098  poimirlem16  38099  poimirlem17  38100  poimirlem18  38101  poimirlem19  38102  poimirlem20  38103  poimirlem21  38104  poimirlem22  38105  poimirlem29  38112  poimirlem30  38113  broucube  38117  volsupnfl  38128  dvasin  38167  dvacos  38168  sdclem2  38205  fdc  38208  heiborlem4  38277  heiborlem6  38279  smgrpismgmOLD  38325  mndoissmgrpOLD  38331  mndoisexid  38332  rngoueqz  38403  drngoi  38414  dfadjliftmap2  38920  dfblockliftmap2  38924  sucpre  38960  eldisjsim2  39398  redvmptabs  42933  mhphflem  43142  prjspertr  43151  prjsperref  43152  prjspersym  43153  prjspreln0  43155  prjspvs  43156  prjsprellsp  43157  jm2.23  43537  wepwsolem  43583  omabs2  43873  omcl3g  43875  trclfvdecomr  44268  mnuprdlem1  44812  mnuprdlem2  44813  binomcxplemdvbinom  44893  binomcxplemnotnn0  44896  orbitcl  45497  ssfiunibd  45852  climinf  46146  stoweidlem15  46553  fourierdlem66  46710  etransclem37  46809  smfsupmpt  47353  smfinfmpt  47357  smflimsuplem8  47365  eldmressn  47595  afvres  47730  ndmaovrcl  47762  2ltceilhalf  47890  minusmodnep2tmod  47917  modmknepk  47926  mod2addne  47928  modm2nep1  47930  modm1nep2  47932  modm1nem2  47933  modm1p1ne  47934  sprsymrelfv  48064  fmtnofz04prm  48150  31prm  48170  ppivalnnnprm  48201  indprmfz  48203  stgr0  48546  stgr1  48547  gpgiedgdmellem  48632  gpgvtx1  48640  gpgedgvtx1  48648  gpgedg2iv  48653  gpg5nbgrvtx13starlem2  48658  pgnbgreunbgrlem3  48704  pgnbgreunbgrlem6  48710  2zrngamnd  48833  2zrngacmnd  48834  2zrngagrp  48835  2zrngALT  48840  2zrngnmlid  48841  2zrngnmlid2  48843  fldhmsubcALTV  48919  lincvalsng  49002  snlindsntor  49057  lincresunit3lem2  49066  lincresunit3  49067  ldepsnlinc  49094  nn0sumshdiglemA  49205  nn0sumshdiglemB  49206  rrx2pnecoorneor  49301  rrx2linest  49328  rrx2linesl  49329  isorcl  49618  catcrcl  49980  setc2othin  50051