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 \to A \subseteq B$

Step	Hyp	Ref	Expression
1		eqimss	$⊢ A = B \to A \subseteq B$
2	1	eqcoms	$⊢ B = A \to A \subseteq B$