Theorem eleq2s 2327

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 2299	. 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 2203

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  elrabi  2970  opelopabsb  4378  epelg  4411  reg3exmidlemwe  4701  elxpi  4765  optocl  4826  elfvm  5703  elfvfvex  5704  fvmbr  5705  fvmptss2  5752  fvmptssdm  5762  acexmidlemcase  6045  elmpocl  6249  ressuppss  6454  mpoxopn0yelv  6470  tfr2a  6552  tfri1dALT  6582  2oconcl  6672  el2oss1o  6676  ecexr  6772  ectocld  6835  ecoptocl  6856  eroveu  6860  mapsnconst  6929  diffitest  7144  en2eqpr  7167  ctssdccl  7402  nninfwlpoimlemginf  7467  exmidonfinlem  7496  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  acnrcl  7508  dmaddpqlem  7692  nqpi  7693  nq0nn  7757  0nsr  8064  suplocsrlempr  8122  cnm  8147  axaddcl  8179  axmulcl  8181  aprcl  8920  aptap  8924  peano2uzs  9916  fzssnn  10402  fzossnn0  10511  infssuzex  10593  infssuzledc  10594  rebtwn2zlemstep  10612  fldiv4p1lem1div2  10665  frecfzennn  10788  fser0const  10897  facnn  11089  bcpasc  11128  hashfzo0  11188  hashfibc  11207  ccatval2  11286  ccatass  11296  pfxclz  11371  wrdeqs1cat  11412  rexuz3  11675  rexanuz2  11676  r19.2uz  11678  cau4  11801  caubnd2  11802  climshft2  11991  climaddc1  12014  climmulc2  12016  climsubc1  12017  climsubc2  12018  climlec2  12026  climcau  12032  climcaucn  12036  iserabs  12161  binomlem  12169  isumshft  12176  cvgratgt0  12219  clim2divap  12226  ntrivcvgap  12234  fprodntrivap  12270  fprodeq0  12303  3prm  12825  phicl2  12911  phibndlem  12913  dfphi2  12917  crth  12921  phimullem  12922  znnen  13149  ennnfonelemkh  13163  fvprif  13556  xpsfeq  13558  ismgmn0  13571  zrhval  14765  lgsdir2lem2  15902  lgsdir2lem3  15903  lgsquadlem2  15951  2lgslem1b  15962  1vgrex  16015  usgredg2v  16219  konigsberglem5  16487  bj-el2oss1o  16546  2o01f  16768  nninfalllem1  16786  nninfall  16787