Theorem xnegeqd 41717

Description: Equality of two extended numbers with -_𝑒 in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.)

Hypothesis

Ref	Expression
xnegeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
xnegeqd	⊢ (𝜑 → -𝑒𝐴 = -𝑒𝐵)

Proof of Theorem xnegeqd

Step	Hyp	Ref	Expression
1		xnegeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		xnegeq 12603	. 2 ⊢ (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → -𝑒𝐴 = -𝑒𝐵)

Syntax hints:   → wi 4   = wceq 1536  -_𝑒cxne 12507

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-iota 6317  df-fv 6366  df-ov 7162  df-neg 10876  df-xneg 12510

This theorem is referenced by:  supminfxr  41746  supminfxr2  41751  supminfxrrnmpt  41753  monoord2xrv  41766  liminfvalxr  42070  liminfvalxrmpt  42073  liminfval4  42076  liminfval3  42077  limsupval4  42081  liminfvaluz2  42082  limsupvaluz4  42087  climliminflimsupd  42088  xlimpnfxnegmnf  42101  liminfpnfuz  42103  xlimpnfxnegmnf2  42145  smfliminflem  43111