This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqimssi

Description: Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007)

Ref Expression
Hypothesis eqimssi.1 
|- A = B
Assertion eqimssi 
|- A C_ B

Proof

Step Hyp Ref Expression
1 eqimssi.1 
 |-  A = B
2 ssid 
 |-  A C_ A
3 2 1 sseqtri 
 |-  A C_ B