Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Some deductions from the field axioms for complex numbers
cnex
Next ⟩
addcl
Metamath Proof Explorer
Ascii
Unicode
Theorem
cnex
Description:
Alias for
ax-cnex
. See also
cnexALT
.
(Contributed by
Mario Carneiro
, 17-Nov-2014)
Ref
Expression
Assertion
cnex
⊢
ℂ
∈
V
Proof
Step
Hyp
Ref
Expression
1
ax-cnex
⊢
ℂ
∈
V