Theorem eleq2s 2329

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 2301	. 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 1398   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

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

This theorem is referenced by:  elrabi  2973  opelopabsb  4383  epelg  4416  reg3exmidlemwe  4706  elxpi  4770  optocl  4831  elfvm  5708  elfvfvex  5709  fvmbr  5710  fvmptss2  5757  fvmptssdm  5767  acexmidlemcase  6053  elmpocl  6257  ressuppss  6467  mpoxopn0yelv  6483  tfr2a  6565  tfri1dALT  6595  2oconcl  6685  el2oss1o  6689  ecexr  6785  ectocld  6848  ecoptocl  6869  eroveu  6873  mapsnconst  6942  diffitest  7157  en2eqpr  7180  ctssdccl  7415  nninfwlpoimlemginf  7480  exmidonfinlem  7509  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  acnrcl  7521  dmaddpqlem  7708  nqpi  7709  nq0nn  7773  0nsr  8080  suplocsrlempr  8138  cnm  8163  axaddcl  8195  axmulcl  8197  aprcl  8937  aptap  8941  peano2uzs  9934  fzssnn  10423  fzossnn0  10533  infssuzex  10615  infssuzledc  10616  rebtwn2zlemstep  10636  fldiv4p1lem1div2  10689  frecfzennn  10812  fser0const  10921  facnn  11114  bcpasc  11153  hashfzo0  11213  hashfibc  11232  ccatval2  11311  ccatass  11321  pfxclz  11396  wrdeqs1cat  11437  rexuz3  11700  rexanuz2  11701  r19.2uz  11703  cau4  11826  caubnd2  11827  climshft2  12016  climaddc1  12039  climmulc2  12041  climsubc1  12042  climsubc2  12043  climlec2  12051  climcau  12057  climcaucn  12061  iserabs  12186  binomlem  12194  isumshft  12201  cvgratgt0  12244  clim2divap  12251  ntrivcvgap  12259  fprodntrivap  12295  fprodeq0  12328  3prm  12850  phicl2  12936  phibndlem  12938  dfphi2  12942  crth  12946  phimullem  12947  ballotfilemfmpn  13178  znnen  13233  ennnfonelemkh  13247  fvprif  13607  xpsfeq  13609  ismgmn0  13621  zrhval  14891  lgsdir2lem2  16028  lgsdir2lem3  16029  lgsquadlem2  16077  2lgslem1b  16088  1vgrex  16141  usgredg2v  16345  konigsberglem5  16613  bj-el2oss1o  16672  2o01f  16894  nninfalllem1  16912  nninfall  16913