Metamath Proof Explorer


Theorem sseqtrrd

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004)

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

Proof

Step Hyp Ref Expression
1 sseqtrrd.1 φ A B
2 sseqtrrd.2 φ C = B
3 2 eqcomd φ B = C
4 1 3 sseqtrd φ A C