Theorem xnegeq 13174

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

Assertion

Ref	Expression
xnegeq	⊢ (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)

Proof of Theorem xnegeq

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4491  +∞cpnf 11212  -∞cmnf 11213  -cneg 11413  -_𝑒cxne 13076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-neg 11415  df-xneg 13079

This theorem is referenced by:  xnegcl  13180  xnegneg  13181  xneg11  13182  xltnegi  13183  xnegid  13205  xnegdi  13215  xsubge0  13228  xlesubadd  13230  xmulneg1  13236  xmulneg2  13237  xmulmnf1  13243  xmulm1  13248  xrsdsval  21334  xrsdsreclblem  21336  xblss2ps  24296  xblss2  24297  xrhmeo  24851  xaddeq0  32683  xrsmulgzz  32954  xrge0npcan  32968  carsgclctunlem2  34317  xnegeqd  45440  xnegeqi  45443  supminfxr2  45472  supminfxrrnmpt  45474  liminflbuz2  45820