Theorem subsval

Description: The value of surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	subsval	|- ( ( A e. No /\ B e. No ) -> ( A -s B ) = ( A +s ( -us ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	|- ( x = A -> ( x +s ( -us ` y ) ) = ( A +s ( -us ` y ) ) )
2		fveq2	|- ( y = B -> ( -us ` y ) = ( -us ` B ) )
3	2	oveq2d	|- ( y = B -> ( A +s ( -us ` y ) ) = ( A +s ( -us ` B ) ) )
4		df-subs	|- -s = ( x e. No , y e. No |-> ( x +s ( -us ` y ) ) )
5		ovex	|- ( A +s ( -us ` B ) ) e. _V
6	1 3 4 5	ovmpo	|- ( ( A e. No /\ B e. No ) -> ( A -s B ) = ( A +s ( -us ` B ) ) )