Theorem eleqtrrd 2257

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  3eltr4d  2261  rspc2vd  3127  exmidsssnc  4205  tfrexlem  6337  nnsucuniel  6498  erref  6557  en1uniel  6806  fin0  6887  fin0or  6888  prarloclemarch2  7420  fzopth  10063  fzoss2  10174  fzosubel3  10198  elfzomin  10208  elfzonlteqm1  10212  fzoend  10224  fzofzp1  10229  fzofzp1b  10230  peano2fzor  10234  zmodfzo  10349  frecuzrdg0  10415  frecuzrdgsuc  10416  frecuzrdgdomlem  10419  frecuzrdg0t  10424  frecuzrdgsuctlem  10425  seq3f1olemqsum  10502  bcn2  10746  summodclem2a  11391  fisumss  11402  fsumm1  11426  fisumcom2  11448  prodmodclem2a  11586  fprodm1  11608  fprodcom2fi  11636  ennnfonelemex  12417  ctinfomlemom  12430  mndpropd  12846  grpsubpropd2  12980  subg0  13045  issubg2m  13054  srgpcomp  13178  srgpcompp  13179  srgpcomppsc  13180  ringpropd  13222  mulgass3  13259  lringuplu  13342  aprcotr  13380  lmodprop2d  13443  islssmd  13451  lmtopcnp  13789  txopn  13804  blpnfctr  13978  metcnpi  14054  metcnpi2  14055  cncfmpt2fcntop  14124  limcimolemlt  14172  cnplimclemr  14177  limccnp2lem  14184  limccnp2cntop  14185  dvidlemap  14199  dvcnp2cntop  14202  dvcn  14203  dvaddxxbr  14204  dvmulxxbr  14205  dvef  14227