Theorem xnegeq

Description: Equality of two extended numbers with -e in front of them. (Contributed by FL, 26-Dec-2011) (Proof shortened by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xnegeq	$$⊢A=B\to -A=-B$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢A=B\to \left(A=\mathrm{+\infty }\leftrightarrow B=\mathrm{+\infty }\right)$$
2		eqeq1	$$⊢A=B\to \left(A=\mathrm{-\infty }\leftrightarrow B=\mathrm{-\infty }\right)$$
3		negeq	$$⊢A=B\to -A=-B$$
4	2 3	ifbieq2d	$$⊢A=B\to if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)=if\left(B=\mathrm{-\infty },\mathrm{+\infty },-B\right)$$
5	1 4	ifbieq2d	$$⊢A=B\to if\left(A=\mathrm{+\infty },\mathrm{-\infty },if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)\right)=if\left(B=\mathrm{+\infty },\mathrm{-\infty },if\left(B=\mathrm{-\infty },\mathrm{+\infty },-B\right)\right)$$
6		df-xneg	$$⊢-A=if\left(A=\mathrm{+\infty },\mathrm{-\infty },if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)\right)$$
7		df-xneg	$$⊢-B=if\left(B=\mathrm{+\infty },\mathrm{-\infty },if\left(B=\mathrm{-\infty },\mathrm{+\infty },-B\right)\right)$$
8	5 6 7	3eqtr4g	$$⊢A=B\to -A=-B$$