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  6013  elmpocl  6217  mpoxopn0yelv  6405  tfr2a  6487  tfri1dALT  6517  2oconcl  6607  el2oss1o  6611  ecexr  6707  ectocld  6770  ecoptocl  6791  eroveu  6795  mapsnconst  6863  diffitest  7076  en2eqpr  7099  ctssdccl  7310  nninfwlpoimlemginf  7375  exmidonfinlem  7404  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acnrcl  7416  dmaddpqlem  7597  nqpi  7598  nq0nn  7662  0nsr  7969  suplocsrlempr  8027  cnm  8052  axaddcl  8084  axmulcl  8086  aprcl  8826  aptap  8830  peano2uzs  9818  fzssnn  10303  fzossnn0  10412  infssuzex  10494  infssuzledc  10495  rebtwn2zlemstep  10513  fldiv4p1lem1div2  10566  frecfzennn  10689  fser0const  10798  facnn  10990  bcpasc  11029  hashfzo0  11088  ccatval2  11179  ccatass  11189  pfxclz  11264  wrdeqs1cat  11305  rexuz3  11555  rexanuz2  11556  r19.2uz  11558  cau4  11681  caubnd2  11682  climshft2  11871  climaddc1  11894  climmulc2  11896  climsubc1  11897  climsubc2  11898  climlec2  11906  climcau  11912  climcaucn  11916  iserabs  12041  binomlem  12049  isumshft  12056  cvgratgt0  12099  clim2divap  12106  ntrivcvgap  12114  fprodntrivap  12150  fprodeq0  12183  3prm  12705  phicl2  12791  phibndlem  12793  dfphi2  12797  crth  12801  phimullem  12802  znnen  13024  ennnfonelemkh  13038  fvprif  13431  xpsfeq  13433  ismgmn0  13446  zrhval  14637  lgsdir2lem2  15764  lgsdir2lem3  15765  lgsquadlem2  15813  2lgslem1b  15824  1vgrex  15877  usgredg2v  16081  bj-el2oss1o  16396  2o01f  16619  nninfalllem1  16636  nninfall  16637