Definition df-subs

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

	Ref	Expression
Assertion	df-subs	Could not format assertion : No typesetting found for |- -s = ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubs	Could not format -s : No typesetting found for class -s with typecode class
1		vx	$$setvarx$$
2		csur	$$class\mathrm{No}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5		cadds	Could not format +s : No typesetting found for class +s with typecode class
6		cnegs	Could not format -us : No typesetting found for class -us with typecode class
7	3	cv	$$setvary$$
8	7 6	cfv	Could not format ( -us ` y ) : No typesetting found for class ( -us ` y ) with typecode class
9	4 8 5	co	Could not format ( x +s ( -us ` y ) ) : No typesetting found for class ( x +s ( -us ` y ) ) with typecode class
10	1 3 2 2 9	cmpo	Could not format ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) ) : No typesetting found for class ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) ) with typecode class
11	0 10	wceq	Could not format -s = ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) ) : No typesetting found for wff -s = ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) ) with typecode wff