Theorem eleq2s 2575

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 2545	. 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 1379   e. wcel 1767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462

This theorem is referenced by:  elrabi  3258  epelg  4792  elxpi  5015  optocl  5074  eldmeldmressn  5312  oprabv  6327  elmpt2cl  6499  bropopvvv  6860  ressuppss  6916  mpt2xopn0yelv  6938  mpt2xopxnop0  6940  tfr2a  7061  rdgseg  7085  2oconcl  7150  ecexr  7313  ectocld  7375  ecoptocl  7398  brecop2  7402  eroveu  7403  mapsnconst  7461  mapfienlem1  7860  mapfienlem2  7861  mapfienlem3  7862  cantnflem2  8105  r1sucg  8183  r1suc  8184  acnrcl  8419  dfac5lem4  8503  fin23lem29  8717  fin23lem30  8718  axcclem  8833  alephval2  8943  0tsk  9129  0nsr  9452  peano2nn  10544  uzssz  11097  peano2uzs  11131  uzsupss  11170  fzossnn0  11820  ltweuz  12036  fzennn  12042  ser1const  12127  expp1  12137  facnn  12319  facp1  12322  bcn0  12352  bcpasc  12363  hashfzo0  12449  ccatval2  12557  ccatass  12566  eqs1  12580  swrd00  12604  swrdid  12611  swrd0  12617  wrdeqcats1  12658  wrdeqs1cat  12659  splfv2a  12691  revccat  12699  rexuz3  13140  rexanuz2  13141  r19.2uz  13143  rexuzre  13144  cau4  13148  caubnd2  13149  climrlim2  13329  climshft2  13364  climaddc1  13416  climmulc2  13418  climsubc1  13419  climsubc2  13420  climlec2  13440  isercoll2  13450  climsup  13451  climcau  13452  caurcvg  13458  caurcvg2  13459  caucvg  13460  caucvgb  13461  iseraltlem1  13463  iseralt  13466  binomlem  13600  isumshft  13610  cvgrat  13651  3prm  14089  phicl2  14153  phibndlem  14155  dfphi2  14159  crt  14163  vdwap0  14349  prmlem1a  14446  xpscfv  14813  xpsfeq  14815  oppccofval  14968  homarcl2  15216  arwrcl  15225  pleval2i  15447  letsr  15710  gsumws1  15830  mulgpropd  15975  psgnunilem2  16316  psgnprfval  16342  gexid  16397  efgmnvl  16528  efgrcl  16529  efgsval  16545  efgs1  16549  efgs1b  16550  frgpuptinv  16585  frgpup3lem  16591  lt6abl  16688  eldprd  16826  eldprdOLD  16828  isunit  17090  isirred  17132  abvrcl  17253  islss  17364  lbsss  17506  lbssp  17508  lbsind  17509  mpfrcl  17958  psr1basf  18011  coe1tm  18085  ply1frcl  18126  cssi  18482  thlle  18495  islbs4  18634  mavmulsolcl  18820  marepvcl  18838  1marepvmarrepid  18844  mdet0pr  18861  m2detleiblem1  18893  cramerimplem1  18952  cramerlem1  18956  chpscmat  19110  chpscmatgsumbin  19112  chpscmatgsummon  19113  ptpjpre1  19807  fin1aufil  20168  lmflf  20241  tsmsfbas  20361  xpsxmetlem  20617  xpsmet  20620  metustsymOLD  20799  metustsym  20800  iscmet3lem3  21464  iscmet3lem1  21465  iscmet3lem2  21466  iscmet3  21467  rrxmvallem  21566  volsup  21701  opnmblALT  21747  itg1val  21825  tdeglem2  22194  ulmcaulem  22523  ulmcau  22524  ulmss  22526  pserdvlem2  22557  eff1olem  22668  logdmnrp  22750  dvlog2lem  22761  logtayl  22769  cxpcn3lem  22849  atancl  22940  atanval  22943  chp1  23169  ppiublem2  23206  lgsdir2lem2  23327  lgsdir2lem3  23328  lgsquadlem2  23358  rplogsumlem1  23397  rplogsumlem2  23398  pntlemj  23516  uhgrac  23981  usgraidx2v  24069  nbgraf1olem3  24119  nbgraf1olem5  24121  wwlkextproplem1  24417  wwlkextproplem2  24418  wwlkextproplem3  24419  clwwlknprop  24448  clwlkisclwwlklem2a4  24460  eleclclwwlknlem1  24493  eleclclwwlknlem2  24494  erclwwlkneqlen  24500  erclwwlknref  24501  erclwwlknsym  24502  erclwwlkntr  24503  clwlkf1clwwlk  24526  2wlkonot3v  24551  2spthonot3v  24552  frgrawopreglem4  24724  frgrawopreg  24726  gxnn0suc  24942  smgrpismgm  25010  smgrpisass  25011  mndoissmgrp  25017  mndoisexid  25018  drngoi  25085  rngoueqz  25108  vci  25117  axhcompl-zf  25591  mayete3i  26322  pj3lem1  26801  fzssnn  27263  xrge0mulc1cn  27559  elmbfmvol2  27878  fibp1  27980  rrvsum  28033  ballotlemfmpn  28073  subfacp1lem1  28263  kur14lem7  28296  divcnvlin  28595  clim2div  28600  ntrivcvg  28608  ntrivcvgtail  28611  fprodntriv  28651  fprodefsum  28681  fprodeq0  28682  iprodefisumlem  28700  iprodefisum  28701  faclimlem1  28745  predel  28840  prednn0  28859  onsucsuccmpi  29485  finixpnum  29615  volsupnfl  29636  dvasin  29680  dvacos  29681  sdclem2  29838  fdc  29841  heiborlem4  29913  heiborlem6  29915  jm2.23  30542  wepwsolem  30591  climinf  31148  stoweidlem15  31315  eldmressn  31675  afvres  31724  ndmaovrcl  31756  usgresvm1  31912  usgresvm1ALT  31916  lincvalsng  32090  snlindsntor  32145  lincresunit3lem2  32154  lincresunit3  32155  ldepsnlinc  32190  bnj529  32877  bnj923  32905  bnj570  33042  bnj594  33049  bnj1173  33137  bnj1256  33150  bnj1259  33151  bnj1296  33156  bnj1498  33196  bj-inftyexpidisj  33685  bj-ccinftydisj  33688  bj-elccinfty  33689