Theorem eleqtrrd 2309

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  3eltr4d  2313  rspc2vd  3193  exmidsssnc  4287  funopsn  5817  tfrexlem  6480  nnsucuniel  6641  erref  6700  en1uniel  6956  fin0  7047  fin0or  7048  pw1if  7410  prarloclemarch2  7606  fzopth  10257  fzoss2  10370  fz1fzo0m1  10389  fzo0addel  10394  fzo0addelr  10395  elfzoext  10398  fzosubel3  10402  elfzomin  10412  elfzonlteqm1  10416  fzoend  10428  fzofzp1  10433  fzofzp1b  10434  peano2fzor  10438  zmodfzo  10569  frecuzrdg0  10635  frecuzrdgsuc  10636  frecuzrdgdomlem  10639  frecuzrdg0t  10644  frecuzrdgsuctlem  10645  seq3f1olemqsum  10735  seqf1oglem2  10742  bcn2  10986  ccats1val2  11171  swrdccat2  11203  pfxccat1  11234  swrdswrd  11237  pfxccatin12  11265  summodclem2a  11892  fisumss  11903  fsumm1  11927  fisumcom2  11949  prodmodclem2a  12087  fprodm1  12109  fprodcom2fi  12137  ennnfonelemex  12985  ctinfomlemom  12998  strslfv3  13078  bassetsnn  13089  gsumpropd2  13426  sgrppropd  13446  mndpropd  13473  imasmnd  13486  grpsubpropd2  13638  imasgrp  13648  subg0  13717  issubg2m  13726  ghmrn  13794  0ghm  13795  resghm2  13798  ghmco  13801  rngpropd  13918  imasrng  13919  srgpcomp  13953  srgpcompp  13954  srgpcomppsc  13955  ringpropd  14001  imasring  14027  qusring2  14029  mulgass3  14048  rhmopp  14140  lringuplu  14160  aprcotr  14249  lmodprop2d  14312  islssmd  14323  2idl0  14476  2idl1  14477  qus2idrng  14489  qus1  14490  qusrhm  14492  znf1o  14615  psrbaglesuppg  14636  psr0cl  14645  psrnegcl  14647  psr1clfi  14652  mplsubgfilemm  14662  lmtopcnp  14924  txopn  14939  blpnfctr  15113  metcnpi  15189  metcnpi2  15190  cncfmpt2fcntop  15273  limcimolemlt  15338  cnplimclemr  15343  limccnp2lem  15350  limccnp2cntop  15351  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvcnp2cntop  15373  dvcn  15374  dvaddxxbr  15375  dvmulxxbr  15376  dvef  15401  lgseisenlem3  15751  lgseisenlem4  15752  iedgedgg  15861  upgrex  15903  upgr1eopdc  15923  usgredg3  16012  edginwlkd  16066