Theorem xnegeqd 42074

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

Syntax hints:   → wi 4   = wceq 1538  -_𝑒cxne 12492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-neg 10862  df-xneg 12495

This theorem is referenced by:  supminfxr  42103  supminfxr2  42108  supminfxrrnmpt  42110  monoord2xrv  42123  liminfvalxr  42425  liminfvalxrmpt  42428  liminfval4  42431  liminfval3  42432  limsupval4  42436  liminfvaluz2  42437  limsupvaluz4  42442  climliminflimsupd  42443  xlimpnfxnegmnf  42456  liminfpnfuz  42458  xlimpnfxnegmnf2  42500  smfliminflem  43461