Definition df-bj-rrvec 32326

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

Assertion

Ref	Expression
df-bj-rrvec	⊢ ℝ-Vec = {𝑥 ∈ LVec ∣ (Scalar‘𝑥) = ℝfld}

Detailed syntax breakdown of Definition df-bj-rrvec

Step	Hyp	Ref	Expression
1		crrvec 32325	. 2 class ℝ-Vec
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1474	. . . . 5 class 𝑥
4		csca 15771	. . . . 5 class Scalar
5	3, 4	cfv 5804	. . . 4 class (Scalar‘𝑥)
6		crefld 19769	. . . 4 class ℝfld
7	5, 6	wceq 1475	. . 3 wff (Scalar‘𝑥) = ℝfld
8		clvec 18923	. . 3 class LVec
9	7, 2, 8	crab 2900	. 2 class {𝑥 ∈ LVec ∣ (Scalar‘𝑥) = ℝfld}
10	1, 9	wceq 1475	1 wff ℝ-Vec = {𝑥 ∈ LVec ∣ (Scalar‘𝑥) = ℝfld}

This definition is referenced by:  bj-rrvecssvec  32327