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  3210  exmidsssnc  4321  funopsn  5865  tfrexlem  6578  nnsucuniel  6741  erref  6800  en1uniel  7057  fin0  7155  fin0or  7156  pw1if  7548  prarloclemarch2  7750  fzopth  10416  fzoss2  10530  fz1fzo0m1  10550  fzo0addel  10555  fzo0addelr  10556  elfzoext  10559  fzosubel3  10563  elfzomin  10573  elfzonlteqm1  10577  fzoend  10589  fzofzp1  10594  fzofzp1b  10595  peano2fzor  10599  zmodfzo  10733  frecuzrdg0  10799  frecuzrdgsuc  10800  frecuzrdgdomlem  10803  frecuzrdg0t  10808  frecuzrdgsuctlem  10809  seq3f1olemqsum  10899  seqf1oglem2  10906  bcn2  11151  ccats1val2  11353  swrdccat2  11388  pfxccat1  11419  swrdswrd  11422  pfxccatin12  11450  summodclem2a  12092  fisumss  12103  fsumm1  12127  fisumcom2  12149  prodmodclem2a  12287  fprodm1  12309  fprodcom2fi  12337  ballotfilemrv  13207  ennnfonelemex  13249  ctinfomlemom  13262  strslfv3  13342  bassetsnn  13353  gsumpropd2  13656  sgrppropd  13676  mndpropd  13701  imasmnd  13708  grpsubpropd2  13860  imasgrp  13864  subg0  13933  issubg2m  13942  ghmrn  14010  0ghm  14011  resghm2  14014  ghmco  14017  rngpropd  14194  imasrng  14195  srgpcomp  14233  srgpcompp  14234  srgpcomppsc  14235  ringpropd  14281  imasring  14307  qusring2  14309  mulgass3  14329  rhmopp  14421  lringuplu  14441  aprcotr  14535  lmodprop2d  14622  islssmd  14633  2idl0  14786  2idl1  14787  qus2idrng  14799  qus1  14800  qusrhm  14802  znf1o  14925  psrbaglesuppg  14947  psrbagaddclfi  14951  psr0cl  14962  psrnegcl  14964  psr1clfi  14969  mplsubgfilemm  14979  lmtopcnp  15241  txopn  15256  blpnfctr  15430  metcnpi  15506  metcnpi2  15507  cncfmpt2fcntop  15590  limcimolemlt  15655  cnplimclemr  15660  limccnp2lem  15667  limccnp2cntop  15668  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvcnp2cntop  15690  dvcn  15691  dvaddxxbr  15692  dvmulxxbr  15693  dvef  15718  lgseisenlem3  16071  lgseisenlem4  16072  iedgedgg  16182  upgrex  16224  upgr1eopdc  16244  upgr1een  16245  umgr1een  16246  usgredg3  16335  uspgr1eopdc  16364  usgr1eop  16366  vtxdfifiun  16418  1loopgruspgr  16424  1loopgrvd2fi  16426  1loopgrvd0fi  16427  1hevtxdg0fi  16428  1hevtxdg1en  16429  1hegrvtxdg1fi  16430  edginwlkd  16476  wlkres  16500  trlsegvdegfi  16588  eupth2lem3lem1fi  16589  eupth2lem3lem2fi  16590  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594