Metamath Proof Explorer

Theorem shsub1

Description: Subspace sum is an upper bound of its arguments. (Contributed by NM, 14-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion shsub1 
|- ( ( A e. SH /\ B e. SH ) -> A C_ ( A +H B ) )

Proof

Step Hyp Ref Expression
1 shsel1 
 |-  ( ( A e. SH /\ B e. SH ) -> ( x e. A -> x e. ( A +H B ) ) )
2 1 ssrdv 
 |-  ( ( A e. SH /\ B e. SH ) -> A C_ ( A +H B ) )