Theorem eleqtrrd 2311

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

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

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 2213

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

This theorem is referenced by:  3eltr4d  2315  rspc2vd  3197  exmidsssnc  4299  funopsn  5838  tfrexlem  6543  nnsucuniel  6706  erref  6765  en1uniel  7021  fin0  7117  fin0or  7118  pw1if  7486  prarloclemarch2  7682  fzopth  10341  fzoss2  10454  fz1fzo0m1  10474  fzo0addel  10479  fzo0addelr  10480  elfzoext  10483  fzosubel3  10487  elfzomin  10497  elfzonlteqm1  10501  fzoend  10513  fzofzp1  10518  fzofzp1b  10519  peano2fzor  10523  zmodfzo  10655  frecuzrdg0  10721  frecuzrdgsuc  10722  frecuzrdgdomlem  10725  frecuzrdg0t  10730  frecuzrdgsuctlem  10731  seq3f1olemqsum  10821  seqf1oglem2  10828  bcn2  11072  ccats1val2  11266  swrdccat2  11301  pfxccat1  11332  swrdswrd  11335  pfxccatin12  11363  summodclem2a  12005  fisumss  12016  fsumm1  12040  fisumcom2  12062  prodmodclem2a  12200  fprodm1  12222  fprodcom2fi  12250  ennnfonelemex  13098  ctinfomlemom  13111  strslfv3  13191  bassetsnn  13202  gsumpropd2  13539  sgrppropd  13559  mndpropd  13586  imasmnd  13599  grpsubpropd2  13751  imasgrp  13761  subg0  13830  issubg2m  13839  ghmrn  13907  0ghm  13908  resghm2  13911  ghmco  13914  rngpropd  14032  imasrng  14033  srgpcomp  14067  srgpcompp  14068  srgpcomppsc  14069  ringpropd  14115  imasring  14141  qusring2  14143  mulgass3  14162  rhmopp  14254  lringuplu  14274  aprcotr  14364  lmodprop2d  14427  islssmd  14438  2idl0  14591  2idl1  14592  qus2idrng  14604  qus1  14605  qusrhm  14607  znf1o  14730  psrbaglesuppg  14751  psr0cl  14765  psrnegcl  14767  psr1clfi  14772  mplsubgfilemm  14782  lmtopcnp  15044  txopn  15059  blpnfctr  15233  metcnpi  15309  metcnpi2  15310  cncfmpt2fcntop  15393  limcimolemlt  15458  cnplimclemr  15463  limccnp2lem  15470  limccnp2cntop  15471  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvcnp2cntop  15493  dvcn  15494  dvaddxxbr  15495  dvmulxxbr  15496  dvef  15521  lgseisenlem3  15874  lgseisenlem4  15875  iedgedgg  15985  upgrex  16027  upgr1eopdc  16047  upgr1een  16048  umgr1een  16049  usgredg3  16138  uspgr1eopdc  16167  usgr1eop  16169  vtxdfifiun  16221  1loopgruspgr  16227  1loopgrvd2fi  16229  1loopgrvd0fi  16230  1hevtxdg0fi  16231  1hevtxdg1en  16232  1hegrvtxdg1fi  16233  edginwlkd  16279  wlkres  16303  trlsegvdegfi  16391  eupth2lem3lem1fi  16392  eupth2lem3lem2fi  16393  eupth2lem3lem6fi  16395  eupth2lem3lem4fi  16397