Theorem eleq2s 2535

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 2507	. 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 1369   e. wcel 1756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-clel 2439

This theorem is referenced by:  elrabi  3119  epelg  4638  elxpi  4861  optocl  4918  elmpt2cl  6309  bropopvvv  6658  ressuppss  6713  mpt2xopn0yelv  6735  mpt2xopxnop0  6737  tfr2a  6859  rdgseg  6883  2oconcl  6948  ecexr  7111  ectocld  7172  ecoptocl  7195  brecop2  7199  eroveu  7200  mapsnconst  7263  mapfienlem1  7659  mapfienlem2  7660  mapfienlem3  7661  cantnflem2  7903  r1sucg  7981  r1suc  7982  acnrcl  8217  dfac5lem4  8301  fin23lem29  8515  fin23lem30  8516  axcclem  8631  alephval2  8741  0tsk  8927  0nsr  9251  peano2nn  10339  uzssz  10885  peano2uzs  10914  uzsupss  10952  fzossnn0  11585  ltweuz  11789  fzennn  11795  ser1const  11867  expp1  11877  facnn  12058  facp1  12061  bcn0  12091  bcpasc  12102  hashfzo0  12196  ccatval2  12282  ccatass  12291  eqs1  12305  swrd00  12319  swrdid  12326  swrd0  12332  wrdeqcats1  12373  wrdeqs1cat  12374  splfv2a  12403  revccat  12411  rexuz3  12841  rexanuz2  12842  r19.2uz  12844  rexuzre  12845  cau4  12849  caubnd2  12850  climrlim2  13030  climshft2  13065  climaddc1  13117  climmulc2  13119  climsubc1  13120  climsubc2  13121  climlec2  13141  isercoll2  13151  climsup  13152  climcau  13153  caurcvg  13159  caurcvg2  13160  caucvg  13161  caucvgb  13162  iseraltlem1  13164  iseralt  13167  binomlem  13297  isumshft  13307  cvgrat  13348  3prm  13785  phicl2  13848  phibndlem  13850  dfphi2  13854  crt  13858  vdwap0  14042  prmlem1a  14139  xpscfv  14505  xpsfeq  14507  oppccofval  14660  homarcl2  14908  arwrcl  14917  pleval2i  15139  letsr  15402  gsumws1  15522  mulgpropd  15665  psgnunilem2  16006  psgnprfval  16030  gexid  16085  efgmnvl  16216  efgrcl  16217  efgsval  16233  efgs1  16237  efgs1b  16238  frgpuptinv  16273  frgpup3lem  16279  lt6abl  16376  eldprd  16491  eldprdOLD  16493  isunit  16754  isirred  16796  abvrcl  16911  islss  17021  lbsss  17163  lbssp  17165  lbsind  17166  mpfrcl  17609  psr1basf  17662  coe1tm  17731  ply1frcl  17758  cssi  18114  thlle  18127  islbs4  18266  mavmulsolcl  18367  marepvcl  18385  1marepvmarrepid  18391  mdet0pr  18408  m2detleiblem1  18435  cramerimplem1  18494  cramerlem1  18498  ptpjpre1  19149  fin1aufil  19510  lmflf  19583  tsmsfbas  19703  xpsxmetlem  19959  xpsmet  19962  metustsymOLD  20141  metustsym  20142  iscmet3lem3  20806  iscmet3lem1  20807  iscmet3lem2  20808  iscmet3  20809  rrxmvallem  20908  volsup  21042  opnmblALT  21088  itg1val  21166  tdeglem2  21535  ulmcaulem  21864  ulmcau  21865  ulmss  21867  pserdvlem2  21898  eff1olem  22009  logdmnrp  22091  dvlog2lem  22102  logtayl  22110  cxpcn3lem  22190  atancl  22281  atanval  22284  chp1  22510  ppiublem2  22547  lgsdir2lem2  22668  lgsdir2lem3  22669  lgsquadlem2  22699  rplogsumlem1  22738  rplogsumlem2  22739  pntlemj  22857  usgraidx2v  23316  nbgraf1olem3  23357  nbgraf1olem5  23359  gxnn0suc  23756  smgrpismgm  23824  smgrpisass  23825  mndoissmgrp  23831  mndoisexid  23832  drngoi  23899  rngoueqz  23922  vci  23931  axhcompl-zf  24405  mayete3i  25136  pj3lem1  25615  fzssnn  26079  xrge0mulc1cn  26376  elmbfmvol2  26687  fibp1  26789  rrvsum  26842  ballotlemfmpn  26882  subfacp1lem1  27072  kur14lem7  27105  divcnvlin  27404  clim2div  27409  ntrivcvg  27417  ntrivcvgtail  27420  fprodntriv  27460  fprodefsum  27490  fprodeq0  27491  iprodefisumlem  27509  iprodefisum  27510  faclimlem1  27554  predel  27649  prednn0  27668  onsucsuccmpi  28294  finixpnum  28419  volsupnfl  28441  dvasin  28485  dvacos  28486  sdclem2  28643  fdc  28646  heiborlem4  28718  heiborlem6  28720  jm2.23  29350  wepwsolem  29399  climinf  29784  stoweidlem15  29815  eldmressn  30032  afvres  30083  ndmaovrcl  30115  eldmeldmressn  30145  oprabv  30162  2wlkonot3v  30399  2spthonot3v  30400  clwwlknprop  30440  clwlkisclwwlklem2a4  30451  eleclclwwlknlem1  30495  eleclclwwlknlem2  30496  erclwwlkneqlen  30503  erclwwlknref  30504  erclwwlknsym  30505  erclwwlkntr  30506  clwlkf1clwwlk  30528  wwlkextproplem1  30565  wwlkextproplem2  30566  wwlkextproplem3  30567  frgrawopreglem4  30645  frgrawopreg  30647  dmatmul  30881  dmatsubcl  30882  dmatmulcl  30884  dmatcrng  30886  scmatsubcl  30889  scmatmulcl  30891  scmatcrng  30893  lincvalsng  30955  snlindsntor  31010  lincresunit3lem2  31019  lincresunit3  31020  ldepsnlinc  31055  bnj529  31738  bnj923  31766  bnj570  31903  bnj594  31910  bnj1173  31998  bnj1256  32011  bnj1259  32012  bnj1296  32017  bnj1498  32057  bj-inftyexpidisj  32538  bj-ccinftydisj  32541  bj-elccinfty  32542