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	$$⊢\mathrm{ℂVec}=\mathrm{CMod}\cap \mathrm{LVec}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccvs	$$class\mathrm{ℂVec}$$
1		cclm	$$class\mathrm{CMod}$$
2		clvec	$$class\mathrm{LVec}$$
3	1 2	cin	$$class\left(\mathrm{CMod}\cap \mathrm{LVec}\right)$$
4	0 3	wceq	$$wff\mathrm{ℂVec}=\mathrm{CMod}\cap \mathrm{LVec}$$