Theorem eleqtrrd 2318

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  3eltr4d  2322  rspc2vd  3216  exmidsssnc  4342  funopsn  5894  tfrexlem  6609  nnsucuniel  6772  erref  6831  en1uniel  7095  fin0  7193  fin0or  7194  pw1if  7590  prarloclemarch2  7792  fzopth  10484  fzoss2  10598  fz1fzo0m1  10618  fzo0addel  10623  fzo0addelr  10624  elfzoext  10627  fzosubel3  10631  elfzomin  10641  elfzonlteqm1  10645  fzoend  10657  fzofzp1  10662  fzofzp1b  10663  peano2fzor  10667  zmodfzo  10805  frecuzrdg0  10871  frecuzrdgsuc  10872  frecuzrdgdomlem  10875  frecuzrdg0t  10880  frecuzrdgsuctlem  10881  seq3f1olemqsum  10971  seqf1oglem2  10978  bcn2  11224  ccats1val2  11430  swrdccat2  11465  pfxccat1  11496  swrdswrd  11499  pfxccatin12  11527  summodclem2a  12173  fisumss  12184  fsumm1  12208  fisumcom2  12230  prodmodclem2a  12368  fprodm1  12390  fprodcom2fi  12418  ballotfilemrv  13321  ennnfonelemex  13363  ctinfomlemom  13376  strslfv3  13456  bassetsnn  13467  sgrppropd  13787  mndpropd  13812  imasmnd  13819  grpsubpropd2  13969  imasgrp  13973  subg0  14042  issubg2m  14051  ghmrn  14119  0ghm  14120  resghm2  14123  ghmco  14126  rngpropd  14361  imasrng  14362  srgpcomp  14401  srgpcompp  14402  srgpcomppsc  14403  ringpropd  14450  imasring  14478  qusring2  14480  mulgass3  14500  rhmopp  14592  lringuplu  14612  aprcotr  14706  lmodprop2d  14794  islssmd  14805  2idl0  14958  2idl1  14959  qus2idrng  14971  qus1  14972  qusrhm  14974  znf1o  15095  assapropd  15123  psrbaglesuppg  15166  psrbagaddclfi  15170  psrbaglefifi  15172  psr0cl  15191  psrnegcl  15193  psr1clfi  15198  mplsubgfilemm  15214  lmtopcnp  15476  txopn  15491  blpnfctr  15665  metcnpi  15741  metcnpi2  15742  cncfmpt2fcntop  15825  limcimolemlt  15890  cnplimclemr  15895  limccnp2lem  15902  limccnp2cntop  15903  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvcnp2cntop  15925  dvcn  15926  dvaddxxbr  15927  dvmulxxbr  15928  dvef  15953  lgseisenlem3  16396  lgseisenlem4  16397  iedgedgg  16507  upgrex  16549  upgr1eopdc  16569  upgr1een  16570  umgr1een  16571  usgredg3  16660  uspgr1eopdc  16689  usgr1eop  16691  vtxdfifiun  16743  1loopgruspgr  16749  1loopgrvd2fi  16751  1loopgrvd0fi  16752  1hevtxdg0fi  16753  1hevtxdg1en  16754  1hegrvtxdg1fi  16755  edginwlkd  16801  wlkres  16825  trlsegvdegfi  16913  eupth2lem3lem1fi  16914  eupth2lem3lem2fi  16915  eupth2lem3lem6fi  16917  eupth2lem3lem4fi  16919  idjudju  17252