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={\mathrm{Base}}_W$$
	lssss.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
Assertion	lssel	$$⊢\left(U\in S\wedge X\in U\right)\to X\in V$$

Proof

Step	Hyp	Ref	Expression
1		lssss.v	$$⊢V={\mathrm{Base}}_W$$
2		lssss.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3	1 2	lssss	$$⊢U\in S\to U\subseteq V$$
4	3	sselda	$$⊢\left(U\in S\wedge X\in U\right)\to X\in V$$