Theorem spansnss2

Description: The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 16-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spansnss2	|- ( ( A e. SH /\ B e. ~H ) -> ( B e. A <-> ( span ` { B } ) C_ A ) )

Proof

Step	Hyp	Ref	Expression
1		spansnss	|- ( ( A e. SH /\ B e. A ) -> ( span ` { B } ) C_ A )
2	1	ex	|- ( A e. SH -> ( B e. A -> ( span ` { B } ) C_ A ) )
3	2	adantr	|- ( ( A e. SH /\ B e. ~H ) -> ( B e. A -> ( span ` { B } ) C_ A ) )
4		spansnid	|- ( B e. ~H -> B e. ( span ` { B } ) )
5		ssel	|- ( ( span ` { B } ) C_ A -> ( B e. ( span ` { B } ) -> B e. A ) )
6	4 5	syl5com	|- ( B e. ~H -> ( ( span ` { B } ) C_ A -> B e. A ) )
7	6	adantl	|- ( ( A e. SH /\ B e. ~H ) -> ( ( span ` { B } ) C_ A -> B e. A ) )
8	3 7	impbid	|- ( ( A e. SH /\ B e. ~H ) -> ( B e. A <-> ( span ` { B } ) C_ A ) )