Theorem eleqtrrd 2285

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  3eltr4d  2289  rspc2vd  3162  exmidsssnc  4247  funopsn  5762  tfrexlem  6420  nnsucuniel  6581  erref  6640  en1uniel  6896  fin0  6982  fin0or  6983  prarloclemarch2  7532  fzopth  10183  fzoss2  10296  fzo0addel  10317  fzo0addelr  10318  elfzoext  10321  fzosubel3  10325  elfzomin  10335  elfzonlteqm1  10339  fzoend  10351  fzofzp1  10356  fzofzp1b  10357  peano2fzor  10361  zmodfzo  10492  frecuzrdg0  10558  frecuzrdgsuc  10559  frecuzrdgdomlem  10562  frecuzrdg0t  10567  frecuzrdgsuctlem  10568  seq3f1olemqsum  10658  seqf1oglem2  10665  bcn2  10909  ccats1val2  11092  swrdccat2  11124  summodclem2a  11692  fisumss  11703  fsumm1  11727  fisumcom2  11749  prodmodclem2a  11887  fprodm1  11909  fprodcom2fi  11937  ennnfonelemex  12785  ctinfomlemom  12798  strslfv3  12878  gsumpropd2  13225  sgrppropd  13245  mndpropd  13272  imasmnd  13285  grpsubpropd2  13437  imasgrp  13447  subg0  13516  issubg2m  13525  ghmrn  13593  0ghm  13594  resghm2  13597  ghmco  13600  rngpropd  13717  imasrng  13718  srgpcomp  13752  srgpcompp  13753  srgpcomppsc  13754  ringpropd  13800  imasring  13826  qusring2  13828  mulgass3  13847  rhmopp  13938  lringuplu  13958  aprcotr  14047  lmodprop2d  14110  islssmd  14121  2idl0  14274  2idl1  14275  qus2idrng  14287  qus1  14288  qusrhm  14290  znf1o  14413  psrbaglesuppg  14434  psr0cl  14443  psrnegcl  14445  psr1clfi  14450  mplsubgfilemm  14460  lmtopcnp  14722  txopn  14737  blpnfctr  14911  metcnpi  14987  metcnpi2  14988  cncfmpt2fcntop  15071  limcimolemlt  15136  cnplimclemr  15141  limccnp2lem  15148  limccnp2cntop  15149  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvcnp2cntop  15171  dvcn  15172  dvaddxxbr  15173  dvmulxxbr  15174  dvef  15199  lgseisenlem3  15549  lgseisenlem4  15550