Metamath Proof Explorer


Theorem eleqtrd

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004)

Ref Expression
Hypotheses eleqtrd.1 φ A B
eleqtrd.2 φ B = C
Assertion eleqtrd φ A C

Proof

Step Hyp Ref Expression
1 eleqtrd.1 φ A B
2 eleqtrd.2 φ B = C
3 2 eleq2d φ A B A C
4 1 3 mpbid φ A C