Theorem xnegeq 13223

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 2739	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = +∞ ↔ 𝐵 = +∞))
2		eqeq1 2739	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 = -∞ ↔ 𝐵 = -∞))
3		negeq 11474	. . . 4 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)
4	2, 3	ifbieq2d 4527	. . 3 ⊢ (𝐴 = 𝐵 → if(𝐴 = -∞, +∞, -𝐴) = if(𝐵 = -∞, +∞, -𝐵))
5	1, 4	ifbieq2d 4527	. 2 ⊢ (𝐴 = 𝐵 → if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴)) = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵)))
6		df-xneg 13128	. 2 ⊢ -𝑒𝐴 = if(𝐴 = +∞, -∞, if(𝐴 = -∞, +∞, -𝐴))
7		df-xneg 13128	. 2 ⊢ -𝑒𝐵 = if(𝐵 = +∞, -∞, if(𝐵 = -∞, +∞, -𝐵))
8	5, 6, 7	3eqtr4g 2795	1 ⊢ (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)

Syntax hints:   → wi 4   = wceq 1540  ifcif 4500  +∞cpnf 11266  -∞cmnf 11267  -cneg 11467  -_𝑒cxne 13125

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-neg 11469  df-xneg 13128

This theorem is referenced by:  xnegcl  13229  xnegneg  13230  xneg11  13231  xltnegi  13232  xnegid  13254  xnegdi  13264  xsubge0  13277  xlesubadd  13279  xmulneg1  13285  xmulneg2  13286  xmulmnf1  13292  xmulm1  13297  xrsdsval  21378  xrsdsreclblem  21380  xblss2ps  24340  xblss2  24341  xrhmeo  24895  xaddeq0  32730  xrsmulgzz  33001  xrge0npcan  33015  carsgclctunlem2  34351  xnegeqd  45464  xnegeqi  45467  supminfxr2  45496  supminfxrrnmpt  45498  liminflbuz2  45844