This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eleqtri

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

Ref Expression
Hypotheses eleqtri.1 ⊢ A ∈ B
eleqtri.2 ⊢ B = C
Assertion eleqtri ⊢ A ∈ C

Proof

Step Hyp Ref Expression
1 eleqtri.1 ⊢ A ∈ B
2 eleqtri.2 ⊢ B = C
3 2 eleq2i ⊢ A ∈ B ↔ A ∈ C
4 1 3 mpbi ⊢ A ∈ C