Theorem eleqtrrd 2257

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  3eltr4d  2261  rspc2vd  3126  exmidsssnc  4204  tfrexlem  6335  nnsucuniel  6496  erref  6555  en1uniel  6804  fin0  6885  fin0or  6886  prarloclemarch2  7418  fzopth  10061  fzoss2  10172  fzosubel3  10196  elfzomin  10206  elfzonlteqm1  10210  fzoend  10222  fzofzp1  10227  fzofzp1b  10228  peano2fzor  10232  zmodfzo  10347  frecuzrdg0  10413  frecuzrdgsuc  10414  frecuzrdgdomlem  10417  frecuzrdg0t  10422  frecuzrdgsuctlem  10423  seq3f1olemqsum  10500  bcn2  10744  summodclem2a  11389  fisumss  11400  fsumm1  11424  fisumcom2  11446  prodmodclem2a  11584  fprodm1  11606  fprodcom2fi  11634  ennnfonelemex  12415  ctinfomlemom  12428  mndpropd  12841  grpsubpropd2  12975  subg0  13040  issubg2m  13049  srgpcomp  13173  srgpcompp  13174  srgpcomppsc  13175  ringpropd  13217  mulgass3  13254  lringuplu  13337  aprcotr  13375  lmodprop2d  13438  lmtopcnp  13753  txopn  13768  blpnfctr  13942  metcnpi  14018  metcnpi2  14019  cncfmpt2fcntop  14088  limcimolemlt  14136  cnplimclemr  14141  limccnp2lem  14148  limccnp2cntop  14149  dvidlemap  14163  dvcnp2cntop  14166  dvcn  14167  dvaddxxbr  14168  dvmulxxbr  14169  dvef  14191