Theorem subseq0d

Description: The difference between two surreals is zero iff they are equal. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Hypotheses	subseq0d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	subseq0d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	subseq0d	⊢ ( 𝜑 → ( ( 𝐴 -s 𝐵 ) = 0s ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		subseq0d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		subseq0d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		subsid	⊢ ( 𝐵 ∈ No → ( 𝐵 -s 𝐵 ) = 0s )
4	2 3	syl	⊢ ( 𝜑 → ( 𝐵 -s 𝐵 ) = 0s )
5	4	eqeq2d	⊢ ( 𝜑 → ( ( 𝐴 -s 𝐵 ) = ( 𝐵 -s 𝐵 ) ↔ ( 𝐴 -s 𝐵 ) = 0s ) )
6	1 2 2	subscan2d	⊢ ( 𝜑 → ( ( 𝐴 -s 𝐵 ) = ( 𝐵 -s 𝐵 ) ↔ 𝐴 = 𝐵 ) )
7	5 6	bitr3d	⊢ ( 𝜑 → ( ( 𝐴 -s 𝐵 ) = 0s ↔ 𝐴 = 𝐵 ) )