Theorem sh0le

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

	Ref	Expression
Assertion	sh0le	⊢ ( 𝐴 ∈ Sℋ → 0ℋ ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-ch0	⊢ 0ℋ = { 0ℎ }
2		sh0	⊢ ( 𝐴 ∈ Sℋ → 0ℎ ∈ 𝐴 )
3	2	snssd	⊢ ( 𝐴 ∈ Sℋ → { 0ℎ } ⊆ 𝐴 )
4	1 3	eqsstrid	⊢ ( 𝐴 ∈ Sℋ → 0ℋ ⊆ 𝐴 )