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	$$⊢\mathrm{i}=⟨0_{𝑹},1_{𝑹}⟩$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ci	$$class\mathrm{i}$$
1		c0r	$$class{0}_{𝑹}$$
2		c1r	$$class{1}_{𝑹}$$
3	1 2	cop	$$class⟨0_{𝑹},1_{𝑹}⟩$$
4	0 3	wceq	$$wff\mathrm{i}=⟨0_{𝑹},1_{𝑹}⟩$$