Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Real subtraction
renegeu
Next ⟩
rernegcl
Metamath Proof Explorer
Ascii
Unicode
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