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

Definition df-c 6758
Description: Define the set of complex numbers. The 23 axioms for complex numbers start at axcnex 6785.
Assertion
Ref Expression
df-c |- CC = (R. X. R.)

Detailed syntax breakdown of Definition df-c
StepHypRef Expression
1 cc 6750 . 2 class CC
2 cnr 6511 . . 3 class R.
32, 2cxp 4117 . 2 class (R. X. R.)
41, 3wceq 1586 1 wff CC = (R. X. R.)
Colors of variables: wff set class
This definition is referenced by:  opelcn 6766  0ncn 6769  addcnsr 6771  mulcnsr 6772  dfcnqs 6780  axaddopr 6783  axmulopr 6784  axcnex 6785  axresscn 6786  axcnre 6802
Copyright terms: Public domain