Theorem bj-rveccvec

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

	Ref	Expression
Assertion	bj-rveccvec	$$⊢V\in \mathrm{ℝVec}\to V\in \mathrm{ℂVec}$$

Proof

Step	Hyp	Ref	Expression
1		bj-rvecsscvec	$$⊢\mathrm{ℝVec}\subseteq \mathrm{ℂVec}$$
2	1	sseli	$$⊢V\in \mathrm{ℝVec}\to V\in \mathrm{ℂVec}$$