Theorem eleq2s 2261

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 2233	. 2 |- ( A e. C <-> A e. B )
3		eleq2s.1	. 2 |- ( A e. B -> ph )
4	2, 3	sylbi 120	1 |- ( A e. C -> ph )

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  elrabi  2879  opelopabsb  4238  epelg  4268  reg3exmidlemwe  4556  elxpi  4620  optocl  4680  fvmptss2  5561  fvmptssdm  5570  acexmidlemcase  5837  elmpocl  6036  mpoxopn0yelv  6207  tfr2a  6289  tfri1dALT  6319  2oconcl  6407  el2oss1o  6411  ecexr  6506  ectocld  6567  ecoptocl  6588  eroveu  6592  mapsnconst  6660  diffitest  6853  en2eqpr  6873  ctssdccl  7076  exmidonfinlem  7149  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  dmaddpqlem  7318  nqpi  7319  nq0nn  7383  0nsr  7690  suplocsrlempr  7748  cnm  7773  axaddcl  7805  axmulcl  7807  aprcl  8544  peano2uzs  9522  fzssnn  10003  fzossnn0  10110  rebtwn2zlemstep  10188  fldiv4p1lem1div2  10240  frecfzennn  10361  fser0const  10451  facnn  10640  bcpasc  10679  hashfzo0  10736  rexuz3  10932  rexanuz2  10933  r19.2uz  10935  cau4  11058  caubnd2  11059  climshft2  11247  climaddc1  11270  climmulc2  11272  climsubc1  11273  climsubc2  11274  climlec2  11282  climcau  11288  climcaucn  11292  iserabs  11416  binomlem  11424  isumshft  11431  cvgratgt0  11474  clim2divap  11481  ntrivcvgap  11489  fprodntrivap  11525  fprodeq0  11558  infssuzex  11882  infssuzledc  11883  3prm  12060  phicl2  12146  phibndlem  12148  dfphi2  12152  crth  12156  phimullem  12157  znnen  12331  ennnfonelemkh  12345  ismgmn0  12589  lgsdir2lem2  13570  lgsdir2lem3  13571  bj-el2oss1o  13655  2o01f  13876  nninfalllem1  13888  nninfall  13889