Theorem eleqtrrd 2314

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  3eltr4d  2318  rspc2vd  3209  exmidsssnc  4318  funopsn  5862  tfrexlem  6567  nnsucuniel  6730  erref  6789  en1uniel  7046  fin0  7144  fin0or  7145  pw1if  7537  prarloclemarch2  7736  fzopth  10398  fzoss2  10512  fz1fzo0m1  10532  fzo0addel  10537  fzo0addelr  10538  elfzoext  10541  fzosubel3  10545  elfzomin  10555  elfzonlteqm1  10559  fzoend  10571  fzofzp1  10576  fzofzp1b  10577  peano2fzor  10581  zmodfzo  10713  frecuzrdg0  10779  frecuzrdgsuc  10780  frecuzrdgdomlem  10783  frecuzrdg0t  10788  frecuzrdgsuctlem  10789  seq3f1olemqsum  10879  seqf1oglem2  10886  bcn2  11130  ccats1val2  11332  swrdccat2  11367  pfxccat1  11398  swrdswrd  11401  pfxccatin12  11429  summodclem2a  12071  fisumss  12082  fsumm1  12106  fisumcom2  12128  prodmodclem2a  12266  fprodm1  12288  fprodcom2fi  12316  ennnfonelemex  13182  ctinfomlemom  13195  strslfv3  13275  bassetsnn  13286  gsumpropd2  13623  sgrppropd  13643  mndpropd  13670  imasmnd  13683  grpsubpropd2  13835  imasgrp  13845  subg0  13914  issubg2m  13923  ghmrn  13991  0ghm  13992  resghm2  13995  ghmco  13998  rngpropd  14116  imasrng  14117  srgpcomp  14151  srgpcompp  14152  srgpcomppsc  14153  ringpropd  14199  imasring  14225  qusring2  14227  mulgass3  14246  rhmopp  14338  lringuplu  14358  aprcotr  14448  lmodprop2d  14513  islssmd  14524  2idl0  14677  2idl1  14678  qus2idrng  14690  qus1  14691  qusrhm  14693  znf1o  14816  psrbaglesuppg  14838  psrbagaddclfi  14842  psr0cl  14853  psrnegcl  14855  psr1clfi  14860  mplsubgfilemm  14870  lmtopcnp  15132  txopn  15147  blpnfctr  15321  metcnpi  15397  metcnpi2  15398  cncfmpt2fcntop  15481  limcimolemlt  15546  cnplimclemr  15551  limccnp2lem  15558  limccnp2cntop  15559  dvidlemap  15573  dvidrelem  15574  dvidsslem  15575  dvcnp2cntop  15581  dvcn  15582  dvaddxxbr  15583  dvmulxxbr  15584  dvef  15609  lgseisenlem3  15962  lgseisenlem4  15963  iedgedgg  16073  upgrex  16115  upgr1eopdc  16135  upgr1een  16136  umgr1een  16137  usgredg3  16226  uspgr1eopdc  16255  usgr1eop  16257  vtxdfifiun  16309  1loopgruspgr  16315  1loopgrvd2fi  16317  1loopgrvd0fi  16318  1hevtxdg0fi  16319  1hevtxdg1en  16320  1hegrvtxdg1fi  16321  edginwlkd  16367  wlkres  16391  trlsegvdegfi  16479  eupth2lem3lem1fi  16480  eupth2lem3lem2fi  16481  eupth2lem3lem6fi  16483  eupth2lem3lem4fi  16485