This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ S ∧ X ∈ U → X ∈ V

Proof

Step Hyp Ref Expression
1 lssss.v ⊢ V = Base W
2 lssss.s ⊢ S = LSubSp ⁡ W
3 1 2 lssss ⊢ U ∈ S → U ⊆ V
4 3 sselda ⊢ U ∈ S ∧ X ∈ U → X ∈ V