This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℂ$

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