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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lssss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	lssel	⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lssss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lssss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3	1 2	lssss	⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ 𝑉 )
4	3	sselda	⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑉 )