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 ( 𝐴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𝐴 )