Metamath Proof Explorer


Theorem eleqtrrd

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

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

Proof

Step Hyp Ref Expression
1 eleqtrrd.1 φAB
2 eleqtrrd.2 φC=B
3 2 eqcomd φB=C
4 1 3 eleqtrd φAC