Metamath Proof Explorer


Theorem negs11

Description: Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion negs11 A No B No + s A = + s B A = B

Proof

Step Hyp Ref Expression
1 fveq2 + s A = + s B + s + s A = + s + s B
2 negnegs A No + s + s A = A
3 negnegs B No + s + s B = B
4 2 3 eqeqan12d A No B No + s + s A = + s + s B A = B
5 1 4 imbitrid A No B No + s A = + s B A = B
6 fveq2 A = B + s A = + s B
7 5 6 impbid1 A No B No + s A = + s B A = B