Definition df-bj-rrvec 34069

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 34068	. 2 class ℝ-Vec
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1507	. . . . 5 class 𝑥
4		csca 16422	. . . . 5 class Scalar
5	3, 4	cfv 6185	. . . 4 class (Scalar‘𝑥)
6		crefld 20465	. . . 4 class ℝfld
7	5, 6	wceq 1508	. . 3 wff (Scalar‘𝑥) = ℝfld
8		clvec 19608	. . 3 class LVec
9	7, 2, 8	crab 3085	. 2 class {𝑥 ∈ LVec ∣ (Scalar‘𝑥) = ℝfld}
10	1, 9	wceq 1508	1 wff ℝ-Vec = {𝑥 ∈ LVec ∣ (Scalar‘𝑥) = ℝfld}

This definition is referenced by:  bj-rrvecssvec  34070