Metamath Proof Explorer


Theorem bj-rvecssvec

Description: Real vector spaces are vector spaces. (Contributed by BJ, 6-Jan-2024)

Ref Expression
Assertion bj-rvecssvec ℝ-Vec ⊆ LVec

Proof

Step Hyp Ref Expression
1 bj-rvecvec ( 𝑥 ∈ ℝ-Vec → 𝑥 ∈ LVec )
2 1 ssriv ℝ-Vec ⊆ LVec