Theorem eleqtrrd 2285

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  3eltr4d  2289  rspc2vd  3162  exmidsssnc  4248  funopsn  5764  tfrexlem  6422  nnsucuniel  6583  erref  6642  en1uniel  6898  fin0  6984  fin0or  6985  prarloclemarch2  7534  fzopth  10185  fzoss2  10298  fzo0addel  10319  fzo0addelr  10320  elfzoext  10323  fzosubel3  10327  elfzomin  10337  elfzonlteqm1  10341  fzoend  10353  fzofzp1  10358  fzofzp1b  10359  peano2fzor  10363  zmodfzo  10494  frecuzrdg0  10560  frecuzrdgsuc  10561  frecuzrdgdomlem  10564  frecuzrdg0t  10569  frecuzrdgsuctlem  10570  seq3f1olemqsum  10660  seqf1oglem2  10667  bcn2  10911  ccats1val2  11095  swrdccat2  11127  pfxccat1  11156  summodclem2a  11725  fisumss  11736  fsumm1  11760  fisumcom2  11782  prodmodclem2a  11920  fprodm1  11942  fprodcom2fi  11970  ennnfonelemex  12818  ctinfomlemom  12831  strslfv3  12911  gsumpropd2  13258  sgrppropd  13278  mndpropd  13305  imasmnd  13318  grpsubpropd2  13470  imasgrp  13480  subg0  13549  issubg2m  13558  ghmrn  13626  0ghm  13627  resghm2  13630  ghmco  13633  rngpropd  13750  imasrng  13751  srgpcomp  13785  srgpcompp  13786  srgpcomppsc  13787  ringpropd  13833  imasring  13859  qusring2  13861  mulgass3  13880  rhmopp  13971  lringuplu  13991  aprcotr  14080  lmodprop2d  14143  islssmd  14154  2idl0  14307  2idl1  14308  qus2idrng  14320  qus1  14321  qusrhm  14323  znf1o  14446  psrbaglesuppg  14467  psr0cl  14476  psrnegcl  14478  psr1clfi  14483  mplsubgfilemm  14493  lmtopcnp  14755  txopn  14770  blpnfctr  14944  metcnpi  15020  metcnpi2  15021  cncfmpt2fcntop  15104  limcimolemlt  15169  cnplimclemr  15174  limccnp2lem  15181  limccnp2cntop  15182  dvidlemap  15196  dvidrelem  15197  dvidsslem  15198  dvcnp2cntop  15204  dvcn  15205  dvaddxxbr  15206  dvmulxxbr  15207  dvef  15232  lgseisenlem3  15582  lgseisenlem4  15583  iedgedgg  15688