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\in ℝ\to \exists x\in ℝA+x=0$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cr	$$classℝ$$
2	0 1	wcel	$$wffA\in ℝ$$
3		vx	$$setvarx$$
4		caddc	$$class+$$
5	3	cv	$$setvarx$$
6	0 5 4	co	$$class\left(A+x\right)$$
7		cc0	$$class0$$
8	6 7	wceq	$$wffA+x=0$$
9	8 3 1	wrex	$$wff\exists x\in ℝA+x=0$$
10	2 9	wi	$$wff\left(A\in ℝ\to \exists x\in ℝA+x=0\right)$$