Theorem eleq2s 2272

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 2244	. 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 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  elrabi  2891  opelopabsb  4261  epelg  4291  reg3exmidlemwe  4579  elxpi  4643  optocl  4703  fvmptss2  5592  fvmptssdm  5601  acexmidlemcase  5870  elmpocl  6069  mpoxopn0yelv  6240  tfr2a  6322  tfri1dALT  6352  2oconcl  6440  el2oss1o  6444  ecexr  6540  ectocld  6601  ecoptocl  6622  eroveu  6626  mapsnconst  6694  diffitest  6887  en2eqpr  6907  ctssdccl  7110  nninfwlpoimlemginf  7174  exmidonfinlem  7192  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  dmaddpqlem  7376  nqpi  7377  nq0nn  7441  0nsr  7748  suplocsrlempr  7806  cnm  7831  axaddcl  7863  axmulcl  7865  aprcl  8603  aptap  8607  peano2uzs  9584  fzssnn  10068  fzossnn0  10175  rebtwn2zlemstep  10253  fldiv4p1lem1div2  10305  frecfzennn  10426  fser0const  10516  facnn  10707  bcpasc  10746  hashfzo0  10803  rexuz3  10999  rexanuz2  11000  r19.2uz  11002  cau4  11125  caubnd2  11126  climshft2  11314  climaddc1  11337  climmulc2  11339  climsubc1  11340  climsubc2  11341  climlec2  11349  climcau  11355  climcaucn  11359  iserabs  11483  binomlem  11491  isumshft  11498  cvgratgt0  11541  clim2divap  11548  ntrivcvgap  11556  fprodntrivap  11592  fprodeq0  11625  infssuzex  11950  infssuzledc  11951  3prm  12128  phicl2  12214  phibndlem  12216  dfphi2  12220  crth  12224  phimullem  12225  znnen  12399  ennnfonelemkh  12413  fvprif  12762  xpsfeq  12764  ismgmn0  12777  lgsdir2lem2  14433  lgsdir2lem3  14434  bj-el2oss1o  14529  2o01f  14749  nninfalllem1  14760  nninfall  14761