Theorem eleq2s 2299

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 2271	. 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 1372   e. wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  elrabi  2925  opelopabsb  4305  epelg  4336  reg3exmidlemwe  4626  elxpi  4690  optocl  4750  elfvm  5608  fvmptss2  5653  fvmptssdm  5663  acexmidlemcase  5938  elmpocl  6140  mpoxopn0yelv  6324  tfr2a  6406  tfri1dALT  6436  2oconcl  6524  el2oss1o  6528  ecexr  6624  ectocld  6687  ecoptocl  6708  eroveu  6712  mapsnconst  6780  diffitest  6983  en2eqpr  7003  ctssdccl  7212  nninfwlpoimlemginf  7277  exmidonfinlem  7300  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  acnrcl  7312  dmaddpqlem  7489  nqpi  7490  nq0nn  7554  0nsr  7861  suplocsrlempr  7919  cnm  7944  axaddcl  7976  axmulcl  7978  aprcl  8718  aptap  8722  peano2uzs  9704  fzssnn  10189  fzossnn0  10297  infssuzex  10374  infssuzledc  10375  rebtwn2zlemstep  10393  fldiv4p1lem1div2  10446  frecfzennn  10569  fser0const  10678  facnn  10870  bcpasc  10909  hashfzo0  10966  ccatval2  11052  ccatass  11062  rexuz3  11243  rexanuz2  11244  r19.2uz  11246  cau4  11369  caubnd2  11370  climshft2  11559  climaddc1  11582  climmulc2  11584  climsubc1  11585  climsubc2  11586  climlec2  11594  climcau  11600  climcaucn  11604  iserabs  11728  binomlem  11736  isumshft  11743  cvgratgt0  11786  clim2divap  11793  ntrivcvgap  11801  fprodntrivap  11837  fprodeq0  11870  3prm  12392  phicl2  12478  phibndlem  12480  dfphi2  12484  crth  12488  phimullem  12489  znnen  12711  ennnfonelemkh  12725  fvprif  13117  xpsfeq  13119  ismgmn0  13132  zrhval  14321  lgsdir2lem2  15448  lgsdir2lem3  15449  lgsquadlem2  15497  2lgslem1b  15508  1vgrex  15559  bj-el2oss1o  15643  2o01f  15864  nninfalllem1  15878  nninfall  15879