Definition df-1

Description: Define the complex number 1. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	df-1	⊢ 1 = ⟨ 1R , 0R ⟩

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1	⊢ 1
1		c1r	⊢ 1R
2		c0r	⊢ 0R
3	1 2	cop	⊢ ⟨ 1R , 0R ⟩
4	0 3	wceq	⊢ 1 = ⟨ 1R , 0R ⟩