Theorem eleq2s 2558

Description: Substitution of equal classes into a membership antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
eleq2s.1	|- ( A e. B -> ph )
eleq2s.2	|- C = B

Assertion

Ref	Expression
eleq2s	|- ( A e. C -> ph )

Proof of Theorem eleq2s

Step	Hyp	Ref	Expression
1		eleq2s.2	. . 3 |- C = B
2	1	eleq2i 2532	. 2 |- ( A e. C <-> A e. B )
3		eleq2s.1	. 2 |- ( A e. B -> ph )
4	2, 3	sylbi 200	1 |- ( A e. C -> ph )

Syntax hints:   -> wi 4   = wceq 1455   e. wcel 1898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-cleq 2455  df-clel 2458

This theorem is referenced by:  elrabi  3205  epelg  4768  elxpi  4872  optocl  4933  eldmeldmressn  5167  predel  5420  fveqdmss  6045  oprabv  6371  elmpt2cl  6543  bropopvvv  6906  bropfvvvv  6908  ressuppss  6966  mpt2xeldm  6989  mpt2xopn0yelv  6991  mpt2xopxnop0  6993  tfr2a  7144  rdgseg  7171  2oconcl  7236  ecexr  7399  ectocld  7461  ecoptocl  7484  brecop2  7488  eroveu  7489  mapsnconst  7548  mapfienlem1  7949  mapfienlem2  7950  mapfienlem3  7951  cantnflem2  8226  r1sucg  8271  r1suc  8272  acnrcl  8504  dfac5lem4  8588  fin23lem29  8802  fin23lem30  8803  axcclem  8918  alephval2  9028  0tsk  9211  0nsr  9534  peano2nn  10654  uzssz  11212  peano2uzs  11247  uzsupss  11290  fzssnn  11877  prednn0  11950  fzossnn0  11986  ltweuz  12213  fzennn  12219  ser1const  12307  expp1  12317  facnn  12499  facp1  12502  bcpasc  12544  hashfzo0  12641  ccatval2  12765  ccatass  12774  swrd00  12817  swrd0  12833  wrdeqs1cat  12874  splfv2a  12906  revccat  12914  rexuz3  13466  rexanuz2  13467  r19.2uz  13469  rexuzre  13470  cau4  13474  caubnd2  13475  climrlim2  13666  climshft2  13701  climaddc1  13753  climmulc2  13755  climsubc1  13756  climsubc2  13757  climlec2  13777  isercoll2  13787  climsup  13788  climcau  13789  caurcvg  13797  caurcvgOLD  13798  caurcvg2  13799  caucvg  13800  caucvgb  13801  iseraltlem1  13803  iseralt  13806  binomlem  13942  isumshft  13952  cvgrat  13994  clim2div  14000  ntrivcvg  14008  ntrivcvgtail  14011  fprodntriv  14051  fprodeq0  14084  fprodefsum  14204  3prm  14696  phicl2  14771  phibndlem  14773  dfphi2  14777  crt  14781  vdwap0  14981  prmlem1a  15133  xpscfv  15523  xpsfeq  15525  oppccofval  15676  homarcl2  15985  arwrcl  15994  pleval2i  16265  letsr  16528  gsumws1  16678  mulgpropd  16846  psgnunilem2  17191  psgnprfval  17217  gexid  17287  efgmnvl  17419  efgrcl  17420  efgsval  17436  efgs1  17440  efgs1b  17441  frgpuptinv  17476  frgpup3lem  17482  lt6abl  17584  eldprd  17691  isunit  17940  isirred  17982  abvrcl  18104  islss  18213  lbsss  18355  lbssp  18357  lbsind  18358  mpfrcl  18796  psr1basf  18849  coe1tm  18921  ply1frcl  18962  cssi  19302  thlle  19315  islbs4  19445  mavmulsolcl  19631  marepvcl  19649  1marepvmarrepid  19655  mdet0pr  19672  m2detleiblem1  19704  cramerimplem1  19763  cramerlem1  19767  chpscmat  19921  chpscmatgsumbin  19923  chpscmatgsummon  19924  ptpjpre1  20641  fin1aufil  21002  lmflf  21075  tsmsfbas  21197  xpsxmetlem  21449  xpsmet  21452  metustsym  21625  iscmet3lem3  22315  iscmet3lem1  22316  iscmet3lem2  22317  iscmet3  22318  rrxmvallem  22413  volsup  22565  opnmblALT  22617  itg1val  22697  tdeglem2  23066  ulmcaulem  23405  ulmcau  23406  ulmss  23408  pserdvlem2  23439  eff1olem  23553  logdmnrp  23642  dvlog2lem  23653  logtayl  23661  cxpcn3lem  23743  atancl  23863  atanval  23866  chp1  24150  ppiublem2  24187  lgsdir2lem2  24308  lgsdir2lem3  24309  lgsquadlem2  24339  rplogsumlem1  24378  rplogsumlem2  24379  pntlemj  24497  uhgrac  25088  usgraidx2v  25176  nbgraf1olem3  25227  nbgraf1olem5  25229  wwlkextproplem1  25525  wwlkextproplem2  25526  wwlkextproplem3  25527  clwwlknprop  25556  clwlkisclwwlklem2a4  25568  eleclclwwlknlem1  25601  eleclclwwlknlem2  25602  erclwwlkneqlen  25608  erclwwlknref  25609  erclwwlknsym  25610  erclwwlkntr  25611  clwlkf1clwwlk  25634  2wlkonot3v  25659  2spthonot3v  25660  frgrawopreglem4  25831  frgrawopreg  25833  gxnn0suc  26048  smgrpismgmOLD  26116  smgrpisass  26117  mndoissmgrpOLD  26123  mndoisexid  26124  drngoi  26191  rngoueqz  26214  vci  26223  axhcompl-zf  26707  mayete3i  27437  pj3lem1  27915  fzto1stfv1  28665  fzto1st  28667  fzto1stinvn  28668  psgnfzto1st  28669  submat1n  28682  xrge0mulc1cn  28798  fiunelros  29047  elmbfmvol2  29139  fibp1  29284  rrvsum  29337  ballotlemfmpn  29377  bnj529  29601  bnj923  29629  bnj570  29766  bnj594  29773  bnj1173  29861  bnj1256  29874  bnj1259  29875  bnj1296  29880  bnj1498  29920  subfacp1lem1  29952  kur14lem7  29985  mvrsval  30193  mvrsfpw  30194  mrsubcv  30198  mrsubccat  30206  msubff  30218  msrid  30233  msubvrs  30248  mppsval  30260  divcnvlin  30417  iprodefisumlem  30426  iprodefisum  30427  faclimlem1  30429  onsucsuccmpi  31153  bj-inftyexpidisj  31698  bj-ccinftydisj  31701  bj-elccinfty  31702  finixpnum  31976  poimirlem5  31991  poimirlem6  31992  poimirlem7  31993  poimirlem8  31994  poimirlem9  31995  poimirlem10  31996  poimirlem11  31997  poimirlem12  31998  poimirlem13  31999  poimirlem14  32000  poimirlem15  32001  poimirlem16  32002  poimirlem17  32003  poimirlem18  32004  poimirlem19  32005  poimirlem20  32006  poimirlem21  32007  poimirlem22  32008  poimirlem29  32015  poimirlem30  32016  broucube  32020  volsupnfl  32031  dvasin  32074  dvacos  32075  sdclem2  32117  fdc  32120  heiborlem4  32192  heiborlem6  32194  jm2.23  35897  wepwsolem  35946  trclfvdecomr  36366  binomcxplemdvbinom  36747  binomcxplemnotnn0  36750  ssfiunibd  37602  climinf  37770  climinfOLD  37771  stoweidlem15  37976  fourierdlem66  38137  etransclem37  38237  eldmressn  38759  afvres  38809  ndmaovrcl  38841  pfx00  39062  pfx0  39063  usgredg2v  39450  umgrres1lem  39523  upgrres1  39526  nbupgrres  39584  usgresvm1  40124  usgresvm1ALT  40128  2zrngamnd  40310  2zrngacmnd  40311  2zrngagrp  40312  2zrngALT  40317  2zrngnmlid  40318  2zrngnmlid2  40320  fldhmsubc  40455  fldhmsubcALTV  40474  lincvalsng  40578  snlindsntor  40633  lincresunit3lem2  40642  lincresunit3  40643  ldepsnlinc  40670  nn0sumshdiglemA  40799  nn0sumshdiglemB  40800