Definition df-1 9521

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

Assertion

Ref	Expression
df-1

Detailed syntax breakdown of Definition df-1

Step	Hyp	Ref	Expression
1		c1 9514	. 2
2		c1r 9266	. . 3
3		c0r 9265	. . 3
4	2, 3	cop 4035	. 2
5	1, 4	wceq 1395	1

This definition is referenced by:  ax1cn  9547  axi2m1  9557  ax1ne0  9558  ax1rid  9559  axrrecex  9561