Theorem eleqtrrd 2158

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 2086	. 2 |- ( ph -> B = C )
4	1, 3	eleqtrd 2157	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1284   e. wcel 1433

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  3eltr4d  2162  tfrexlem  5971  erref  6149  en1uniel  6307  fin0  6369  fin0or  6370  prarloclemarch2  6609  fzopth  9079  fzoss2  9181  fzosubel3  9205  elfzomin  9215  elfzonlteqm1  9219  fzoend  9231  fzofzp1  9236  fzofzp1b  9237  peano2fzor  9241  zmodfzo  9349  frecuzrdgcl  9415  frecuzrdg0  9416  frecuzrdgsuc  9417  bcn2  9691