Theorem eleqtrrd 2220

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

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  3eltr4d  2224  exmidsssnc  4134  tfrexlem  6239  nnsucuniel  6399  erref  6457  en1uniel  6706  fin0  6787  fin0or  6788  prarloclemarch2  7251  fzopth  9872  fzoss2  9980  fzosubel3  10004  elfzomin  10014  elfzonlteqm1  10018  fzoend  10030  fzofzp1  10035  fzofzp1b  10036  peano2fzor  10040  zmodfzo  10151  frecuzrdg0  10217  frecuzrdgsuc  10218  frecuzrdgdomlem  10221  frecuzrdg0t  10226  frecuzrdgsuctlem  10227  seq3f1olemqsum  10304  bcn2  10542  summodclem2a  11182  fisumss  11193  fsumm1  11217  fisumcom2  11239  prodmodclem2a  11377  ennnfonelemex  11963  ctinfomlemom  11976  lmtopcnp  12458  txopn  12473  blpnfctr  12647  metcnpi  12723  metcnpi2  12724  cncfmpt2fcntop  12793  limcimolemlt  12841  cnplimclemr  12846  limccnp2lem  12853  limccnp2cntop  12854  dvidlemap  12868  dvcnp2cntop  12871  dvcn  12872  dvaddxxbr  12873  dvmulxxbr  12874  dvef  12896