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  3631  optocl  5718  optoclOLD  5719  ssrel  5732  eldmeldmressn  5984  predel  6279  fveqdmss  7024  oprabv  7420  elmpocl  7601  el2mpocsbcl  8028  bropopvvv  8033  bropfvvvv  8035  ressuppss  8126  mpoxeldm  8154  mpoxopn0yelv  8156  mpoxopxnop0  8158  tfr2a  8327  rdgseg  8354  2oconcl  8431  ecexr  8641  ectocld  8722  ecoptocl  8747  brecop2  8751  eroveu  8752  mapfvd  8820  mapsnconst  8833  mapfienlem1  9311  mapfienlem2  9312  mapfienlem3  9313  cantnflem2  9602  r1sucg  9684  r1suc  9685  acnrcl  9955  dfac5lem4  10039  dfac5lem4OLD  10041  fin23lem29  10254  fin23lem30  10255  axcclem  10370  alephval2  10486  0tsk  10669  0nsr  10993  peano2nn  12177  uzssz  12800  peano2uzs  12843  uzsupss  12881  fzssnn  13513  prednn0  13597  fzossnn0  13636  fldiv4p1lem1div2  13785  modaddid  13860  ltweuz  13914  fzennn  13921  ser1const  14011  expp1  14021  facnn  14228  facp1  14231  bcpasc  14274  hashfzo0  14383  tpfo  14453  ccatval2  14531  ccatass  14542  swrd00  14598  swrd0  14612  pfx00  14628  pfx0  14629  wrdeqs1cat  14673  splfv2a  14709  revccat  14719  rexuz3  15302  rexanuz2  15303  r19.2uz  15305  rexuzre  15306  cau4  15310  caubnd2  15311  climrlim2  15500  climshft2  15535  climaddc1  15588  climmulc2  15590  climsubc1  15591  climsubc2  15592  climlec2  15612  isercoll2  15622  climsup  15623  climcau  15624  caurcvg  15630  caurcvg2  15631  caucvg  15632  caucvgb  15633  iseraltlem1  15635  iseralt  15638  binomlem  15785  isumshft  15795  cvgrat  15839  clim2div  15845  ntrivcvg  15853  ntrivcvgtail  15856  fprodntriv  15898  fprodeq0  15931  fprodefsum  16051  pwp1fsum  16351  3prm  16654  phicl2  16729  phibndlem  16731  dfphi2  16735  crth  16739  vdwap0  16938  prmlem1a  17068  fvprif  17516  xpsfeq  17518  oppccofval  17673  homarcl2  17993  arwrcl  18002  pleval2i  18291  letsr  18550  gsumws1  18797  smndex1mndlem  18871  mulgnngsum  19046  mulgpropd  19083  psgnunilem2  19461  psgnprfval  19487  gexid  19547  efgmnvl  19680  efgrcl  19681  efgsval  19697  efgs1  19701  efgs1b  19702  frgpuptinv  19737  frgpup3lem  19743  lt6abl  19861  eldprd  19972  isunit  20344  isirred  20390  fldhmsubc  20753  abvrcl  20781  islss  20920  lbsss  21064  lbssp  21066  lbsind  21067  cssi  21674  thlle  21687  islbs4  21822  psrbagleadd1  21918  mpfrcl  22073  psr1basf  22175  coe1tm  22248  ply1frcl  22293  mavmulsolcl  22526  marepvcl  22544  1marepvmarrepid  22550  mdet0pr  22567  m2detleiblem1  22599  cramerimplem1  22658  cramerlem1  22662  chpscmat  22817  chpscmatgsumbin  22819  chpscmatgsummon  22820  ptpjpre1  23546  fin1aufil  23907  lmflf  23980  tsmsfbas  24103  xpsxmetlem  24354  xpsmet  24357  metustsym  24530  iscmet3lem3  25267  iscmet3lem1  25268  iscmet3lem2  25269  iscmet3  25270  rrxmvallem  25381  volsup  25533  opnmblALT  25580  itg1val  25660  tdeglem2  26036  ulmcaulem  26372  ulmcau  26373  ulmss  26375  pserdvlem2  26406  eff1olem  26525  logdmnrp  26618  dvlog2lem  26629  logtayl  26637  cxpcn3lem  26724  atancl  26858  atanval  26861  chp1  27144  ppiublem2  27180  lgsdir2lem2  27303  lgsdir2lem3  27304  lgsquadlem2  27358  2lgslem1b  27369  rplogsumlem1  27461  rplogsumlem2  27462  pntlemj  27580  nnne0s  28343  1vgrex  29085  edglnl  29226  usgredg2v  29310  umgrres1lem  29393  upgrres1  29396  nbupgrres  29447  clwlkwlk  29858  wwlksnextproplem1  29992  wwlksnextproplem2  29993  wwlksnextproplem3  29994  rusgrnumwwlkb0  30057  clwlkclwwlklem2a4  30082  eleclclwwlknlem1  30145  eleclclwwlknlem2  30146  erclwwlkneqlen  30153  erclwwlknref  30154  erclwwlknsym  30155  erclwwlkntr  30156  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  frgrnbnb  30378  frgrwopreglem4  30400  frgrwopreglem5  30406  frgrwopreg  30408  numclwlk1  30456  vciOLD  30647  axhcompl-zf  31084  mayete3i  31814  pj3lem1  32292  fzto1stfv1  33177  fzto1st  33179  fzto1stinvn  33180  psgnfzto1st  33181  rmfsupp2  33314  erler  33341  vieta  33739  submat1n  33965  xrge0mulc1cn  34101  fiunelros  34334  elmbfmvol2  34427  fibp1  34561  rrvsum  34614  ballotlemfmpn  34655  reprsuc  34775  bnj529  34900  bnj923  34927  bnj570  35063  bnj594  35070  bnj1173  35160  bnj1256  35173  bnj1259  35174  bnj1296  35179  bnj1498  35219  fineqvnttrclselem1  35281  subfacp1lem1  35377  kur14lem7  35410  sat1el2xp  35577  mvrsval  35703  mvrsfpw  35704  mrsubcv  35708  mrsubccat  35716  msubff  35728  msrid  35743  msubvrs  35758  mppsval  35770  divcnvlin  35931  iprodefisumlem  35938  iprodefisum  35939  faclimlem1  35941  onsucsuccmpi  36641  bj-opelresdm  37475  bj-inftyexpitaudisj  37535  bj-inftyexpidisj  37540  bj-ccinftydisj  37543  bj-elccinfty  37544  finixpnum  37940  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem9  37964  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem13  37968  poimirlem14  37969  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem29  37984  poimirlem30  37985  broucube  37989  volsupnfl  38000  dvasin  38039  dvacos  38040  sdclem2  38077  fdc  38080  heiborlem4  38149  heiborlem6  38151  smgrpismgmOLD  38197  mndoissmgrpOLD  38203  mndoisexid  38204  rngoueqz  38275  drngoi  38286  dfadjliftmap2  38792  dfblockliftmap2  38796  sucpre  38832  eldisjsim2  39270  redvmptabs  42806  mhphflem  43043  prjspertr  43052  prjsperref  43053  prjspersym  43054  prjspreln0  43056  prjspvs  43057  prjsprellsp  43058  jm2.23  43442  wepwsolem  43488  omabs2  43778  omcl3g  43780  trclfvdecomr  44173  mnuprdlem1  44717  mnuprdlem2  44718  binomcxplemdvbinom  44798  binomcxplemnotnn0  44801  orbitcl  45402  ssfiunibd  45760  climinf  46054  stoweidlem15  46461  fourierdlem66  46618  etransclem37  46717  smfsupmpt  47261  smfinfmpt  47265  smflimsuplem8  47273  eldmressn  47497  afvres  47632  ndmaovrcl  47664  2ltceilhalf  47792  minusmodnep2tmod  47819  modmknepk  47828  mod2addne  47830  modm2nep1  47832  modm1nep2  47834  modm1nem2  47835  modm1p1ne  47836  sprsymrelfv  47966  fmtnofz04prm  48052  31prm  48072  ppivalnnnprm  48103  indprmfz  48105  stgr0  48448  stgr1  48449  gpgiedgdmellem  48534  gpgvtx1  48542  gpgedgvtx1  48550  gpgedg2iv  48555  gpg5nbgrvtx13starlem2  48560  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem6  48612  2zrngamnd  48735  2zrngacmnd  48736  2zrngagrp  48737  2zrngALT  48742  2zrngnmlid  48743  2zrngnmlid2  48745  fldhmsubcALTV  48821  lincvalsng  48904  snlindsntor  48959  lincresunit3lem2  48968  lincresunit3  48969  ldepsnlinc  48996  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  rrx2pnecoorneor  49203  rrx2linest  49230  rrx2linesl  49231  isorcl  49520  catcrcl  49882  setc2othin  49953