Theorem subsval

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

	Ref	Expression
Assertion	subsval	Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A -s B ) = ( A +s ( -us ` B ) ) ) with typecode |-

Proof

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