Theorem lbsel

Description: An element of a basis is a vector. (Contributed by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Hypotheses	lbsss.v	|- V = ( Base ` W )
	lbsss.j	|- J = ( LBasis ` W )
Assertion	lbsel	|- ( ( B e. J /\ E e. B ) -> E e. V )

Proof

Step	Hyp	Ref	Expression
1		lbsss.v	|- V = ( Base ` W )
2		lbsss.j	|- J = ( LBasis ` W )
3	1 2	lbsss	|- ( B e. J -> B C_ V )
4	3	sselda	|- ( ( B e. J /\ E e. B ) -> E e. V )