Definition df-subs

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

	Ref	Expression
Assertion	df-subs	$$⊢{-}_s=\left(x\in \mathrm{No},y\in \mathrm{No}⟼x{+}_s{+}_s\left(y\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubs	$$class{-}_s$$
1		vx	$$setvarx$$
2		csur	$$class\mathrm{No}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5		cadds	$$class{+}_s$$
6		cnegs	$$class{+}_s$$
7	3	cv	$$setvary$$
8	7 6	cfv	$$class{+}_s\left(y\right)$$
9	4 8 5	co	$$class\left(x{+}_s{+}_s\left(y\right)\right)$$
10	1 3 2 2 9	cmpo	$$class\left(x\in \mathrm{No},y\in \mathrm{No}⟼x{+}_s{+}_s\left(y\right)\right)$$
11	0 10	wceq	$$wff{-}_s=\left(x\in \mathrm{No},y\in \mathrm{No}⟼x{+}_s{+}_s\left(y\right)\right)$$