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