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

Metamath Proof Explorer

Theorem shsub1

Description: Subspace sum is an upper bound of its arguments. (Contributed by NM, 14-Dec-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	shsub1	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to A \subseteq A +_{ℋ} B$

Step	Hyp	Ref	Expression
1		shsel1	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to (x \in A \to x \in (A +_{ℋ} B))$
2	1	ssrdv	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ}) \to A \subseteq A +_{ℋ} B$