Metamath Proof Explorer

Theorem renegeu

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

Ref Expression
Assertion renegeu 
|- ( A e. RR -> E! x e. RR ( A + x ) = 0 )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. RR -> A e. RR )
2 ax-rnegex 
 |-  ( A e. RR -> E. x e. RR ( A + x ) = 0 )
3 1 2 renegeulem 
 |-  ( A e. RR -> E! x e. RR ( A + x ) = 0 )