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 e. SH -> 0H C_ A )

Proof

Step Hyp Ref Expression
1 df-ch0 
 |-  0H = { 0h }
2 sh0 
 |-  ( A e. SH -> 0h e. A )
3 2 snssd 
 |-  ( A e. SH -> { 0h } C_ A )
4 1 3 eqsstrid 
 |-  ( A e. SH -> 0H C_ A )