Metamath Proof Explorer


Theorem renegeu

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

Ref Expression
Assertion renegeu A ∃! x A + x = 0

Proof

Step Hyp Ref Expression
1 id A A
2 ax-rnegex A x A + x = 0
3 1 2 renegeulem A ∃! x A + x = 0