Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Some deductions from the field axioms for complex numbers
1ex
Next ⟩
cnre
Metamath Proof Explorer
Unicode
Structured
Theorem
1ex
Description:
One is a set.
(Contributed by
David A. Wheeler
, 7-Jul-2016)
Ref
Expression
Assertion
1ex
|- 1 e. _V
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
|- 1 e. CC
2
1
elexi
|- 1 e. _V