Axiom ax-icn

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

	Ref	Expression
Assertion	ax-icn	$$⊢\mathrm{i}\in ℂ$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ci	$$class\mathrm{i}$$
1		cc	$$classℂ$$
2	0 1	wcel	$$wff\mathrm{i}\in ℂ$$