Theorem eleq2s 2858

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  elrabi  3619  elrabiOLD  3620  optocl  5682  ssrel  5694  eldmeldmressn  5938  predel  6227  fveqdmss  6965  oprabv  7344  elmpocl  7520  el2mpocsbcl  7934  bropopvvv  7939  bropfvvvv  7941  ressuppss  8008  mpoxeldm  8036  mpoxopn0yelv  8038  mpoxopxnop0  8040  tfr2a  8235  rdgseg  8262  2oconcl  8342  ecexr  8512  ectocld  8582  ecoptocl  8605  brecop2  8609  eroveu  8610  mapfvd  8676  mapsnconst  8689  mapfienlem1  9173  mapfienlem2  9174  mapfienlem3  9175  cantnflem2  9457  r1sucg  9536  r1suc  9537  acnrcl  9807  dfac5lem4  9891  fin23lem29  10106  fin23lem30  10107  axcclem  10222  alephval2  10337  0tsk  10520  0nsr  10844  peano2nn  11994  uzssz  12612  peano2uzs  12651  uzsupss  12689  fzssnn  13309  prednn0  13389  fzossnn0  13427  fldiv4p1lem1div2  13564  ltweuz  13690  fzennn  13697  ser1const  13788  expp1  13798  facnn  13998  facp1  14001  bcpasc  14044  hashfzo0  14154  ccatval2  14292  ccatass  14302  swrd00  14366  swrd0  14380  pfx00  14396  pfx0  14397  wrdeqs1cat  14442  splfv2a  14478  revccat  14488  rexuz3  15069  rexanuz2  15070  r19.2uz  15072  rexuzre  15073  cau4  15077  caubnd2  15078  climrlim2  15265  climshft2  15300  climaddc1  15353  climmulc2  15355  climsubc1  15356  climsubc2  15357  climlec2  15379  isercoll2  15389  climsup  15390  climcau  15391  caurcvg  15397  caurcvg2  15398  caucvg  15399  caucvgb  15400  iseraltlem1  15402  iseralt  15405  binomlem  15550  isumshft  15560  cvgrat  15604  clim2div  15610  ntrivcvg  15618  ntrivcvgtail  15621  fprodntriv  15661  fprodeq0  15694  fprodefsum  15813  pwp1fsum  16109  3prm  16408  phicl2  16478  phibndlem  16480  dfphi2  16484  crth  16488  vdwap0  16686  prmlem1a  16817  fvprif  17281  xpsfeq  17283  oppccofval  17435  homarcl2  17759  arwrcl  17768  pleval2i  18063  letsr  18320  gsumws1  18485  smndex1mndlem  18557  mulgnngsum  18718  mulgpropd  18754  psgnunilem2  19112  psgnprfval  19138  gexid  19195  efgmnvl  19329  efgrcl  19330  efgsval  19346  efgs1  19350  efgs1b  19351  frgpuptinv  19386  frgpup3lem  19392  lt6abl  19505  eldprd  19616  isunit  19908  isirred  19950  abvrcl  20090  islss  20205  lbsss  20348  lbssp  20350  lbsind  20351  cssi  20898  thlle  20912  thlleOLD  20913  islbs4  21048  mpfrcl  21304  psr1basf  21381  coe1tm  21453  ply1frcl  21493  mavmulsolcl  21709  marepvcl  21727  1marepvmarrepid  21733  mdet0pr  21750  m2detleiblem1  21782  cramerimplem1  21841  cramerlem1  21845  chpscmat  22000  chpscmatgsumbin  22002  chpscmatgsummon  22003  ptpjpre1  22731  fin1aufil  23092  lmflf  23165  tsmsfbas  23288  xpsxmetlem  23541  xpsmet  23544  metustsym  23720  iscmet3lem3  24463  iscmet3lem1  24464  iscmet3lem2  24465  iscmet3  24466  rrxmvallem  24577  volsup  24729  opnmblALT  24776  itg1val  24856  tdeglem2  25235  ulmcaulem  25562  ulmcau  25563  ulmss  25565  pserdvlem2  25596  eff1olem  25713  logdmnrp  25805  dvlog2lem  25816  logtayl  25824  cxpcn3lem  25909  atancl  26040  atanval  26043  chp1  26325  ppiublem2  26360  lgsdir2lem2  26483  lgsdir2lem3  26484  lgsquadlem2  26538  2lgslem1b  26549  rplogsumlem1  26641  rplogsumlem2  26642  pntlemj  26760  1vgrex  27381  edglnl  27522  usgredg2v  27603  umgrres1lem  27686  upgrres1  27689  nbupgrres  27740  clwlkwlk  28152  wwlksnextproplem1  28283  wwlksnextproplem2  28284  wwlksnextproplem3  28285  rusgrnumwwlkb0  28345  clwlkclwwlklem2a4  28370  eleclclwwlknlem1  28433  eleclclwwlknlem2  28434  erclwwlkneqlen  28441  erclwwlknref  28442  erclwwlknsym  28443  erclwwlkntr  28444  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  frgrnbnb  28666  frgrwopreglem4  28688  frgrwopreglem5  28694  frgrwopreg  28696  numclwlk1  28744  vciOLD  28932  axhcompl-zf  29369  mayete3i  30099  pj3lem1  30577  fzto1stfv1  31377  fzto1st  31379  fzto1stinvn  31380  psgnfzto1st  31381  rmfsupp2  31501  submat1n  31764  xrge0mulc1cn  31900  fiunelros  32151  elmbfmvol2  32243  fibp1  32377  rrvsum  32430  ballotlemfmpn  32470  reprsuc  32604  bnj529  32730  bnj923  32757  bnj570  32894  bnj594  32901  bnj1173  32991  bnj1256  33004  bnj1259  33005  bnj1296  33010  bnj1498  33050  subfacp1lem1  33150  kur14lem7  33183  sat1el2xp  33350  mvrsval  33476  mvrsfpw  33477  mrsubcv  33481  mrsubccat  33489  msubff  33501  msrid  33516  msubvrs  33531  mppsval  33543  divcnvlin  33707  iprodefisumlem  33715  iprodefisum  33716  faclimlem1  33718  onsucsuccmpi  34641  bj-opelresdm  35325  bj-inftyexpitaudisj  35385  bj-inftyexpidisj  35390  bj-ccinftydisj  35393  bj-elccinfty  35394  finixpnum  35771  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem9  35795  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem13  35799  poimirlem14  35800  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem29  35815  poimirlem30  35816  broucube  35820  volsupnfl  35831  dvasin  35870  dvacos  35871  sdclem2  35909  fdc  35912  heiborlem4  35981  heiborlem6  35983  smgrpismgmOLD  36029  mndoissmgrpOLD  36035  mndoisexid  36036  rngoueqz  36107  drngoi  36118  mhphflem  40291  prjspertr  40451  prjsperref  40452  prjspersym  40453  prjspreln0  40455  prjspvs  40456  prjsprellsp  40457  jm2.23  40825  wepwsolem  40874  trclfvdecomr  41343  mnuprdlem1  41897  mnuprdlem2  41898  binomcxplemdvbinom  41978  binomcxplemnotnn0  41981  ssfiunibd  42855  climinf  43154  stoweidlem15  43563  fourierdlem66  43720  etransclem37  43819  smfsupmpt  44359  smflimsuplem8  44371  eldmressn  44542  afvres  44675  ndmaovrcl  44707  sprsymrelfv  44957  fmtnofz04prm  45040  31prm  45060  2zrngamnd  45510  2zrngacmnd  45511  2zrngagrp  45512  2zrngALT  45517  2zrngnmlid  45518  2zrngnmlid2  45520  fldhmsubc  45653  fldhmsubcALTV  45671  lincvalsng  45768  snlindsntor  45823  lincresunit3lem2  45832  lincresunit3  45833  ldepsnlinc  45860  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  rrx2pnecoorneor  46072  rrx2linest  46099  rrx2linesl  46100  setc2othin  46348