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
$${\u22a2}\u2102\in \mathrm{V}$$
Proof
Step
Hyp
Ref
Expression
1
ax-cnex
$${\u22a2}\u2102\in \mathrm{V}$$