Metamath Proof Explorer


Theorem eleqtrri

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

Ref Expression
Hypotheses eleqtrri.1 𝐴𝐵
eleqtrri.2 𝐶 = 𝐵
Assertion eleqtrri 𝐴𝐶

Proof

Step Hyp Ref Expression
1 eleqtrri.1 𝐴𝐵
2 eleqtrri.2 𝐶 = 𝐵
3 2 eqcomi 𝐵 = 𝐶
4 1 3 eleqtri 𝐴𝐶