Theorem eleq2s 2551

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 2521	. 2 |- ( A e. C <-> A e. B )
3		eleq2s.1	. 2 |- ( A e. B -> ph )
4	2, 3	sylbi 195	1 |- ( A e. C -> ph )

Syntax hints:   -> wi 4   = wceq 1383   e. wcel 1804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-cleq 2435  df-clel 2438

This theorem is referenced by:  elrabi  3240  epelg  4782  elxpi  5005  optocl  5066  eldmeldmressn  5304  fveqdmss  6011  oprabv  6330  elmpt2cl  6502  bropopvvv  6865  ressuppss  6921  mpt2xopn0yelv  6943  mpt2xopxnop0  6945  tfr2a  7066  rdgseg  7090  2oconcl  7155  ecexr  7318  ectocld  7380  ecoptocl  7403  brecop2  7407  eroveu  7408  mapsnconst  7466  mapfienlem1  7866  mapfienlem2  7867  mapfienlem3  7868  cantnflem2  8112  r1sucg  8190  r1suc  8191  acnrcl  8426  dfac5lem4  8510  fin23lem29  8724  fin23lem30  8725  axcclem  8840  alephval2  8950  0tsk  9136  0nsr  9459  peano2nn  10554  uzssz  11109  peano2uzs  11144  uzsupss  11183  fzossnn0  11835  ltweuz  12051  fzennn  12057  ser1const  12142  expp1  12152  facnn  12334  facp1  12337  bcpasc  12378  hashfzo0  12467  ccatval2  12575  ccatass  12584  eqs1  12600  swrd00  12624  swrdid  12631  swrd0  12637  wrdeqcats1  12678  wrdeqs1cat  12679  splfv2a  12711  revccat  12719  rexuz3  13160  rexanuz2  13161  r19.2uz  13163  rexuzre  13164  cau4  13168  caubnd2  13169  climrlim2  13349  climshft2  13384  climaddc1  13436  climmulc2  13438  climsubc1  13439  climsubc2  13440  climlec2  13460  isercoll2  13470  climsup  13471  climcau  13472  caurcvg  13478  caurcvg2  13479  caucvg  13480  caucvgb  13481  iseraltlem1  13483  iseralt  13486  binomlem  13620  isumshft  13630  cvgrat  13671  3prm  14111  phicl2  14175  phibndlem  14177  dfphi2  14181  crt  14185  vdwap0  14371  prmlem1a  14469  xpscfv  14836  xpsfeq  14838  oppccofval  14988  homarcl2  15236  arwrcl  15245  pleval2i  15468  letsr  15731  gsumws1  15881  mulgpropd  16049  psgnunilem2  16394  psgnprfval  16420  gexid  16475  efgmnvl  16606  efgrcl  16607  efgsval  16623  efgs1  16627  efgs1b  16628  frgpuptinv  16663  frgpup3lem  16669  lt6abl  16771  eldprd  16909  eldprdOLD  16911  isunit  17180  isirred  17222  abvrcl  17344  islss  17455  lbsss  17597  lbssp  17599  lbsind  17600  mpfrcl  18061  psr1basf  18114  coe1tm  18188  ply1frcl  18229  cssi  18588  thlle  18601  islbs4  18740  mavmulsolcl  18926  marepvcl  18944  1marepvmarrepid  18950  mdet0pr  18967  m2detleiblem1  18999  cramerimplem1  19058  cramerlem1  19062  chpscmat  19216  chpscmatgsumbin  19218  chpscmatgsummon  19219  ptpjpre1  19945  fin1aufil  20306  lmflf  20379  tsmsfbas  20499  xpsxmetlem  20755  xpsmet  20758  metustsymOLD  20937  metustsym  20938  iscmet3lem3  21602  iscmet3lem1  21603  iscmet3lem2  21604  iscmet3  21605  rrxmvallem  21704  volsup  21839  opnmblALT  21885  itg1val  21963  tdeglem2  22332  ulmcaulem  22661  ulmcau  22662  ulmss  22664  pserdvlem2  22695  eff1olem  22807  logdmnrp  22894  dvlog2lem  22905  logtayl  22913  cxpcn3lem  22993  atancl  23084  atanval  23087  chp1  23313  ppiublem2  23350  lgsdir2lem2  23471  lgsdir2lem3  23472  lgsquadlem2  23502  rplogsumlem1  23541  rplogsumlem2  23542  pntlemj  23660  uhgrac  24177  usgraidx2v  24265  nbgraf1olem3  24315  nbgraf1olem5  24317  wwlkextproplem1  24613  wwlkextproplem2  24614  wwlkextproplem3  24615  clwwlknprop  24644  clwlkisclwwlklem2a4  24656  eleclclwwlknlem1  24689  eleclclwwlknlem2  24690  erclwwlkneqlen  24696  erclwwlknref  24697  erclwwlknsym  24698  erclwwlkntr  24699  clwlkf1clwwlk  24722  2wlkonot3v  24747  2spthonot3v  24748  frgrawopreglem4  24919  frgrawopreg  24921  gxnn0suc  25138  smgrpismgmOLD  25206  smgrpisass  25207  mndoissmgrpOLD  25213  mndoisexid  25214  drngoi  25281  rngoueqz  25304  vci  25313  axhcompl-zf  25787  mayete3i  26518  pj3lem1  26997  fzssnn  27467  xrge0mulc1cn  27796  elmbfmvol2  28111  fibp1  28213  rrvsum  28266  ballotlemfmpn  28306  subfacp1lem1  28496  kur14lem7  28529  mvrsval  28738  mvrsfpw  28739  mrsubcv  28743  mrsubccat  28751  msubff  28763  msrid  28778  msubvrs  28793  mppsval  28805  divcnvlin  28993  clim2div  28998  ntrivcvg  29006  ntrivcvgtail  29009  fprodntriv  29049  fprodefsum  29079  fprodeq0  29080  iprodefisumlem  29098  iprodefisum  29099  faclimlem1  29143  predel  29238  prednn0  29257  onsucsuccmpi  29883  finixpnum  30013  volsupnfl  30034  dvasin  30078  dvacos  30079  sdclem2  30210  fdc  30213  heiborlem4  30285  heiborlem6  30287  jm2.23  30913  wepwsolem  30962  ssfiunibd  31458  climinf  31520  stoweidlem15  31686  fourierdlem66  31844  eldmressn  32046  afvres  32095  ndmaovrcl  32127  usgresvm1  32281  usgresvm1ALT  32285  2zrngamnd  32457  2zrngacmnd  32458  2zrngagrp  32459  2zrngALT  32464  2zrngnmlid  32465  2zrngnmlid2  32467  fldhmsubc  32625  fldhmsubcOLD  32644  lincvalsng  32752  snlindsntor  32807  lincresunit3lem2  32816  lincresunit3  32817  ldepsnlinc  32844  bnj529  33531  bnj923  33559  bnj570  33696  bnj594  33703  bnj1173  33791  bnj1256  33804  bnj1259  33805  bnj1296  33810  bnj1498  33850  bj-inftyexpidisj  34353  bj-ccinftydisj  34356  bj-elccinfty  34357