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 x ℝVec x LVec
2 1 ssriv ℝVec LVec