Theorem eleq2s 2324

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 2296	. 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 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

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

This theorem is referenced by:  elrabi  2957  opelopabsb  4352  epelg  4385  reg3exmidlemwe  4675  elxpi  4739  optocl  4800  elfvm  5668  elfvfvex  5669  fvmbr  5670  fvmptss2  5717  fvmptssdm  5727  acexmidlemcase  6008  elmpocl  6212  mpoxopn0yelv  6400  tfr2a  6482  tfri1dALT  6512  2oconcl  6602  el2oss1o  6606  ecexr  6702  ectocld  6765  ecoptocl  6786  eroveu  6790  mapsnconst  6858  diffitest  7069  en2eqpr  7092  ctssdccl  7301  nninfwlpoimlemginf  7366  exmidonfinlem  7394  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  acnrcl  7406  dmaddpqlem  7587  nqpi  7588  nq0nn  7652  0nsr  7959  suplocsrlempr  8017  cnm  8042  axaddcl  8074  axmulcl  8076  aprcl  8816  aptap  8820  peano2uzs  9808  fzssnn  10293  fzossnn0  10402  infssuzex  10483  infssuzledc  10484  rebtwn2zlemstep  10502  fldiv4p1lem1div2  10555  frecfzennn  10678  fser0const  10787  facnn  10979  bcpasc  11018  hashfzo0  11077  ccatval2  11165  ccatass  11175  pfxclz  11250  wrdeqs1cat  11291  rexuz3  11541  rexanuz2  11542  r19.2uz  11544  cau4  11667  caubnd2  11668  climshft2  11857  climaddc1  11880  climmulc2  11882  climsubc1  11883  climsubc2  11884  climlec2  11892  climcau  11898  climcaucn  11902  iserabs  12026  binomlem  12034  isumshft  12041  cvgratgt0  12084  clim2divap  12091  ntrivcvgap  12099  fprodntrivap  12135  fprodeq0  12168  3prm  12690  phicl2  12776  phibndlem  12778  dfphi2  12782  crth  12786  phimullem  12787  znnen  13009  ennnfonelemkh  13023  fvprif  13416  xpsfeq  13418  ismgmn0  13431  zrhval  14621  lgsdir2lem2  15748  lgsdir2lem3  15749  lgsquadlem2  15797  2lgslem1b  15808  1vgrex  15861  usgredg2v  16063  bj-el2oss1o  16306  2o01f  16529  nninfalllem1  16546  nninfall  16547