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

Metamath Proof Explorer

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 ∈ J ∧ E ∈ B → E ∈ V

Proof

Step Hyp Ref Expression
1 lbsss.v ⊢ V = Base W
2 lbsss.j ⊢ J = LBasis ⁡ W
3 1 2 lbsss ⊢ B ∈ J → B ⊆ V
4 3 sselda ⊢ B ∈ J ∧ E ∈ B → E ∈ V