Theorem eleqtrd 2167

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eleqtrd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eleqtrd	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	eleq2d 2158	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
4	1, 3	mpbid 146	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1290   ∈ wcel 1439

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 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085

This theorem is referenced by:  eleqtrrd  2168  3eltr3d  2171  syl5eleq  2177  syl6eleq  2181  opth1  4072  0nelop  4084  tfisi  4415  ercl  6317  erth  6350  ecelqsdm  6376  phpm  6635  lincmb01cmp  9481  fzopth  9536  fzoaddel2  9665  fzosubel2  9667  fzocatel  9671  zpnn0elfzo1  9680  fzoend  9694  peano2fzor  9704  monoord2  9966  isermono  9967  bcpasc  10235  zfz1isolemiso  10305  fisum0diag2  10902  isumsplit  10946