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

Metamath Proof Explorer

Theorem sh0le

Description: The zero subspace is the smallest subspace. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	sh0le	$⊢ A \in S_{ℋ} \to 0_{ℋ} \subseteq A$

Step	Hyp	Ref	Expression
1		df-ch0	$⊢ 0_{ℋ} = \{0_{ℎ}\}$
2		sh0	$⊢ A \in S_{ℋ} \to 0_{ℎ} \in A$
3	2	snssd	$⊢ A \in S_{ℋ} \to \{0_{ℎ}\} \subseteq A$
4	1 3	eqsstrid	$⊢ A \in S_{ℋ} \to 0_{ℋ} \subseteq A$