Theorem lssel

Description: A subspace member is a vector. (Contributed by NM, 11-Jan-2014) (Revised by Mario Carneiro, 8-Jan-2015)

	Ref	Expression
Hypotheses	lssss.v	|- V = ( Base ` W )
	lssss.s	|- S = ( LSubSp ` W )
Assertion	lssel	|- ( ( U e. S /\ X e. U ) -> X e. V )

Proof

Step	Hyp	Ref	Expression
1		lssss.v	|- V = ( Base ` W )
2		lssss.s	|- S = ( LSubSp ` W )
3	1 2	lssss	|- ( U e. S -> U C_ V )
4	3	sselda	|- ( ( U e. S /\ X e. U ) -> X e. V )