Axiom ax-1cn

Description: 1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn . (Contributed by NM, 1-Mar-1995)

	Ref	Expression
Assertion	ax-1cn	$$⊢1\in ℂ$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1	$$class1$$
1		cc	$$classℂ$$
2	0 1	wcel	$$wff1\in ℂ$$