Theorem eleqtri 2313

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eleqtr.1	⊢ 𝐴 ∈ 𝐵
eleqtr.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eleqtri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eleqtri

Step	Hyp	Ref	Expression
1		eleqtr.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtr.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	eleq2i 2305	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)
4	1, 3	mpbi 145	1 ⊢ 𝐴 ∈ 𝐶

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleqtrri  2314  3eltr3i  2319  prid2  3818  2eluzge0  9984  fz01or  10528  fz0to4untppr  10541  ef0lem  12443  ege2le3  12454  efgt1p2  12478  efgt1p  12479  phi1  13017  ballotfilem2  13277  ballotfilem1ri  13327  cnrehmeocntop  15760  dvcjbr  15858  log2ublem2  16141