Theorem negex

Description: A negative is a set. (Contributed by NM, 4-Apr-2005)

	Ref	Expression
Assertion	negex	$$⊢-A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-neg	$$⊢-A=0-A$$
2	1	ovexi	$$⊢-A\in \mathrm{V}$$