Theorem eleqtrrd 2114

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrrd.1	|- (ph -> A e. B)
eleqtrrd.2	|- (ph -> C = B)

Assertion

Ref	Expression
eleqtrrd	|- (ph -> A e. C)

Proof of Theorem eleqtrrd

Step	Hyp	Ref	Expression
1		eleqtrrd.1	. 2 |- (ph -> A e. B)
2		eleqtrrd.2	. . 3 |- (ph -> C = B)
3	2	eqcomd 2042	. 2 |- (ph -> B = C)
4	1, 3	eleqtrd 2113	1 |- (ph -> A e. C)

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:  3eltr4d  2118  tfrexlem  5889  erref  6062  en1uniel  6220  prarloclemarch2  6402  fzopth  8694  fzoss2  8798  fzosubel3  8822  elfzomin  8832  elfzonlteqm1  8836  fzoend  8848  fzofzp1  8853  fzofzp1b  8854  peano2fzor  8858  frecuzrdgcl  8880  frecuzrdg0  8881  frecuzrdgsuc  8882