Theorem eleq2s 2901

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

Syntax hints:   → wi 4   = wceq 1637   ∈ wcel 2156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2782

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2797  df-clel 2800

This theorem is referenced by:  elrabi  3552  epelg  5223  elxpi  5330  optocl  5395  eldmeldmressn  5643  predel  5908  fveqdmss  6574  oprabv  6931  elmpt2cl  7104  el2mpt2csbcl  7481  bropopvvv  7487  bropfvvvv  7489  ressuppss  7546  mpt2xeldm  7570  mpt2xopn0yelv  7572  mpt2xopxnop0  7574  tfr2a  7725  rdgseg  7752  2oconcl  7818  ecexr  7982  ectocld  8047  ecoptocl  8070  brecop2  8074  brecop2OLD  8075  eroveu  8076  mapsnconst  8138  mapfienlem1  8547  mapfienlem2  8548  mapfienlem3  8549  cantnflem2  8832  r1sucg  8877  r1suc  8878  acnrcl  9146  dfac5lem4  9230  fin23lem29  9446  fin23lem30  9447  axcclem  9562  alephval2  9677  0tsk  9860  0nsr  10183  peano2nn  11315  uzssz  11922  peano2uzs  11958  uzsupss  11997  fzssnn  12606  prednn0  12685  fzossnn0  12721  fldiv4p1lem1div2  12858  ltweuz  12982  fzennn  12989  ser1const  13078  expp1  13088  facnn  13280  facp1  13283  bcpasc  13326  hashfzo0  13432  ccatval2  13573  ccatass  13583  swrd00  13639  swrd0  13656  wrdeqs1cat  13696  splfv2a  13729  revccat  13737  rexuz3  14309  rexanuz2  14310  r19.2uz  14312  rexuzre  14313  cau4  14317  caubnd2  14318  climrlim2  14499  climshft2  14534  climaddc1  14586  climmulc2  14588  climsubc1  14589  climsubc2  14590  climlec2  14610  isercoll2  14620  climsup  14621  climcau  14622  caurcvg  14628  caurcvg2  14629  caucvg  14630  caucvgb  14631  iseraltlem1  14633  iseralt  14636  binomlem  14781  isumshft  14791  cvgrat  14834  clim2div  14840  ntrivcvg  14848  ntrivcvgtail  14851  fprodntriv  14891  fprodeq0  14924  fprodefsum  15043  pwp1fsum  15332  3prm  15622  phicl2  15688  phibndlem  15690  dfphi2  15694  crth  15698  vdwap0  15895  prmlem1a  16023  xpscfv  16425  xpsfeq  16427  oppccofval  16578  homarcl2  16887  arwrcl  16896  pleval2i  17167  letsr  17430  gsumws1  17579  mulgpropd  17784  psgnunilem2  18114  psgnprfval  18140  gexid  18195  efgmnvl  18326  efgrcl  18327  efgsval  18343  efgs1  18347  efgs1b  18348  frgpuptinv  18383  frgpup3lem  18389  lt6abl  18495  eldprd  18603  isunit  18857  isirred  18899  abvrcl  19023  islss  19137  lbsss  19282  lbssp  19284  lbsind  19285  mpfrcl  19724  psr1basf  19777  coe1tm  19849  ply1frcl  19889  cssi  20236  thlle  20249  islbs4  20379  mavmulsolcl  20566  marepvcl  20584  1marepvmarrepid  20590  mdet0pr  20607  m2detleiblem1  20639  cramerimplem1  20699  cramerimplem1OLD  20700  cramerlem1  20704  chpscmat  20858  chpscmatgsumbin  20860  chpscmatgsummon  20861  ptpjpre1  21586  fin1aufil  21947  lmflf  22020  tsmsfbas  22142  xpsxmetlem  22395  xpsmet  22398  metustsym  22571  iscmet3lem3  23298  iscmet3lem1  23299  iscmet3lem2  23300  iscmet3  23301  rrxmvallem  23397  volsup  23535  opnmblALT  23582  itg1val  23662  tdeglem2  24033  ulmcaulem  24360  ulmcau  24361  ulmss  24363  pserdvlem2  24394  eff1olem  24507  logdmnrp  24599  dvlog2lem  24610  logtayl  24618  cxpcn3lem  24700  atancl  24820  atanval  24823  chp1  25105  ppiublem2  25140  lgsdir2lem2  25263  lgsdir2lem3  25264  lgsquadlem2  25318  2lgslem1b  25329  rplogsumlem1  25385  rplogsumlem2  25386  pntlemj  25504  1vgrex  26094  edglnl  26251  usgredg2v  26332  umgrres1lem  26416  upgrres1  26419  nbupgrres  26479  clwlkwlk  26897  wwlksnextproplem1  27045  wwlksnextproplem2  27046  wwlksnextproplem3  27047  rusgrnumwwlkb0  27111  clwlkclwwlklem2a4  27138  eleclclwwlknlem1  27209  eleclclwwlknlem2  27210  erclwwlkneqlen  27217  erclwwlknref  27218  erclwwlknsym  27219  erclwwlkntr  27220  hashecclwwlkn1  27226  umgrhashecclwwlk  27227  clwlksf1clwwlkOLD  27241  frgrnbnb  27466  frgrwopreglem4  27488  frgrwopreglem5  27494  frgrwopreg  27496  numclwlk1  27549  vciOLD  27742  axhcompl-zf  28181  mayete3i  28913  pj3lem1  29391  fzto1stfv1  30174  fzto1st  30176  fzto1stinvn  30177  psgnfzto1st  30178  submat1n  30194  xrge0mulc1cn  30310  fiunelros  30560  elmbfmvol2  30652  fibp1  30786  rrvsum  30839  ballotlemfmpn  30879  reprsuc  31016  bnj529  31132  bnj923  31159  bnj570  31296  bnj594  31303  bnj1173  31391  bnj1256  31404  bnj1259  31405  bnj1296  31410  bnj1498  31450  subfacp1lem1  31482  kur14lem7  31515  mvrsval  31723  mvrsfpw  31724  mrsubcv  31728  mrsubccat  31736  msubff  31748  msrid  31763  msubvrs  31778  mppsval  31790  divcnvlin  31938  iprodefisumlem  31946  iprodefisum  31947  faclimlem1  31949  onsucsuccmpi  32757  bj-inftyexpidisj  33412  bj-ccinftydisj  33415  bj-elccinfty  33416  finixpnum  33705  poimirlem5  33725  poimirlem6  33726  poimirlem7  33727  poimirlem8  33728  poimirlem9  33729  poimirlem10  33730  poimirlem11  33731  poimirlem12  33732  poimirlem13  33733  poimirlem14  33734  poimirlem15  33735  poimirlem16  33736  poimirlem17  33737  poimirlem18  33738  poimirlem19  33739  poimirlem20  33740  poimirlem21  33741  poimirlem22  33742  poimirlem29  33749  poimirlem30  33750  broucube  33754  volsupnfl  33765  dvasin  33806  dvacos  33807  sdclem2  33847  fdc  33850  heiborlem4  33922  heiborlem6  33924  smgrpismgmOLD  33970  mndoissmgrpOLD  33976  mndoisexid  33977  rngoueqz  34048  drngoi  34059  jm2.23  38062  wepwsolem  38111  trclfvdecomr  38518  binomcxplemdvbinom  39050  binomcxplemnotnn0  39053  ssfiunibd  40002  climinf  40316  stoweidlem15  40709  fourierdlem66  40866  etransclem37  40965  smflimsuplem8  41513  eldmressn  41654  afvres  41759  ndmaovrcl  41791  pfx00  41957  pfx0  41958  fmtnofz04prm  42062  31prm  42085  sprsymrelfv  42310  2zrngamnd  42507  2zrngacmnd  42508  2zrngagrp  42509  2zrngALT  42514  2zrngnmlid  42515  2zrngnmlid2  42517  fldhmsubc  42650  fldhmsubcALTV  42668  lincvalsng  42771  snlindsntor  42826  lincresunit3lem2  42835  lincresunit3  42836  ldepsnlinc  42863  nn0sumshdiglemA  42979  nn0sumshdiglemB  42980