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

Metamath Proof Explorer

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 i ∈ ℂ

Detailed syntax breakdown

Step Hyp Ref Expression
0 ci ⊢ i
1 cc ⊢ ℂ
2 0 1 wcel ⊢ i ∈ ℂ