Definition df-rr3

Description: Define the set of all points RR3 . We define each point A 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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crr3c	⊢ RR3
1		cr	⊢ ℝ
2		cmap	⊢ ↑m
3		c1	⊢ 1
4		c2	⊢ 2
5		c3	⊢ 3
6	3 4 5	ctp	⊢ { 1 , 2 , 3 }
7	1 6 2	co	⊢ ( ℝ ↑m { 1 , 2 , 3 } )
8	0 7	wceq	⊢ RR3 = ( ℝ ↑m { 1 , 2 , 3 } )