Theorem eleq2s 2300

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 2272	. 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 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  elrabi  2926  opelopabsb  4306  epelg  4337  reg3exmidlemwe  4627  elxpi  4691  optocl  4751  elfvm  5609  fvmptss2  5654  fvmptssdm  5664  acexmidlemcase  5939  elmpocl  6141  mpoxopn0yelv  6325  tfr2a  6407  tfri1dALT  6437  2oconcl  6525  el2oss1o  6529  ecexr  6625  ectocld  6688  ecoptocl  6709  eroveu  6713  mapsnconst  6781  diffitest  6984  en2eqpr  7004  ctssdccl  7213  nninfwlpoimlemginf  7278  exmidonfinlem  7301  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  acnrcl  7313  dmaddpqlem  7490  nqpi  7491  nq0nn  7555  0nsr  7862  suplocsrlempr  7920  cnm  7945  axaddcl  7977  axmulcl  7979  aprcl  8719  aptap  8723  peano2uzs  9705  fzssnn  10190  fzossnn0  10299  infssuzex  10376  infssuzledc  10377  rebtwn2zlemstep  10395  fldiv4p1lem1div2  10448  frecfzennn  10571  fser0const  10680  facnn  10872  bcpasc  10911  hashfzo0  10968  ccatval2  11054  ccatass  11064  rexuz3  11301  rexanuz2  11302  r19.2uz  11304  cau4  11427  caubnd2  11428  climshft2  11617  climaddc1  11640  climmulc2  11642  climsubc1  11643  climsubc2  11644  climlec2  11652  climcau  11658  climcaucn  11662  iserabs  11786  binomlem  11794  isumshft  11801  cvgratgt0  11844  clim2divap  11851  ntrivcvgap  11859  fprodntrivap  11895  fprodeq0  11928  3prm  12450  phicl2  12536  phibndlem  12538  dfphi2  12542  crth  12546  phimullem  12547  znnen  12769  ennnfonelemkh  12783  fvprif  13175  xpsfeq  13177  ismgmn0  13190  zrhval  14379  lgsdir2lem2  15506  lgsdir2lem3  15507  lgsquadlem2  15555  2lgslem1b  15566  1vgrex  15617  bj-el2oss1o  15710  2o01f  15931  nninfalllem1  15945  nninfall  15946