Definition df-rr3 41984

Description: Define the set of all points RR3. We define each point 𝐴 as a function to allow the use of vector addition and subtraction as well as scalar multiplication in our proofs. (Contributed by Andrew Salmon, 15-Jul-2012.)

Assertion

Ref	Expression
df-rr3	⊢ RR3 = (ℝ ↑m {1, 2, 3})

Detailed syntax breakdown of Definition df-rr3

Step	Hyp	Ref	Expression
1		crr3c 41968	. 2 class RR3
2		cr 10801	. . 3 class ℝ
3		c1 10803	. . . 4 class 1
4		c2 11958	. . . 4 class 2
5		c3 11959	. . . 4 class 3
6	3, 4, 5	ctp 4562	. . 3 class {1, 2, 3}
7		cmap 8573	. . 3 class ↑m
8	2, 6, 7	co 7255	. 2 class (ℝ ↑m {1, 2, 3})
9	1, 8	wceq 1539	1 wff RR3 = (ℝ ↑m {1, 2, 3})

This definition is referenced by: (None)