Theorem eleq2s 2174

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

Syntax hints:   -> wi 4   = wceq 1285   e. wcel 1434

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078

This theorem is referenced by:  elrabi  2747  opelopabsb  4023  epelg  4053  reg3exmidlemwe  4329  elxpi  4387  optocl  4442  fvmptss2  5279  fvmptssdm  5287  acexmidlemcase  5538  elmpt2cl  5729  mpt2xopn0yelv  5888  tfr2a  5970  tfri1dALT  6000  2oconcl  6086  ecexr  6177  ectocld  6238  ecoptocl  6259  eroveu  6263  diffitest  6421  en2eqpr  6434  dmaddpqlem  6629  nqpi  6630  nq0nn  6694  0nsr  6988  axaddcl  7094  axmulcl  7096  peano2uzs  8753  fzossnn0  9261  rebtwn2zlemstep  9339  fldiv4p1lem1div2  9387  frecfzennn  9508  facnn  9751  bcpasc  9790  rexuz3  10014  rexanuz2  10015  r19.2uz  10017  cau4  10140  caubnd2  10141  climshft2  10283  climaddc1  10305  climmulc2  10307  climsubc1  10308  climsubc2  10309  climlec2  10317  climcau  10322  climcaucn  10326  infssuzex  10489  infssuzledc  10490  3prm  10654  znnen  10709