Theorem eleq2s 2291

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 2263	. 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 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  elrabi  2917  opelopabsb  4294  epelg  4325  reg3exmidlemwe  4615  elxpi  4679  optocl  4739  elfvm  5591  fvmptss2  5636  fvmptssdm  5646  acexmidlemcase  5917  elmpocl  6118  mpoxopn0yelv  6297  tfr2a  6379  tfri1dALT  6409  2oconcl  6497  el2oss1o  6501  ecexr  6597  ectocld  6660  ecoptocl  6681  eroveu  6685  mapsnconst  6753  diffitest  6948  en2eqpr  6968  ctssdccl  7177  nninfwlpoimlemginf  7242  exmidonfinlem  7260  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  dmaddpqlem  7444  nqpi  7445  nq0nn  7509  0nsr  7816  suplocsrlempr  7874  cnm  7899  axaddcl  7931  axmulcl  7933  aprcl  8673  aptap  8677  peano2uzs  9658  fzssnn  10143  fzossnn0  10251  infssuzex  10323  infssuzledc  10324  rebtwn2zlemstep  10342  fldiv4p1lem1div2  10395  frecfzennn  10518  fser0const  10627  facnn  10819  bcpasc  10858  hashfzo0  10915  rexuz3  11155  rexanuz2  11156  r19.2uz  11158  cau4  11281  caubnd2  11282  climshft2  11471  climaddc1  11494  climmulc2  11496  climsubc1  11497  climsubc2  11498  climlec2  11506  climcau  11512  climcaucn  11516  iserabs  11640  binomlem  11648  isumshft  11655  cvgratgt0  11698  clim2divap  11705  ntrivcvgap  11713  fprodntrivap  11749  fprodeq0  11782  3prm  12296  phicl2  12382  phibndlem  12384  dfphi2  12388  crth  12392  phimullem  12393  znnen  12615  ennnfonelemkh  12629  fvprif  12986  xpsfeq  12988  ismgmn0  13001  zrhval  14173  lgsdir2lem2  15270  lgsdir2lem3  15271  lgsquadlem2  15319  2lgslem1b  15330  bj-el2oss1o  15420  2o01f  15641  nninfalllem1  15652  nninfall  15653