Theorem negex

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

	Ref	Expression
Assertion	negex	|- -u A e. _V

Proof

Step	Hyp	Ref	Expression
1		df-neg	|- -u A = ( 0 - A )
2	1	ovexi	|- -u A e. _V