Definition df-cvs 25157

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.)

Assertion

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

Detailed syntax breakdown of Definition df-cvs

Step	Hyp	Ref	Expression
1		ccvs 25156	. 2 class ℂVec
2		cclm 25095	. . 3 class ℂMod
3		clvec 21101	. . 3 class LVec
4	2, 3	cin 3950	. 2 class (ℂMod ∩ LVec)
5	1, 4	wceq 1540	1 wff ℂVec = (ℂMod ∩ LVec)

This definition is referenced by:  cvslvec  25158  cvsclm  25159  iscvs  25160  cvsi  25163  cnstrcvs  25174  cncvs  25178  recvs  25179  recvsOLD  25180  qcvs  25181  zclmncvs  25182  bj-rvecsscvec  37305