Theorem eleqtrrd 2287

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  3eltr4d  2291  rspc2vd  3170  exmidsssnc  4263  funopsn  5785  tfrexlem  6443  nnsucuniel  6604  erref  6663  en1uniel  6919  fin0  7008  fin0or  7009  pw1if  7371  prarloclemarch2  7567  fzopth  10218  fzoss2  10331  fzo0addel  10354  fzo0addelr  10355  elfzoext  10358  fzosubel3  10362  elfzomin  10372  elfzonlteqm1  10376  fzoend  10388  fzofzp1  10393  fzofzp1b  10394  peano2fzor  10398  zmodfzo  10529  frecuzrdg0  10595  frecuzrdgsuc  10596  frecuzrdgdomlem  10599  frecuzrdg0t  10604  frecuzrdgsuctlem  10605  seq3f1olemqsum  10695  seqf1oglem2  10702  bcn2  10946  ccats1val2  11130  swrdccat2  11162  pfxccat1  11193  swrdswrd  11196  pfxccatin12  11224  summodclem2a  11807  fisumss  11818  fsumm1  11842  fisumcom2  11864  prodmodclem2a  12002  fprodm1  12024  fprodcom2fi  12052  ennnfonelemex  12900  ctinfomlemom  12913  strslfv3  12993  gsumpropd2  13340  sgrppropd  13360  mndpropd  13387  imasmnd  13400  grpsubpropd2  13552  imasgrp  13562  subg0  13631  issubg2m  13640  ghmrn  13708  0ghm  13709  resghm2  13712  ghmco  13715  rngpropd  13832  imasrng  13833  srgpcomp  13867  srgpcompp  13868  srgpcomppsc  13869  ringpropd  13915  imasring  13941  qusring2  13943  mulgass3  13962  rhmopp  14053  lringuplu  14073  aprcotr  14162  lmodprop2d  14225  islssmd  14236  2idl0  14389  2idl1  14390  qus2idrng  14402  qus1  14403  qusrhm  14405  znf1o  14528  psrbaglesuppg  14549  psr0cl  14558  psrnegcl  14560  psr1clfi  14565  mplsubgfilemm  14575  lmtopcnp  14837  txopn  14852  blpnfctr  15026  metcnpi  15102  metcnpi2  15103  cncfmpt2fcntop  15186  limcimolemlt  15251  cnplimclemr  15256  limccnp2lem  15263  limccnp2cntop  15264  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvcnp2cntop  15286  dvcn  15287  dvaddxxbr  15288  dvmulxxbr  15289  dvef  15314  lgseisenlem3  15664  lgseisenlem4  15665  iedgedgg  15772  upgrex  15814  upgr1eopdc  15831