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  6610  nnsucuniel  6773  erref  6832  en1uniel  7097  fin0  7195  fin0or  7196  funisfsuppdc  7298  pw1if  7590  prarloclemarch2  7792  fzopth  10483  fzoss2  10597  fz1fzo0m1  10617  fzo0addel  10622  fzo0addelr  10623  elfzoext  10626  fzosubel3  10630  elfzomin  10640  elfzonlteqm1  10644  fzoend  10656  fzofzp1  10661  fzofzp1b  10662  peano2fzor  10666  zmodfzo  10804  frecuzrdg0  10870  frecuzrdgsuc  10871  frecuzrdgdomlem  10874  frecuzrdg0t  10879  frecuzrdgsuctlem  10880  seq3f1olemqsum  10970  seqf1oglem2  10977  bcn2  11223  ccats1val2  11429  swrdccat2  11464  pfxccat1  11495  swrdswrd  11498  pfxccatin12  11526  summodclem2a  12172  fisumss  12183  fsumm1  12207  fisumcom2  12229  prodmodclem2a  12367  fprodm1  12389  fprodcom2fi  12417  ballotfilemrv  13320  ennnfonelemex  13362  ctinfomlemom  13375  strslfv3  13455  bassetsnn  13466  sgrppropd  13786  mndpropd  13811  imasmnd  13818  grpsubpropd2  13968  imasgrp  13972  subg0  14041  issubg2m  14050  ghmrn  14118  0ghm  14119  resghm2  14122  ghmco  14125  rngpropd  14360  imasrng  14361  srgpcomp  14400  srgpcompp  14401  srgpcomppsc  14402  ringpropd  14449  imasring  14477  qusring2  14479  mulgass3  14499  rhmopp  14591  lringuplu  14611  aprcotr  14705  lmodprop2d  14793  islssmd  14804  2idl0  14957  2idl1  14958  qus2idrng  14970  qus1  14971  qusrhm  14973  znf1o  15094  assapropd  15122  snifpsrbagfi  15168  psrbaglesuppg  15170  psrbagaddclfi  15173  psrbaglefifi  15175  psrbagmaxlemfi  15180  psr0cl  15200  psrnegcl  15202  psr1clfi  15207  mvrffi  15218  lmtopcnp  15493  txopn  15508  blpnfctr  15682  metcnpi  15758  metcnpi2  15759  cncfmpt2fcntop  15842  limcimolemlt  15907  cnplimclemr  15912  limccnp2lem  15919  limccnp2cntop  15920  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvcnp2cntop  15942  dvcn  15943  dvaddxxbr  15944  dvmulxxbr  15945  dvef  15970  lgseisenlem3  16413  lgseisenlem4  16414  iedgedgg  16524  upgrex  16566  upgr1eopdc  16586  upgr1een  16587  umgr1een  16588  usgredg3  16677  uspgr1eopdc  16706  usgr1eop  16708  vtxdfifiun  16760  1loopgruspgr  16766  1loopgrvd2fi  16768  1loopgrvd0fi  16769  1hevtxdg0fi  16770  1hevtxdg1en  16771  1hegrvtxdg1fi  16772  edginwlkd  16818  wlkres  16842  trlsegvdegfi  16930  eupth2lem3lem1fi  16931  eupth2lem3lem2fi  16932  eupth2lem3lem6fi  16934  eupth2lem3lem4fi  16936  idjudju  17269