Definition df-bj-rrvec 33149

Description: Definition of the class of real vector spaces. (Contributed by BJ, 9-Jun-2019.)

Assertion

Ref	Expression
df-bj-rrvec	|- RR-Vec = { x e. LVec | (Scalar ` x ) = RRfld }

Detailed syntax breakdown of Definition df-bj-rrvec

Step	Hyp	Ref	Expression
1		crrvec 33148	. 2 class RR-Vec
2		vx	. . . . . 6 setvar x
3	2	cv 1482	. . . . 5 class x
4		csca 15944	. . . . 5 class Scalar
5	3, 4	cfv 5888	. . . 4 class (Scalar ` x )
6		crefld 19950	. . . 4 class RRfld
7	5, 6	wceq 1483	. . 3 wff (Scalar ` x ) = RRfld
8		clvec 19102	. . 3 class LVec
9	7, 2, 8	crab 2916	. 2 class { x e. LVec | (Scalar ` x ) = RRfld }
10	1, 9	wceq 1483	1 wff RR-Vec = { x e. LVec | (Scalar ` x ) = RRfld }

This definition is referenced by:  bj-rrvecssvec  33150