Theorem eleqtrrd 2179

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

Syntax hints:   → wi 4   = wceq 1299   ∈ wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096

This theorem is referenced by:  3eltr4d  2183  exmidsssnc  4064  tfrexlem  6161  nnsucuniel  6321  erref  6379  en1uniel  6628  fin0  6708  fin0or  6709  prarloclemarch2  7128  fzopth  9682  fzoss2  9790  fzosubel3  9814  elfzomin  9824  elfzonlteqm1  9828  fzoend  9840  fzofzp1  9845  fzofzp1b  9846  peano2fzor  9850  zmodfzo  9961  frecuzrdg0  10027  frecuzrdgsuc  10028  frecuzrdgdomlem  10031  frecuzrdg0t  10036  frecuzrdgsuctlem  10037  seq3f1olemqsum  10114  bcn2  10351  summodclem2a  10989  fisumss  11000  fsumm1  11024  fisumcom2  11046  ennnfonelemex  11719  ctinfomlemom  11732  lmtopcnp  12200  txopn  12215  blpnfctr  12367  metcnpi  12439  metcnpi2  12440  limcimolemlt  12513  dvidlemap  12533