Metamath Proof Explorer


Definition df-subs

Description: Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Assertion df-subs - s = x No , y No x + s + s y

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubs class - s
1 vx setvar x
2 csur class No
3 vy setvar y
4 1 cv setvar x
5 cadds class + s
6 cnegs class + s
7 3 cv setvar y
8 7 6 cfv class + s y
9 4 8 5 co class x + s + s y
10 1 3 2 2 9 cmpo class x No , y No x + s + s y
11 0 10 wceq wff - s = x No , y No x + s + s y