Definition df-rr3 40802

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 40786	. 2 class RR3
2		cr 10530	. . 3 class ℝ
3		c1 10532	. . . 4 class 1
4		c2 11686	. . . 4 class 2
5		c3 11687	. . . 4 class 3
6	3, 4, 5	ctp 4565	. . 3 class {1, 2, 3}
7		cmap 8400	. . 3 class ↑m
8	2, 6, 7	co 7150	. 2 class (ℝ ↑m {1, 2, 3})
9	1, 8	wceq 1533	1 wff RR3 = (ℝ ↑m {1, 2, 3})

This definition is referenced by: (None)