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

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

This theorem is referenced by:  elrabi  2960  opelopabsb  4360  epelg  4393  reg3exmidlemwe  4683  elxpi  4747  optocl  4808  elfvm  5681  elfvfvex  5682  fvmbr  5683  fvmptss2  5730  fvmptssdm  5740  acexmidlemcase  6023  elmpocl  6227  ressuppss  6432  mpoxopn0yelv  6448  tfr2a  6530  tfri1dALT  6560  2oconcl  6650  el2oss1o  6654  ecexr  6750  ectocld  6813  ecoptocl  6834  eroveu  6838  mapsnconst  6906  diffitest  7119  en2eqpr  7142  ctssdccl  7353  nninfwlpoimlemginf  7418  exmidonfinlem  7447  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  acnrcl  7459  dmaddpqlem  7640  nqpi  7641  nq0nn  7705  0nsr  8012  suplocsrlempr  8070  cnm  8095  axaddcl  8127  axmulcl  8129  aprcl  8868  aptap  8872  peano2uzs  9862  fzssnn  10348  fzossnn0  10457  infssuzex  10539  infssuzledc  10540  rebtwn2zlemstep  10558  fldiv4p1lem1div2  10611  frecfzennn  10734  fser0const  10843  facnn  11035  bcpasc  11074  hashfzo0  11133  ccatval2  11224  ccatass  11234  pfxclz  11309  wrdeqs1cat  11350  rexuz3  11613  rexanuz2  11614  r19.2uz  11616  cau4  11739  caubnd2  11740  climshft2  11929  climaddc1  11952  climmulc2  11954  climsubc1  11955  climsubc2  11956  climlec2  11964  climcau  11970  climcaucn  11974  iserabs  12099  binomlem  12107  isumshft  12114  cvgratgt0  12157  clim2divap  12164  ntrivcvgap  12172  fprodntrivap  12208  fprodeq0  12241  3prm  12763  phicl2  12849  phibndlem  12851  dfphi2  12855  crth  12859  phimullem  12860  znnen  13082  ennnfonelemkh  13096  fvprif  13489  xpsfeq  13491  ismgmn0  13504  zrhval  14696  lgsdir2lem2  15831  lgsdir2lem3  15832  lgsquadlem2  15880  2lgslem1b  15891  1vgrex  15944  usgredg2v  16148  konigsberglem5  16416  bj-el2oss1o  16475  2o01f  16697  nninfalllem1  16717  nninfall  16718