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	⊢ ℝ-Vec = {𝑥 ∈ LVec ∣ (Scalar‘𝑥) = ℝfld}

Detailed syntax breakdown of Definition df-bj-rrvec

Step	Hyp	Ref	Expression
1		crrvec 33148	. 2 class ℝ-Vec
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1482	. . . . 5 class 𝑥
4		csca 15944	. . . . 5 class Scalar
5	3, 4	cfv 5888	. . . 4 class (Scalar‘𝑥)
6		crefld 19950	. . . 4 class ℝfld
7	5, 6	wceq 1483	. . 3 wff (Scalar‘𝑥) = ℝfld
8		clvec 19102	. . 3 class LVec
9	7, 2, 8	crab 2916	. 2 class {𝑥 ∈ LVec ∣ (Scalar‘𝑥) = ℝfld}
10	1, 9	wceq 1483	1 wff ℝ-Vec = {𝑥 ∈ LVec ∣ (Scalar‘𝑥) = ℝfld}

This definition is referenced by:  bj-rrvecssvec  33150