Theorem subsval

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

	Ref	Expression
Assertion	subsval	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 -s 𝐵 ) = ( 𝐴 +s ( -us ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 +s ( -us ‘ 𝑦 ) ) = ( 𝐴 +s ( -us ‘ 𝑦 ) ) )
2		fveq2	⊢ ( 𝑦 = 𝐵 → ( -us ‘ 𝑦 ) = ( -us ‘ 𝐵 ) )
3	2	oveq2d	⊢ ( 𝑦 = 𝐵 → ( 𝐴 +s ( -us ‘ 𝑦 ) ) = ( 𝐴 +s ( -us ‘ 𝐵 ) ) )
4		df-subs	⊢ -s = ( 𝑥 ∈ No , 𝑦 ∈ No ↦ ( 𝑥 +s ( -us ‘ 𝑦 ) ) )
5		ovex	⊢ ( 𝐴 +s ( -us ‘ 𝐵 ) ) ∈ V
6	1 3 4 5	ovmpo	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 -s 𝐵 ) = ( 𝐴 +s ( -us ‘ 𝐵 ) ) )