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 220	1 ⊢ (𝐴 ∈ 𝐶 → 𝜑)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  elrabi  3641  optocl  5745  optoclOLD  5746  ssrel  5759  eldmeldmressn  6016  imadifssran  6195  predel  6317  fveqdmss  7070  oprabv  7472  elmpocl  7654  el2mpocsbcl  8085  bropopvvv  8090  bropfvvvv  8092  ressuppss  8184  mpoxeldm  8212  mpoxopn0yelv  8214  mpoxopxnop0  8216  tfr2a  8387  rdgseg  8414  2oconcl  8495  ecexr  8706  ectocld  8787  ecoptocl  8812  brecop2  8816  eroveu  8817  mapfvd  8891  mapsnconst  8904  mapfienlem1  9381  mapfienlem2  9382  mapfienlem3  9383  cantnflem2  9675  r1sucg  9759  r1suc  9760  karden  9940  acnrcl  10102  dfac5lem4  10186  fin23lem29  10400  fin23lem30  10401  axcclem  10516  alephval2  10638  0tsk  10821  0nsr  11145  peano2nn  12328  uzssz  12967  peano2uzs  13010  uzsupss  13048  fzssnn  13682  prednn0  13766  fzossnn0  13805  fldiv4p1lem1div2  13955  modaddid  14030  ltweuz  14084  fzennn  14091  ser1const  14181  expp1  14191  facnn  14399  facp1  14402  bcpasc  14445  hashfzo0  14555  tpfo  14625  ccatval2  14703  ccatass  14714  swrd00  14772  swrd0  14788  pfx00  14804  pfx0  14805  wrdeqs1cat  14849  splfv2a  14885  revccat  14895  rexuz3  15496  rexanuz2  15497  r19.2uz  15499  rexuzre  15500  cau4  15504  caubnd2  15505  climrlim2  15694  climshft2  15729  climaddc1  15782  climmulc2  15784  climsubc1  15785  climsubc2  15786  climlec2  15806  isercoll2  15816  climsup  15817  climcau  15818  caurcvg  15824  caurcvg2  15825  caucvg  15826  caucvgb  15827  iseraltlem1  15829  iseralt  15832  binomlem  15978  isumshft  15988  cvgrat  16032  clim2div  16038  ntrivcvg  16046  ntrivcvgtail  16049  fprodntriv  16089  fprodeq0  16122  fprodefsum  16241  pwp1fsum  16541  3prm  16849  phicl2  16925  phibndlem  16927  dfphi2  16931  crth  16935  vdwap0  17134  prmlem1a  17264  fvprif  17713  xpsfeq  17715  oppccofval  17870  homarcl2  18190  arwrcl  18199  pleval2i  18488  letsr  18747  gsumws1  19014  smndex1mndlem  19088  mulgnngsum  19269  mulgpropd  19306  psgnunilem2  19689  psgnprfval  19715  gexid  19775  efgmnvl  19908  efgrcl  19909  efgsval  19925  efgs1  19929  efgs1b  19930  frgpuptinv  19965  frgpup3lem  19971  lt6abl  20089  eldprd  20200  isunit  20583  isirred  20629  fldhmsubc  21022  abvrcl  21050  islss  21189  lbsss  21332  lbssp  21334  lbsind  21335  cssi  21970  thlle  21983  islbs4  22118  psrbagleadd1  22216  mpfrcl  22374  psr1basf  22499  coe1tm  22572  ply1frcl  22616  mavmulsolcl  22846  marepvcl  22864  1marepvmarrepid  22870  mdet0pr  22887  m2detleiblem1  22919  cramerimplem1  22981  cramerlem1  22985  chpscmat  23140  chpscmatgsumbin  23142  chpscmatgsummon  23143  ptpjpre1  23870  fin1aufil  24231  lmflf  24304  tsmsfbas  24427  xpsxmetlem  24678  xpsmet  24681  metustsym  24854  iscmet3lem3  25591  iscmet3lem1  25592  iscmet3lem2  25593  iscmet3  25594  rrxmvallem  25705  volsup  25857  opnmblALT  25904  itg1val  25984  tdeglem2  26359  ulmcaulem  26703  ulmcau  26704  ulmss  26706  pserdvlem2  26737  eff1olem  26858  logdmnrp  26951  dvlog2lem  26962  logtayl  26970  cxpcn3lem  27057  atancl  27191  atanval  27194  chp1  27476  ppiublem2  27512  lgsdir2lem2  27635  lgsdir2lem3  27636  lgsquadlem2  27690  2lgslem1b  27701  rplogsumlem1  27793  rplogsumlem2  27794  pntlemj  27912  nnne0s  28705  1vgrex  29562  edglnl  29703  usgredg2v  29790  umgrres1lem  29873  upgrres1  29876  nbupgrres  29927  clwlkwlk  30344  wwlksnextproplem1  30480  wwlksnextproplem2  30481  wwlksnextproplem3  30482  rusgrnumwwlkb0  30545  clwlkclwwlklem2a4  30570  eleclclwwlknlem1  30633  eleclclwwlknlem2  30634  erclwwlkneqlen  30641  erclwwlknref  30642  erclwwlknsym  30643  erclwwlkntr  30644  hashecclwwlkn1  30650  umgrhashecclwwlk  30651  frgrnbnb  30876  frgrwopreglem4  30898  frgrwopreglem5  30904  frgrwopreg  30906  numclwlk1  30954  vciOLD  31145  axhcompl-zf  31582  mayete3i  32312  pj3lem1  32790  fzto1stfv1  33644  fzto1st  33646  fzto1stinvn  33647  psgnfzto1st  33648  rmfsupp2  33780  erler  33808  selvply1rhmlemb  34133  vieta  34194  submat1n  34419  xrge0mulc1cn  34555  fiunelros  34789  elmbfmvol2  34882  fibp1  35016  rrvsum  35069  ballotlemfmpn  35110  reprsuc  35227  bnj529  35355  bnj923  35382  bnj570  35518  bnj594  35525  bnj1173  35615  bnj1256  35628  bnj1259  35629  bnj1296  35634  bnj1498  35674  rankfo  35714  fineqvnttrclselem1  35762  subfacp1lem1  35913  kur14lem7  35946  sat1el2xp  36113  mvrsval  36239  mvrsfpw  36240  mrsubcv  36244  mrsubccat  36252  msubff  36264  msrid  36279  msubvrs  36294  mppsval  36306  divcnvlin  36467  iprodefisumlem  36474  iprodefisum  36475  faclimlem1  36477  onsucsuccmpi  37201  bj-opelresdm  38034  bj-inftyexpitaudisj  38094  bj-inftyexpidisj  38099  bj-ccinftydisj  38102  bj-elccinfty  38103  finixpnum  38496  poimirlem5  38511  poimirlem6  38512  poimirlem7  38513  poimirlem8  38514  poimirlem9  38515  poimirlem10  38516  poimirlem11  38517  poimirlem12  38518  poimirlem13  38519  poimirlem14  38520  poimirlem15  38521  poimirlem16  38522  poimirlem17  38523  poimirlem18  38524  poimirlem19  38525  poimirlem20  38526  poimirlem21  38527  poimirlem22  38528  poimirlem29  38535  poimirlem30  38536  broucube  38540  volsupnfl  38551  dvasin  38590  dvacos  38591  sdclem2  38644  fdc  38647  heiborlem4  38716  heiborlem6  38718  smgrpismgmOLD  38764  mndoissmgrpOLD  38770  mndoisexid  38771  rngoueqz  38842  drngoi  38853  dfadjliftmap2  39357  dfblockliftmap2  39361  sucpre  39397  eldisjsim2  39835  redvmptabs  43379  mhphflem  43586  prjspertr  43595  prjsperref  43596  prjspersym  43597  prjspreln0  43599  prjspvs  43600  prjsprellsp  43601  jm2.23  43956  wepwsolem  44002  omabs2  44292  omcl3g  44294  trclfvdecomr  44687  mnuprdlem1  45215  mnuprdlem2  45216  binomcxplemdvbinom  45296  binomcxplemnotnn0  45299  orbitcl  45899  ssfiunibd  46268  climinf  46562  stoweidlem15  46969  fourierdlem66  47126  etransclem37  47225  smfsupmpt  47769  smfinfmpt  47773  smflimsuplem8  47781  eldmressn  48051  afvres  48186  ndmaovrcl  48218  2ltceilhalf  48346  minusmodnep2tmod  48373  modmknepk  48382  mod2addne  48384  modm2nep1  48386  modm1nep2  48388  modm1nem2  48389  modm1p1ne  48390  sprsymrelfv  48520  fmtnofz04prm  48606  31prm  48626  ppivalnnnprm  48657  indprmfz  48659  stgr0  49002  stgr1  49003  gpgiedgdmellem  49088  gpgvtx1  49096  gpgedgvtx1  49104  gpgedg2iv  49109  gpg5nbgrvtx13starlem2  49114  pgnbgreunbgrlem3  49160  pgnbgreunbgrlem6  49166  2zrngamnd  49288  2zrngacmnd  49289  2zrngagrp  49290  2zrngALT  49295  2zrngnmlid  49296  2zrngnmlid2  49298  fldhmsubcALTV  49374  lincvalsng  49472  snlindsntor  49527  lincresunit3lem2  49536  lincresunit3  49537  ldepsnlinc  49564  nn0sumshdiglemA  49675  nn0sumshdiglemB  49676  rrx2pnecoorneor  49771  rrx2linest  49798  rrx2linesl  49799  isorcl  50085  catcrcl  50447  setc2othin  50518