Metamath Proof Explorer


Theorem shle0

Description: No subspace is smaller than the zero subspace. (Contributed by NM, 24-Nov-2004) (New usage is discouraged.)

Ref Expression
Assertion shle0
|- ( A e. SH -> ( A C_ 0H <-> A = 0H ) )

Proof

Step Hyp Ref Expression
1 sh0le
 |-  ( A e. SH -> 0H C_ A )
2 1 biantrud
 |-  ( A e. SH -> ( A C_ 0H <-> ( A C_ 0H /\ 0H C_ A ) ) )
3 eqss
 |-  ( A = 0H <-> ( A C_ 0H /\ 0H C_ A ) )
4 2 3 bitr4di
 |-  ( A e. SH -> ( A C_ 0H <-> A = 0H ) )