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  13835  txopn  13850  blpnfctr  14024  metcnpi  14100  metcnpi2  14101  cncfmpt2fcntop  14170  limcimolemlt  14218  cnplimclemr  14223  limccnp2lem  14230  limccnp2cntop  14231  dvidlemap  14245  dvcnp2cntop  14248  dvcn  14249  dvaddxxbr  14250  dvmulxxbr  14251  dvef  14273