Theorem xneg11

Description: Extended real version of neg11 . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xneg11	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-A=-B\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		xnegeq	$$⊢-A=-B\to -\left(-A\right)=-\left(-B\right)$$
2		xnegneg	$$⊢A\in {ℝ}^{*}\to -\left(-A\right)=A$$
3		xnegneg	$$⊢B\in {ℝ}^{*}\to -\left(-B\right)=B$$
4	2 3	eqeqan12d	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-\left(-A\right)=-\left(-B\right)\leftrightarrow A=B\right)$$
5	1 4	imbitrid	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-A=-B\to A=B\right)$$
6		xnegeq	$$⊢A=B\to -A=-B$$
7	5 6	impbid1	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(-A=-B\leftrightarrow A=B\right)$$