Metamath Proof Explorer


Theorem eqimss2

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

Ref Expression
Assertion eqimss2 B = A A B

Proof

Step Hyp Ref Expression
1 eqimss A = B A B
2 1 eqcoms B = A A B