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

Definition df-1 7265
Description: Define the complex number 1 (base 10).
Assertion
Ref Expression
df-1

Detailed syntax breakdown of Definition df-1
StepHypRef Expression
1 c1 7258 . 2
2 c1r 7009 . . 3
3 c0r 7008 . . 3
42, 3cop 3089 . 2
51, 4wceq 1414 1
Colors of variables: wff set class
This definition is referenced by:  ax1cn 7290  axi2m1 7300  ax1ne0 7301  ax1rid 7302  axrrecex 7304
Copyright terms: Public domain