Theorem xnegeq 13338

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 2765	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = +∞ ↔ 𝐵 = +∞))
2		eqeq1 2765	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 = -∞ ↔ 𝐵 = -∞))
3		negeq 11550	. . . 4 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
4	2, 3	ifbieq2d 4509	. . 3 ⊢ (𝐴 = 𝐵 → if(𝐴 = -∞, +∞, -𝐴) = if(𝐵 = -∞, +∞, -𝐵))
5	1, 4	ifbieq2d 4509	. 2 ⊢ (𝐴 = 𝐵 → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵)))
6		df-xneg 13242	. 2 ⊢ -e𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
7		df-xneg 13242	. 2 ⊢ -e𝐵 = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵))
8	5, 6, 7	3eqtr4g 2821	1 ⊢ (𝐴 = 𝐵 → -e𝐴 = -e𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4482  +∞cpnf 11341  -∞cmnf 11342   -cneg 11543   -_ecxne 13239

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3900  df-un 3902  df-ss 3915  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6495  df-fv 6547  df-ov 7424  df-neg 11545  df-xneg 13242

This theorem is used by:  xnegcl  13344  xnegneg  13345  xneg11  13346  xltnegi  13347  xnegid  13369  xnegdi  13379  xsubge0  13392  xlesubadd  13394  xmulneg1  13400  xmulneg2  13401  xmulmnf1  13407  xmulm1  13412  xrsdsval  21718  xrsdsreclblem  21720  xblss2ps  24721  xblss2  24722  xrhmeo  25268  xaddeq0  33346  xrsmulgzz  33571  xrge0npcan  33582  carsgclctunlem2  34952  xnegeqd  46448  xnegeqi  46451  supminfxr2  46480  supminfxrrnmpt  46482  liminflbuz2  46826