Theorem eleqtrrd 2312

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  3eltr4d  2316  rspc2vd  3207  exmidsssnc  4316  funopsn  5860  tfrexlem  6565  nnsucuniel  6728  erref  6787  en1uniel  7044  fin0  7142  fin0or  7143  pw1if  7535  prarloclemarch2  7734  fzopth  10395  fzoss2  10508  fz1fzo0m1  10528  fzo0addel  10533  fzo0addelr  10534  elfzoext  10537  fzosubel3  10541  elfzomin  10551  elfzonlteqm1  10555  fzoend  10567  fzofzp1  10572  fzofzp1b  10573  peano2fzor  10577  zmodfzo  10709  frecuzrdg0  10775  frecuzrdgsuc  10776  frecuzrdgdomlem  10779  frecuzrdg0t  10784  frecuzrdgsuctlem  10785  seq3f1olemqsum  10875  seqf1oglem2  10882  bcn2  11126  ccats1val2  11328  swrdccat2  11363  pfxccat1  11394  swrdswrd  11397  pfxccatin12  11425  summodclem2a  12067  fisumss  12078  fsumm1  12102  fisumcom2  12124  prodmodclem2a  12262  fprodm1  12284  fprodcom2fi  12312  ennnfonelemex  13165  ctinfomlemom  13178  strslfv3  13258  bassetsnn  13269  gsumpropd2  13606  sgrppropd  13626  mndpropd  13653  imasmnd  13666  grpsubpropd2  13818  imasgrp  13828  subg0  13897  issubg2m  13906  ghmrn  13974  0ghm  13975  resghm2  13978  ghmco  13981  rngpropd  14099  imasrng  14100  srgpcomp  14134  srgpcompp  14135  srgpcomppsc  14136  ringpropd  14182  imasring  14208  qusring2  14210  mulgass3  14229  rhmopp  14321  lringuplu  14341  aprcotr  14431  lmodprop2d  14496  islssmd  14507  2idl0  14660  2idl1  14661  qus2idrng  14673  qus1  14674  qusrhm  14676  znf1o  14799  psrbaglesuppg  14821  psrbagaddclfi  14825  psr0cl  14836  psrnegcl  14838  psr1clfi  14843  mplsubgfilemm  14853  lmtopcnp  15115  txopn  15130  blpnfctr  15304  metcnpi  15380  metcnpi2  15381  cncfmpt2fcntop  15464  limcimolemlt  15529  cnplimclemr  15534  limccnp2lem  15541  limccnp2cntop  15542  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvcnp2cntop  15564  dvcn  15565  dvaddxxbr  15566  dvmulxxbr  15567  dvef  15592  lgseisenlem3  15945  lgseisenlem4  15946  iedgedgg  16056  upgrex  16098  upgr1eopdc  16118  upgr1een  16119  umgr1een  16120  usgredg3  16209  uspgr1eopdc  16238  usgr1eop  16240  vtxdfifiun  16292  1loopgruspgr  16298  1loopgrvd2fi  16300  1loopgrvd0fi  16301  1hevtxdg0fi  16302  1hevtxdg1en  16303  1hegrvtxdg1fi  16304  edginwlkd  16350  wlkres  16374  trlsegvdegfi  16462  eupth2lem3lem1fi  16463  eupth2lem3lem2fi  16464  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468