Metamath Proof Explorer


Theorem eleqtri

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

Ref Expression
Hypotheses eleqtri.1 AB
eleqtri.2 B=C
Assertion eleqtri AC

Proof

Step Hyp Ref Expression
1 eleqtri.1 AB
2 eleqtri.2 B=C
3 2 eleq2i ABAC
4 1 3 mpbi AC