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  3194  exmidsssnc  4291  funopsn  5825  tfrexlem  6495  nnsucuniel  6658  erref  6717  en1uniel  6973  fin0  7067  fin0or  7068  pw1if  7433  prarloclemarch2  7629  fzopth  10286  fzoss2  10399  fz1fzo0m1  10418  fzo0addel  10423  fzo0addelr  10424  elfzoext  10427  fzosubel3  10431  elfzomin  10441  elfzonlteqm1  10445  fzoend  10457  fzofzp1  10462  fzofzp1b  10463  peano2fzor  10467  zmodfzo  10599  frecuzrdg0  10665  frecuzrdgsuc  10666  frecuzrdgdomlem  10669  frecuzrdg0t  10674  frecuzrdgsuctlem  10675  seq3f1olemqsum  10765  seqf1oglem2  10772  bcn2  11016  ccats1val2  11207  swrdccat2  11242  pfxccat1  11273  swrdswrd  11276  pfxccatin12  11304  summodclem2a  11932  fisumss  11943  fsumm1  11967  fisumcom2  11989  prodmodclem2a  12127  fprodm1  12149  fprodcom2fi  12177  ennnfonelemex  13025  ctinfomlemom  13038  strslfv3  13118  bassetsnn  13129  gsumpropd2  13466  sgrppropd  13486  mndpropd  13513  imasmnd  13526  grpsubpropd2  13678  imasgrp  13688  subg0  13757  issubg2m  13766  ghmrn  13834  0ghm  13835  resghm2  13838  ghmco  13841  rngpropd  13958  imasrng  13959  srgpcomp  13993  srgpcompp  13994  srgpcomppsc  13995  ringpropd  14041  imasring  14067  qusring2  14069  mulgass3  14088  rhmopp  14180  lringuplu  14200  aprcotr  14289  lmodprop2d  14352  islssmd  14363  2idl0  14516  2idl1  14517  qus2idrng  14529  qus1  14530  qusrhm  14532  znf1o  14655  psrbaglesuppg  14676  psr0cl  14685  psrnegcl  14687  psr1clfi  14692  mplsubgfilemm  14702  lmtopcnp  14964  txopn  14979  blpnfctr  15153  metcnpi  15229  metcnpi2  15230  cncfmpt2fcntop  15313  limcimolemlt  15378  cnplimclemr  15383  limccnp2lem  15390  limccnp2cntop  15391  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvcnp2cntop  15413  dvcn  15414  dvaddxxbr  15415  dvmulxxbr  15416  dvef  15441  lgseisenlem3  15791  lgseisenlem4  15792  iedgedgg  15902  upgrex  15944  upgr1eopdc  15964  usgredg3  16053  uspgr1eopdc  16082  usgr1eop  16084  vtxdfifiun  16103  1loopgruspgr  16109  1loopgrvd2fi  16111  1loopgrvd0fi  16112  1hevtxdg0fi  16113  edginwlkd  16152  wlkres  16174