Theorem renegeu

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

	Ref	Expression
Assertion	renegeu	⊢ ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
2		ax-rnegex	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )
3	1 2	renegeulem	⊢ ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )