Theorem eleq2s 2882

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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

This theorem is used by:  elrabi  3644  optocl  5751  optoclOLD  5752  ssrel  5765  eldmeldmressn  6027  imadifssranOLD  6216  predel  6345  fveqdmss  7105  oprabv  7506  elmpocl  7689  el2mpocsbcl  8124  bropopvvv  8129  bropfvvvv  8131  ressuppss  8231  mpoxeldm  8259  mpoxopn0yelv  8261  mpoxopxnop0  8263  tfr2a  8434  rdgseg  8461  2oconcl  8542  ecexr  8753  ectocld  8834  ecoptocl  8859  brecop2  8863  eroveu  8864  mapfvd  8938  mapsnconst  8951  mapfienlem1  9427  mapfienlem2  9428  mapfienlem3  9429  cantnflem2  9721  r1sucg  9806  r1suc  9807  karden  9989  acnrcl  10151  dfac5lem4  10235  fin23lem29  10449  fin23lem30  10450  axcclem  10565  alephval2  10687  0tsk  10870  0nsr  11194  peano2nn  12377  uzssz  13016  peano2uzs  13059  uzsupss  13097  fzssnn  13732  prednn0  13816  fzossnn0  13855  fldiv4p1lem1div2  14005  modaddid  14080  ltweuz  14134  fzennn  14141  ser1const  14231  expp1  14241  facnn  14449  facp1  14452  bcpasc  14495  hashfzo0  14605  tpfo  14675  ccatval2  14753  ccatass  14764  swrd00  14823  swrd0  14839  pfx00  14855  pfx0  14856  wrdeqs1cat  14900  splfv2a  14936  revccat  14946  rexuz3  15548  rexanuz2  15549  r19.2uz  15551  rexuzre  15552  cau4  15556  caubnd2  15557  climrlim2  15746  climshft2  15781  climaddc1  15834  climmulc2  15836  climsubc1  15837  climsubc2  15838  climlec2  15858  isercoll2  15868  climsup  15869  climcau  15870  caurcvg  15876  caurcvg2  15877  caucvg  15878  caucvgb  15879  iseraltlem1  15881  iseralt  15884  binomlem  16030  isumshft  16040  cvgrat  16084  clim2div  16090  ntrivcvg  16098  ntrivcvgtail  16101  fprodntriv  16141  fprodeq0  16174  fprodefsum  16293  pwp1fsum  16593  3prm  16901  phicl2  16977  phibndlem  16979  dfphi2  16983  crth  16987  vdwap0  17186  prmlem1a  17316  fvprif  17765  xpsfeq  17767  oppccofval  17922  homarcl2  18242  arwrcl  18251  pleval2i  18540  letsr  18799  gsumws1  19066  smndex1mndlem  19140  mulgnngsum  19321  mulgpropd  19358  psgnunilem2  19742  psgnprfval  19768  gexid  19828  efgmnvl  19961  efgrcl  19962  efgsval  19978  efgs1  19982  efgs1b  19983  frgpuptinv  20018  frgpup3lem  20024  lt6abl  20142  eldprd  20253  isunit  20636  isirred  20682  fldhmsubc  21075  abvrcl  21103  islss  21242  lbsss  21385  lbssp  21387  lbsind  21388  cssi  22023  thlle  22036  islbs4  22171  psrbagleadd1  22269  mpfrcl  22427  psr1basf  22552  coe1tm  22625  ply1frcl  22669  mavmulsolcl  22899  marepvcl  22917  1marepvmarrepid  22923  mdet0pr  22940  m2detleiblem1  22972  cramerimplem1  23034  cramerlem1  23038  chpscmat  23193  chpscmatgsumbin  23195  chpscmatgsummon  23196  ptpjpre1  23923  fin1aufil  24284  lmflf  24357  tsmsfbas  24480  xpsxmetlem  24731  xpsmet  24734  metustsym  24907  iscmet3lem3  25644  iscmet3lem1  25645  iscmet3lem2  25646  iscmet3  25647  rrxmvallem  25758  volsup  25910  opnmblALT  25957  itg1val  26037  tdeglem2  26412  ulmcaulem  26754  ulmcau  26755  ulmss  26757  pserdvlem2  26788  eff1olem  26909  logdmnrp  27002  dvlog2lem  27013  logtayl  27021  cxpcn3lem  27108  atancl  27242  atanval  27245  chp1  27527  ppiublem2  27563  lgsdir2lem2  27686  lgsdir2lem3  27687  lgsquadlem2  27741  2lgslem1b  27752  rplogsumlem1  27844  rplogsumlem2  27845  pntlemj  27963  nnne0s  28756  1vgrex  29613  edglnl  29754  usgredg2v  29841  umgrres1lem  29924  upgrres1  29927  nbupgrres  29978  clwlkwlk  30395  wwlksnextproplem1  30531  wwlksnextproplem2  30532  wwlksnextproplem3  30533  rusgrnumwwlkb0  30596  clwlkclwwlklem2a4  30621  eleclclwwlknlem1  30684  eleclclwwlknlem2  30685  erclwwlkneqlen  30692  erclwwlknref  30693  erclwwlknsym  30694  erclwwlkntr  30695  hashecclwwlkn1  30701  umgrhashecclwwlk  30702  frgrnbnb  30927  frgrwopreglem4  30949  frgrwopreglem5  30955  frgrwopreg  30957  numclwlk1  31005  vciOLD  31196  axhcompl-zf  31633  mayete3i  32363  pj3lem1  32841  fzto1stfv1  33738  fzto1st  33740  fzto1stinvn  33741  psgnfzto1st  33742  rmfsupp2  33874  erler  33902  selvply1rhmlemb  34234  vieta  34295  submat1n  34520  xrge0mulc1cn  34656  fiunelros  34890  elmbfmvol2  34982  fibp1  35116  rrvsum  35169  ballotlemfmpn  35210  reprsuc  35327  bnj529  35455  bnj923  35482  bnj570  35618  bnj594  35625  bnj1173  35715  bnj1256  35728  bnj1259  35729  bnj1296  35734  bnj1498  35774  rankfo  35830  fineqvnttrclselem1  35902  subfacp1lem1  36124  kur14lem7  36157  sat1el2xp  36324  mvrsval  36450  mvrsfpw  36451  mrsubcv  36455  mrsubccat  36463  msubff  36475  msrid  36490  msubvrs  36505  mppsval  36517  divcnvlin  36689  iprodefisumlem  36696  iprodefisum  36697  faclimlem1  36699  onsucsuccmpi  37422  bj-opelresdm  38271  bj-inftyexpitaudisj  38331  bj-inftyexpidisj  38336  bj-ccinftydisj  38339  bj-elccinfty  38340  finixpnum  38733  poimirlem5  38748  poimirlem6  38749  poimirlem7  38750  poimirlem8  38751  poimirlem9  38752  poimirlem10  38753  poimirlem11  38754  poimirlem12  38755  poimirlem13  38756  poimirlem14  38757  poimirlem15  38758  poimirlem16  38759  poimirlem17  38760  poimirlem18  38761  poimirlem19  38762  poimirlem20  38763  poimirlem21  38764  poimirlem22  38765  poimirlem29  38772  poimirlem30  38773  broucube  38777  volsupnfl  38788  dvasin  38827  dvacos  38828  sdclem2  38879  fdc  38882  heiborlem4  38951  heiborlem6  38953  smgrpismgmOLD  38999  mndoissmgrpOLD  39005  mndoisexid  39006  rngoueqz  39077  drngoi  39088  dfadjliftmap2  39592  dfblockliftmap2  39596  sucpre  39632  eldisjsim2  40070  redvmptabs  43615  mhphflem  43828  prjspertr  43837  prjsperref  43838  prjspersym  43839  prjspreln0  43841  prjspvs  43842  prjsprellsp  43843  jm2.23  44207  wepwsolem  44253  omabs2  44537  omcl3g  44539  trclfvdecomr  44931  mnuprdlem1  45459  mnuprdlem2  45460  binomcxplemdvbinom  45540  binomcxplemnotnn0  45543  orbitcl  46153  hfstructstruct  46234  hfstructfun  46235  rnhfstructsshf  46236  ssfiunibd  46540  climinf  46833  stoweidlem15  47240  fourierdlem66  47397  etransclem37  47496  smfsupmpt  48040  smfinfmpt  48044  smflimsuplem8  48052  eldmressn  48322  afvres  48457  ndmaovrcl  48489  2ltceilhalf  48617  minusmodnep2tmod  48644  modmknepk  48653  mod2addne  48655  modm2nep1  48657  modm1nep2  48659  modm1nem2  48660  modm1p1ne  48661  sprsymrelfv  48791  fmtnofz04prm  48877  31prm  48897  ppivalnnnprm  48928  indprmfz  48930  stgr0  49273  stgr1  49274  gpgiedgdmellem  49359  gpgvtx1  49367  gpgedgvtx1  49375  gpgedg2iv  49380  gpg5nbgrvtx13starlem2  49385  pgnbgreunbgrlem3  49431  pgnbgreunbgrlem6  49437  2zrngamnd  49559  2zrngacmnd  49560  2zrngagrp  49561  2zrngALT  49566  2zrngnmlid  49567  2zrngnmlid2  49569  fldhmsubcALTV  49645  lincvalsng  49743  snlindsntor  49798  lincresunit3lem2  49807  lincresunit3  49808  ldepsnlinc  49835  nn0sumshdiglemA  49946  nn0sumshdiglemB  49947  rrx2pnecoorneor  50043  rrx2linest  50069  isorcl  50362  catcrcl  50745  setc2othin  50816