Theorem xnegeq 13337

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.)

Assertion

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

Proof of Theorem xnegeq

Step	Hyp	Ref	Expression
1		eqeq1 2764	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = +∞ ↔ 𝐵 = +∞))
2		eqeq1 2764	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 = -∞ ↔ 𝐵 = -∞))
3		negeq 11549	. . . 4 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
4	2, 3	ifbieq2d 4508	. . 3 ⊢ (𝐴 = 𝐵 → if(𝐴 = -∞, +∞, -𝐴) = if(𝐵 = -∞, +∞, -𝐵))
5	1, 4	ifbieq2d 4508	. 2 ⊢ (𝐴 = 𝐵 → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵)))
6		df-xneg 13241	. 2 ⊢ -e𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
7		df-xneg 13241	. 2 ⊢ -e𝐵 = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵))
8	5, 6, 7	3eqtr4g 2820	1 ⊢ (𝐴 = 𝐵 → -e𝐴 = -e𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ifcif 4481  +∞cpnf 11340  -∞cmnf 11341   -cneg 11542   -_ecxne 13238

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-neg 11544  df-xneg 13241

This theorem is used by:  xnegcl  13343  xnegneg  13344  xneg11  13345  xltnegi  13346  xnegid  13368  xnegdi  13378  xsubge0  13391  xlesubadd  13393  xmulneg1  13399  xmulneg2  13400  xmulmnf1  13406  xmulm1  13411  xrsdsval  21717  xrsdsreclblem  21719  xblss2ps  24720  xblss2  24721  xrhmeo  25267  xaddeq0  33345  xrsmulgzz  33570  xrge0npcan  33581  carsgclctunlem2  34951  xnegeqd  46447  xnegeqi  46450  supminfxr2  46479  supminfxrrnmpt  46481  liminflbuz2  46825