Definition df-cvs

Description: Define the class of subcomplex vector spaces, which are the subcomplex modules which are also vector spaces. (Contributed by Thierry Arnoux, 22-May-2019)

	Ref	Expression
Assertion	df-cvs	⊢ ℂVec = ( ℂMod ∩ LVec )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccvs	⊢ ℂVec
1		cclm	⊢ ℂMod
2		clvec	⊢ LVec
3	1 2	cin	⊢ ( ℂMod ∩ LVec )
4	0 3	wceq	⊢ ℂVec = ( ℂMod ∩ LVec )