Theorem eleq2s 2301

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  elrabi  2930  opelopabsb  4319  epelg  4350  reg3exmidlemwe  4640  elxpi  4704  optocl  4764  elfvm  5627  fvmptss2  5672  fvmptssdm  5682  acexmidlemcase  5957  elmpocl  6159  mpoxopn0yelv  6343  tfr2a  6425  tfri1dALT  6455  2oconcl  6543  el2oss1o  6547  ecexr  6643  ectocld  6706  ecoptocl  6727  eroveu  6731  mapsnconst  6799  diffitest  7005  en2eqpr  7025  ctssdccl  7234  nninfwlpoimlemginf  7299  exmidonfinlem  7327  exmidfodomrlemr  7336  exmidfodomrlemrALT  7337  acnrcl  7339  dmaddpqlem  7520  nqpi  7521  nq0nn  7585  0nsr  7892  suplocsrlempr  7950  cnm  7975  axaddcl  8007  axmulcl  8009  aprcl  8749  aptap  8753  peano2uzs  9735  fzssnn  10220  fzossnn0  10329  infssuzex  10408  infssuzledc  10409  rebtwn2zlemstep  10427  fldiv4p1lem1div2  10480  frecfzennn  10603  fser0const  10712  facnn  10904  bcpasc  10943  hashfzo0  11000  ccatval2  11087  ccatass  11097  pfxclz  11165  wrdeqs1cat  11206  rexuz3  11386  rexanuz2  11387  r19.2uz  11389  cau4  11512  caubnd2  11513  climshft2  11702  climaddc1  11725  climmulc2  11727  climsubc1  11728  climsubc2  11729  climlec2  11737  climcau  11743  climcaucn  11747  iserabs  11871  binomlem  11879  isumshft  11886  cvgratgt0  11929  clim2divap  11936  ntrivcvgap  11944  fprodntrivap  11980  fprodeq0  12013  3prm  12535  phicl2  12621  phibndlem  12623  dfphi2  12627  crth  12631  phimullem  12632  znnen  12854  ennnfonelemkh  12868  fvprif  13260  xpsfeq  13262  ismgmn0  13275  zrhval  14464  lgsdir2lem2  15591  lgsdir2lem3  15592  lgsquadlem2  15640  2lgslem1b  15651  1vgrex  15704  bj-el2oss1o  15880  2o01f  16101  nninfalllem1  16117  nninfall  16118