Theorem elspansn3

Description: A member of the span of the singleton of a vector is a member of a subspace containing the vector. (Contributed by NM, 16-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	elspansn3	|- ( ( A e. SH /\ B e. A /\ C e. ( span ` { B } ) ) -> C e. A )

Proof

Step	Hyp	Ref	Expression
1		spansnss	|- ( ( A e. SH /\ B e. A ) -> ( span ` { B } ) C_ A )
2	1	sseld	|- ( ( A e. SH /\ B e. A ) -> ( C e. ( span ` { B } ) -> C e. A ) )
3	2	3impia	|- ( ( A e. SH /\ B e. A /\ C e. ( span ` { B } ) ) -> C e. A )