Description: Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | df-subs |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | csubs | ||
1 | vx | ||
2 | csur | ||
3 | vy | ||
4 | 1 | cv | |
5 | cadds | ||
6 | cnegs | ||
7 | 3 | cv | |
8 | 7 6 | cfv | |
9 | 4 8 5 | co | |
10 | 1 3 2 2 9 | cmpo | |
11 | 0 10 | wceq |