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
Ascii
Structured
Theorem
1ex
Description:
One is a set.
(Contributed by
David A. Wheeler
, 7-Jul-2016)
Ref
Expression
Assertion
1ex
⊢
1 ∈ V
Proof
Step
Hyp
Ref
Expression
1
ax-1cn
⊢
1 ∈ ℂ
2
1
elexi
⊢
1 ∈ V