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