Theorem eleq2s 2326

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 2298	. 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 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  elrabi  2959  opelopabsb  4354  epelg  4387  reg3exmidlemwe  4677  elxpi  4741  optocl  4802  elfvm  5672  elfvfvex  5673  fvmbr  5674  fvmptss2  5721  fvmptssdm  5731  acexmidlemcase  6012  elmpocl  6216  mpoxopn0yelv  6404  tfr2a  6486  tfri1dALT  6516  2oconcl  6606  el2oss1o  6610  ecexr  6706  ectocld  6769  ecoptocl  6790  eroveu  6794  mapsnconst  6862  diffitest  7075  en2eqpr  7098  ctssdccl  7309  nninfwlpoimlemginf  7374  exmidonfinlem  7403  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  acnrcl  7415  dmaddpqlem  7596  nqpi  7597  nq0nn  7661  0nsr  7968  suplocsrlempr  8026  cnm  8051  axaddcl  8083  axmulcl  8085  aprcl  8825  aptap  8829  peano2uzs  9817  fzssnn  10302  fzossnn0  10411  infssuzex  10492  infssuzledc  10493  rebtwn2zlemstep  10511  fldiv4p1lem1div2  10564  frecfzennn  10687  fser0const  10796  facnn  10988  bcpasc  11027  hashfzo0  11086  ccatval2  11174  ccatass  11184  pfxclz  11259  wrdeqs1cat  11300  rexuz3  11550  rexanuz2  11551  r19.2uz  11553  cau4  11676  caubnd2  11677  climshft2  11866  climaddc1  11889  climmulc2  11891  climsubc1  11892  climsubc2  11893  climlec2  11901  climcau  11907  climcaucn  11911  iserabs  12035  binomlem  12043  isumshft  12050  cvgratgt0  12093  clim2divap  12100  ntrivcvgap  12108  fprodntrivap  12144  fprodeq0  12177  3prm  12699  phicl2  12785  phibndlem  12787  dfphi2  12791  crth  12795  phimullem  12796  znnen  13018  ennnfonelemkh  13032  fvprif  13425  xpsfeq  13427  ismgmn0  13440  zrhval  14630  lgsdir2lem2  15757  lgsdir2lem3  15758  lgsquadlem2  15806  2lgslem1b  15817  1vgrex  15870  usgredg2v  16074  bj-el2oss1o  16370  2o01f  16593  nninfalllem1  16610  nninfall  16611