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

Metamath Proof Explorer

Theorem eqimss2

Description: Equality implies inclusion. (Contributed by NM, 23-Nov-2003)

Ref Expression
Assertion eqimss2 
|- ( B = A -> A C_ B )

Proof

Step Hyp Ref Expression
1 eqimss 
 |-  ( A = B -> A C_ B )
2 1 eqcoms 
 |-  ( B = A -> A C_ B )