Theorem renegeu

Description: Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023)

	Ref	Expression
Assertion	renegeu	$$⊢A\in ℝ\to \exists !x\in ℝA+x=0$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\in ℝ\to A\in ℝ$$
2		ax-rnegex	$$⊢A\in ℝ\to \exists x\in ℝA+x=0$$
3	1 2	renegeulem	$$⊢A\in ℝ\to \exists !x\in ℝA+x=0$$