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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1	$$class1$$
1		c1r	$$class{1}_{𝑹}$$
2		c0r	$$class{0}_{𝑹}$$
3	1 2	cop	$$class⟨1_{𝑹},0_{𝑹}⟩$$
4	0 3	wceq	$$wff1=⟨1_{𝑹},0_{𝑹}⟩$$