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 e. CC

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1
 |-  1
1 cc
 |-  CC
2 0 1 wcel
 |-  1 e. CC