Theorem xnegeq 13361

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 2767	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = +∞ ↔ 𝐵 = +∞))
2		eqeq1 2767	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 = -∞ ↔ 𝐵 = -∞))
3		negeq 11573	. . . 4 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
4	2, 3	ifbieq2d 4512	. . 3 ⊢ (𝐴 = 𝐵 → if(𝐴 = -∞, +∞, -𝐴) = if(𝐵 = -∞, +∞, -𝐵))
5	1, 4	ifbieq2d 4512	. 2 ⊢ (𝐴 = 𝐵 → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵)))
6		df-xneg 13265	. 2 ⊢ -e𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
7		df-xneg 13265	. 2 ⊢ -e𝐵 = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵))
8	5, 6, 7	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → -e𝐴 = -e𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4485  +∞cpnf 11364  -∞cmnf 11365   -cneg 11566   -_ecxne 13262

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6509  df-fv 6563  df-ov 7443  df-neg 11568  df-xneg 13265

This theorem is used by:  xnegcl  13367  xnegneg  13368  xneg11  13369  xltnegi  13370  xnegid  13392  xnegdi  13402  xsubge0  13415  xlesubadd  13417  xmulneg1  13423  xmulneg2  13424  xmulmnf1  13430  xmulm1  13435  xrsdsval  21744  xrsdsreclblem  21746  xblss2ps  24747  xblss2  24748  xrhmeo  25294  xaddeq0  33412  xrsmulgzz  33637  xrge0npcan  33648  carsgclctunlem2  35018  xnegeqd  46650  xnegeqi  46653  supminfxr2  46682  supminfxrrnmpt  46684  liminflbuz2  47028