Database
REAL AND COMPLEX NUMBERS
Real and complex numbers - basic operations
Subtraction
negex
Next ⟩
subcl
Metamath Proof Explorer
Ascii
Unicode
Theorem
negex
Description:
A negative is a set.
(Contributed by
NM
, 4-Apr-2005)
Ref
Expression
Assertion
negex
$${\u22a2}-{A}\in \mathrm{V}$$
Proof
Step
Hyp
Ref
Expression
1
df-neg
$${\u22a2}-{A}=0-{A}$$
2
1
ovexi
$${\u22a2}-{A}\in \mathrm{V}$$