Definition df-i

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

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

Detailed syntax breakdown

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