Theorem negex

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

	Ref	Expression
Assertion	negex	⊢ - 𝐴 ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-neg	⊢ - 𝐴 = ( 0 − 𝐴 )
2	1	ovexi	⊢ - 𝐴 ∈ V