Metamath Proof Explorer


Axiom ax-rnegex

Description: Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by Theorem axrnegex . (Contributed by Eric Schmidt, 21-May-2007)

Ref Expression
Assertion ax-rnegex A x A + x = 0

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cr class
2 0 1 wcel wff A
3 vx setvar x
4 caddc class +
5 3 cv setvar x
6 0 5 4 co class A + x
7 cc0 class 0
8 6 7 wceq wff A + x = 0
9 8 3 1 wrex wff x A + x = 0
10 2 9 wi wff A x A + x = 0