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