HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-c 5212
Description: Define the set of complex numbers. The 25 axioms for complex numbers start at axcnex 5239.
Assertion
Ref Expression
df-c |- CC = (R. X. R.)
Detailed syntax breakdown of Definition df-c
StepHypRef Expression
1 cc 5204 . 2 class CC
2 cnr 4965 . . 3 class R.
32, 2cxp 3158 . 2 class (R. X. R.)
41, 3wceq 953 1 wff CC = (R. X. R.)
Colors of variables: wff set class
This definition is referenced by:  opelcn 5220  0ncn 5223  addcnsr 5225  mulcnsr 5226  dfcnqs 5234  axaddopr 5237  axmulopr 5238  axcnex 5239  axresscn 5240  ax0id 5253  ax1id 5254  axcnre 5258
Copyright terms: Public domain