Theorem eleqtrrd 2318

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 2244	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eleqtrd 2317	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced by:  3eltr4d  2322  rspc2vd  3216  exmidsssnc  4335  funopsn  5882  tfrexlem  6595  nnsucuniel  6758  erref  6817  en1uniel  7081  fin0  7179  fin0or  7180  pw1if  7574  prarloclemarch2  7776  fzopth  10445  fzoss2  10559  fz1fzo0m1  10579  fzo0addel  10584  fzo0addelr  10585  elfzoext  10588  fzosubel3  10592  elfzomin  10602  elfzonlteqm1  10606  fzoend  10618  fzofzp1  10623  fzofzp1b  10624  peano2fzor  10628  zmodfzo  10762  frecuzrdg0  10828  frecuzrdgsuc  10829  frecuzrdgdomlem  10832  frecuzrdg0t  10837  frecuzrdgsuctlem  10838  seq3f1olemqsum  10928  seqf1oglem2  10935  bcn2  11180  ccats1val2  11386  swrdccat2  11421  pfxccat1  11452  swrdswrd  11455  pfxccatin12  11483  summodclem2a  12126  fisumss  12137  fsumm1  12161  fisumcom2  12183  prodmodclem2a  12321  fprodm1  12343  fprodcom2fi  12371  ballotfilemrv  13241  ennnfonelemex  13283  ctinfomlemom  13296  strslfv3  13376  bassetsnn  13387  sgrppropd  13705  mndpropd  13730  imasmnd  13737  grpsubpropd2  13887  imasgrp  13891  subg0  13960  issubg2m  13969  ghmrn  14037  0ghm  14038  resghm2  14041  ghmco  14044  rngpropd  14229  imasrng  14230  srgpcomp  14268  srgpcompp  14269  srgpcomppsc  14270  ringpropd  14316  imasring  14342  qusring2  14344  mulgass3  14364  rhmopp  14456  lringuplu  14476  aprcotr  14570  lmodprop2d  14657  islssmd  14668  2idl0  14821  2idl1  14822  qus2idrng  14834  qus1  14835  qusrhm  14837  znf1o  14958  psrbaglesuppg  14980  psrbagaddclfi  14984  psr0cl  14995  psrnegcl  14997  psr1clfi  15002  mplsubgfilemm  15012  lmtopcnp  15274  txopn  15289  blpnfctr  15463  metcnpi  15539  metcnpi2  15540  cncfmpt2fcntop  15623  limcimolemlt  15688  cnplimclemr  15693  limccnp2lem  15700  limccnp2cntop  15701  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvcnp2cntop  15723  dvcn  15724  dvaddxxbr  15725  dvmulxxbr  15726  dvef  15751  lgseisenlem3  16105  lgseisenlem4  16106  iedgedgg  16216  upgrex  16258  upgr1eopdc  16278  upgr1een  16279  umgr1een  16280  usgredg3  16369  uspgr1eopdc  16398  usgr1eop  16400  vtxdfifiun  16452  1loopgruspgr  16458  1loopgrvd2fi  16460  1loopgrvd0fi  16461  1hevtxdg0fi  16462  1hevtxdg1en  16463  1hegrvtxdg1fi  16464  edginwlkd  16510  wlkres  16534  trlsegvdegfi  16622  eupth2lem3lem1fi  16623  eupth2lem3lem2fi  16624  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628