Theorem eleqtrrd 2311

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrrd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrrd.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
eleqtrrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrd

Step	Hyp	Ref	Expression
1		eleqtrrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrrd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2237	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2310	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  3eltr4d  2315  rspc2vd  3196  exmidsssnc  4293  funopsn  5830  tfrexlem  6500  nnsucuniel  6663  erref  6722  en1uniel  6978  fin0  7074  fin0or  7075  pw1if  7443  prarloclemarch2  7639  fzopth  10296  fzoss2  10409  fz1fzo0m1  10429  fzo0addel  10434  fzo0addelr  10435  elfzoext  10438  fzosubel3  10442  elfzomin  10452  elfzonlteqm1  10456  fzoend  10468  fzofzp1  10473  fzofzp1b  10474  peano2fzor  10478  zmodfzo  10610  frecuzrdg0  10676  frecuzrdgsuc  10677  frecuzrdgdomlem  10680  frecuzrdg0t  10685  frecuzrdgsuctlem  10686  seq3f1olemqsum  10776  seqf1oglem2  10783  bcn2  11027  ccats1val2  11221  swrdccat2  11256  pfxccat1  11287  swrdswrd  11290  pfxccatin12  11318  summodclem2a  11960  fisumss  11971  fsumm1  11995  fisumcom2  12017  prodmodclem2a  12155  fprodm1  12177  fprodcom2fi  12205  ennnfonelemex  13053  ctinfomlemom  13066  strslfv3  13146  bassetsnn  13157  gsumpropd2  13494  sgrppropd  13514  mndpropd  13541  imasmnd  13554  grpsubpropd2  13706  imasgrp  13716  subg0  13785  issubg2m  13794  ghmrn  13862  0ghm  13863  resghm2  13866  ghmco  13869  rngpropd  13987  imasrng  13988  srgpcomp  14022  srgpcompp  14023  srgpcomppsc  14024  ringpropd  14070  imasring  14096  qusring2  14098  mulgass3  14117  rhmopp  14209  lringuplu  14229  aprcotr  14318  lmodprop2d  14381  islssmd  14392  2idl0  14545  2idl1  14546  qus2idrng  14558  qus1  14559  qusrhm  14561  znf1o  14684  psrbaglesuppg  14705  psr0cl  14714  psrnegcl  14716  psr1clfi  14721  mplsubgfilemm  14731  lmtopcnp  14993  txopn  15008  blpnfctr  15182  metcnpi  15258  metcnpi2  15259  cncfmpt2fcntop  15342  limcimolemlt  15407  cnplimclemr  15412  limccnp2lem  15419  limccnp2cntop  15420  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvcnp2cntop  15442  dvcn  15443  dvaddxxbr  15444  dvmulxxbr  15445  dvef  15470  lgseisenlem3  15820  lgseisenlem4  15821  iedgedgg  15931  upgrex  15973  upgr1eopdc  15993  upgr1een  15994  umgr1een  15995  usgredg3  16084  uspgr1eopdc  16113  usgr1eop  16115  vtxdfifiun  16167  1loopgruspgr  16173  1loopgrvd2fi  16175  1loopgrvd0fi  16176  1hevtxdg0fi  16177  1hevtxdg1en  16178  1hegrvtxdg1fi  16179  edginwlkd  16225  wlkres  16249  trlsegvdegfi  16337  eupth2lem3lem1fi  16338  eupth2lem3lem2fi  16339  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343