HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-1 8069
Description: Define the complex number 1.
Assertion
Ref Expression
df-1

Detailed syntax breakdown of Definition df-1
StepHypRef Expression
1 c1 8062 . 2
2 c1r 7815 . . 3
3 c0r 7814 . . 3
42, 3cop 3271 . 2
51, 4wceq 1531 1
Colors of variables: wff set class
This definition is referenced by:  ax1cn  8095  axi2m1  8105  ax1ne0  8106  ax1rid  8107  axrrecex  8109
Copyright terms: Public domain