Theorem eleq2s 2496

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

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721

This theorem is referenced by:  elrabi  3050  epelg  4455  elxpi  4853  optocl  4911  elmpt2cl  6247  bropopvvv  6385  mpt2xopn0yelv  6423  mpt2xopxnop0  6425  tfr2a  6615  rdgseg  6639  2oconcl  6706  ecexr  6869  ectocld  6930  ecoptocl  6953  brecop2  6957  eroveu  6958  mapsnconst  7018  cantnflem2  7602  r1sucg  7651  r1suc  7652  acnrcl  7879  dfac5lem4  7963  fin23lem29  8177  fin23lem30  8178  axcclem  8293  alephval2  8403  0tsk  8586  0nsr  8910  peano2nn  9968  uzssz  10461  peano2uzs  10487  uzsupss  10524  ltweuz  11256  fzennn  11262  ser1const  11334  expp1  11343  facnn  11523  facp1  11526  bcn0  11556  bcpasc  11567  hashfzo0  11650  ccatval2  11701  ccatass  11705  eqs1  11716  swrd00  11720  swrdid  11727  splfv2a  11740  wrdeqcats1  11743  wrdeqs1cat  11744  revccat  11753  rexuz3  12107  rexanuz2  12108  r19.2uz  12110  rexuzre  12111  cau4  12115  caubnd2  12116  climrlim2  12296  climshft2  12331  climaddc1  12383  climmulc2  12385  climsubc1  12386  climsubc2  12387  climlec2  12407  isercoll2  12417  climsup  12418  climcau  12419  caurcvg  12425  caurcvg2  12426  caucvg  12427  caucvgb  12428  iseraltlem1  12430  iseralt  12433  binomlem  12563  isumshft  12574  cvgrat  12615  3prm  13051  phicl2  13112  phibndlem  13114  dfphi2  13118  crt  13122  vdwap0  13299  prmlem1a  13384  xpscfv  13742  xpsfeq  13744  oppccofval  13897  homarcl2  14145  arwrcl  14154  pleval2i  14376  letsr  14627  gsumws1  14740  mulgpropd  14878  gexid  15170  efgmnvl  15301  efgrcl  15302  efgsval  15318  efgs1  15322  efgs1b  15323  frgpuptinv  15358  frgpup3lem  15364  lt6abl  15459  eldprd  15517  isunit  15717  isirred  15759  abvrcl  15864  islss  15966  lbsss  16104  lbssp  16106  lbsind  16107  psr1basf  16554  coe1tm  16620  cssi  16866  thlle  16879  ptpjpre1  17556  fin1aufil  17917  lmflf  17990  tsmsfbas  18110  xpsxmetlem  18362  xpsmet  18365  metustsymOLD  18544  metustsym  18545  iscmet3lem3  19196  iscmet3lem1  19197  iscmet3lem2  19198  iscmet3  19199  volsup  19403  opnmblALT  19448  itg1val  19528  mpfrcl  19892  tdeglem2  19937  ulmcaulem  20263  ulmcau  20264  ulmss  20266  pserdvlem2  20297  eff1olem  20403  logdmnrp  20485  dvlog2lem  20496  logtayl  20504  cxpcn3lem  20584  atancl  20674  atanval  20677  chp1  20903  ppiublem2  20940  lgsdir2lem2  21061  lgsdir2lem3  21062  lgsquadlem2  21092  rplogsumlem1  21131  rplogsumlem2  21132  pntlemj  21250  usgraidx2v  21365  nbgraf1olem3  21406  nbgraf1olem5  21408  gxnn0suc  21805  smgrpismgm  21873  smgrpisass  21874  mndoissmgrp  21880  mndoisexid  21881  drngoi  21948  rngoueqz  21971  vci  21980  axhcompl-zf  22454  mayete3i  23183  pj3lem1  23662  fzssnn  24100  xrge0mulc1cn  24280  elmbfmvol2  24570  rrvsum  24665  ballotlemfmpn  24705  subfacp1lem1  24818  kur14lem7  24851  divcnvlin  25165  clim2div  25170  ntrivcvg  25178  ntrivcvgtail  25181  fprodntriv  25221  fprodefsum  25251  fprodeq0  25252  iprodefisumlem  25270  iprodefisum  25271  faclimlem1  25310  predel  25397  prednn0  25416  onsucsuccmpi  26097  volsupnfl  26150  sdclem2  26336  fdc  26339  heiborlem4  26413  heiborlem6  26415  jm2.23  26957  wepwsolem  27006  islbs4  27170  psgnunilem2  27286  climinf  27599  stoweidlem15  27631  eldmressn  27851  afvres  27903  ndmaovrcl  27935  2wlkonot3v  28072  2spthonot3v  28073  frgrawopreglem4  28150  frgrawopreg  28152  bnj529  28815  bnj923  28843  bnj570  28982  bnj594  28989  bnj1173  29077  bnj1256  29090  bnj1259  29091  bnj1296  29096  bnj1498  29136

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400