Theorem lbsel

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

	Ref	Expression
Hypotheses	lbsss.v	$$⊢V={\mathrm{Base}}_W$$
	lbsss.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
Assertion	lbsel	$$⊢\left(B\in J\wedge E\in B\right)\to E\in V$$

Proof

Step	Hyp	Ref	Expression
1		lbsss.v	$$⊢V={\mathrm{Base}}_W$$
2		lbsss.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
3	1 2	lbsss	$$⊢B\in J\to B\subseteq V$$
4	3	sselda	$$⊢\left(B\in J\wedge E\in B\right)\to E\in V$$