Theorem eleq2s 2129

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

Syntax hints:   -> wi 4   = wceq 1242   e. wcel 1390

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033

This theorem is referenced by:  elrabi  2689  opelopabsb  3988  epelg  4018  elxpi  4304  optocl  4359  fvmptss2  5190  fvmptssdm  5198  acexmidlemcase  5450  elmpt2cl  5640  mpt2xopn0yelv  5795  tfr2a  5877  2oconcl  5961  ecexr  6047  ectocld  6108  ecoptocl  6129  eroveu  6133  dmaddpqlem  6361  nqpi  6362  nq0nn  6425  0nsr  6677  axaddcl  6750  axmulcl  6752  peano2uzs  8303  fzossnn0  8801  frecfzennn  8884