Theorem eleqtrrd 2255

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

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

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-cleq 2168  df-clel 2171

This theorem is referenced by:  3eltr4d  2259  rspc2vd  3123  exmidsssnc  4198  tfrexlem  6325  nnsucuniel  6486  erref  6545  en1uniel  6794  fin0  6875  fin0or  6876  prarloclemarch2  7393  fzopth  10031  fzoss2  10142  fzosubel3  10166  elfzomin  10176  elfzonlteqm1  10180  fzoend  10192  fzofzp1  10197  fzofzp1b  10198  peano2fzor  10202  zmodfzo  10317  frecuzrdg0  10383  frecuzrdgsuc  10384  frecuzrdgdomlem  10387  frecuzrdg0t  10392  frecuzrdgsuctlem  10393  seq3f1olemqsum  10470  bcn2  10712  summodclem2a  11357  fisumss  11368  fsumm1  11392  fisumcom2  11414  prodmodclem2a  11552  fprodm1  11574  fprodcom2fi  11602  ennnfonelemex  12382  ctinfomlemom  12395  mndpropd  12707  grpsubpropd2  12836  srgpcomp  12970  srgpcompp  12971  srgpcomppsc  12972  ringpropd  13013  mulgass3  13049  lmtopcnp  13321  txopn  13336  blpnfctr  13510  metcnpi  13586  metcnpi2  13587  cncfmpt2fcntop  13656  limcimolemlt  13704  cnplimclemr  13709  limccnp2lem  13716  limccnp2cntop  13717  dvidlemap  13731  dvcnp2cntop  13734  dvcn  13735  dvaddxxbr  13736  dvmulxxbr  13737  dvef  13759