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	⊢ ( 𝐴 = 𝐵 → -𝑒 𝐴 = -𝑒 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 = +∞ ↔ 𝐵 = +∞ ) )
2		eqeq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 = -∞ ↔ 𝐵 = -∞ ) )
3		negeq	⊢ ( 𝐴 = 𝐵 → - 𝐴 = - 𝐵 )
4	2 3	ifbieq2d	⊢ ( 𝐴 = 𝐵 → if ( 𝐴 = -∞ , +∞ , - 𝐴 ) = if ( 𝐵 = -∞ , +∞ , - 𝐵 ) )
5	1 4	ifbieq2d	⊢ ( 𝐴 = 𝐵 → if ( 𝐴 = +∞ , -∞ , if ( 𝐴 = -∞ , +∞ , - 𝐴 ) ) = if ( 𝐵 = +∞ , -∞ , if ( 𝐵 = -∞ , +∞ , - 𝐵 ) ) )
6		df-xneg	⊢ -𝑒 𝐴 = if ( 𝐴 = +∞ , -∞ , if ( 𝐴 = -∞ , +∞ , - 𝐴 ) )
7		df-xneg	⊢ -𝑒 𝐵 = if ( 𝐵 = +∞ , -∞ , if ( 𝐵 = -∞ , +∞ , - 𝐵 ) )
8	5 6 7	3eqtr4g	⊢ ( 𝐴 = 𝐵 → -𝑒 𝐴 = -𝑒 𝐵 )