Theorem xnegeqd 45440

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 13174	. 2 ⊢ (𝐴 = 𝐵 → -𝑒𝐴 = -𝑒𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → -𝑒𝐴 = -𝑒𝐵)

Syntax hints:   → wi 4   = wceq 1540  -_𝑒cxne 13076

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-neg 11415  df-xneg 13079

This theorem is referenced by:  supminfxr  45467  supminfxr2  45472  supminfxrrnmpt  45474  monoord2xrv  45486  liminfvalxr  45788  liminfvalxrmpt  45791  liminfval4  45794  liminfval3  45795  limsupval4  45799  liminfvaluz2  45800  limsupvaluz4  45805  climliminflimsupd  45806  xlimpnfxnegmnf  45819  liminfpnfuz  45821  xlimpnfxnegmnf2  45863  smfliminflem  46835