Theorem bj-rveccvec

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

	Ref	Expression
Assertion	bj-rveccvec	⊢ ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂVec )

Proof

Step	Hyp	Ref	Expression
1		bj-rvecsscvec	⊢ ℝ-Vec ⊆ ℂVec
2	1	sseli	⊢ ( 𝑉 ∈ ℝ-Vec → 𝑉 ∈ ℂVec )