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  4340  funopsn  5891  tfrexlem  6605  nnsucuniel  6768  erref  6827  en1uniel  7091  fin0  7189  fin0or  7190  pw1if  7584  prarloclemarch2  7786  fzopth  10477  fzoss2  10591  fz1fzo0m1  10611  fzo0addel  10616  fzo0addelr  10617  elfzoext  10620  fzosubel3  10624  elfzomin  10634  elfzonlteqm1  10638  fzoend  10650  fzofzp1  10655  fzofzp1b  10656  peano2fzor  10660  zmodfzo  10797  frecuzrdg0  10863  frecuzrdgsuc  10864  frecuzrdgdomlem  10867  frecuzrdg0t  10872  frecuzrdgsuctlem  10873  seq3f1olemqsum  10963  seqf1oglem2  10970  bcn2  11216  ccats1val2  11422  swrdccat2  11457  pfxccat1  11488  swrdswrd  11491  pfxccatin12  11519  summodclem2a  12164  fisumss  12175  fsumm1  12199  fisumcom2  12221  prodmodclem2a  12359  fprodm1  12381  fprodcom2fi  12409  ballotfilemrv  13312  ennnfonelemex  13354  ctinfomlemom  13367  strslfv3  13447  bassetsnn  13458  sgrppropd  13777  mndpropd  13802  imasmnd  13809  grpsubpropd2  13959  imasgrp  13963  subg0  14032  issubg2m  14041  ghmrn  14109  0ghm  14110  resghm2  14113  ghmco  14116  rngpropd  14303  imasrng  14304  srgpcomp  14343  srgpcompp  14344  srgpcomppsc  14345  ringpropd  14392  imasring  14418  qusring2  14420  mulgass3  14440  rhmopp  14532  lringuplu  14552  aprcotr  14646  lmodprop2d  14734  islssmd  14745  2idl0  14898  2idl1  14899  qus2idrng  14911  qus1  14912  qusrhm  14914  znf1o  15035  assapropd  15063  psrbaglesuppg  15106  psrbagaddclfi  15110  psr0cl  15121  psrnegcl  15123  psr1clfi  15128  mplsubgfilemm  15138  lmtopcnp  15400  txopn  15415  blpnfctr  15589  metcnpi  15665  metcnpi2  15666  cncfmpt2fcntop  15749  limcimolemlt  15814  cnplimclemr  15819  limccnp2lem  15826  limccnp2cntop  15827  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvcnp2cntop  15849  dvcn  15850  dvaddxxbr  15851  dvmulxxbr  15852  dvef  15877  lgseisenlem3  16289  lgseisenlem4  16290  iedgedgg  16400  upgrex  16442  upgr1eopdc  16462  upgr1een  16463  umgr1een  16464  usgredg3  16553  uspgr1eopdc  16582  usgr1eop  16584  vtxdfifiun  16636  1loopgruspgr  16642  1loopgrvd2fi  16644  1loopgrvd0fi  16645  1hevtxdg0fi  16646  1hevtxdg1en  16647  1hegrvtxdg1fi  16648  edginwlkd  16694  wlkres  16718  trlsegvdegfi  16806  eupth2lem3lem1fi  16807  eupth2lem3lem2fi  16808  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812