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 | $${\u22a2}1\in \u2102$$ |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | c1 | $${class}1$$ | |
1 | cc | $${class}\u2102$$ | |
2 | 0 1 | wcel | $${wff}1\in \u2102$$ |