Definition df-c 4034

Description: Define the set of complex numbers.

Assertion

Ref	Expression
df-c	⊢ ℂ = (R × R)

Detailed syntax breakdown of Definition df-c

Step	Hyp	Ref	Expression
1		cc 4026	. 2 class ℂ
2		cnr 3787	. . 3 class R
3	2, 2	cxp 2408	. 2 class (R × R)
4	1, 3	wceq 1091	1 wff ℂ = (R × *)

This definition is referenced by:  opelcn 4042  0ncn 4045  addcnsr 4047  mulcnsr 4048  dfcnqs 4056  axaddex 4059  axmulex 4060  axcnex 4061  axresscn 4062  axaddcl 4066  axmulcl 4068  ax0id 4076  ax1id 4077  axnegex 4078  axrecex 4079  axcnre 4087

metamath.org