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	|- ( ph -> A e. No )
	subseq0d.2	|- ( ph -> B e. No )
Assertion	subseq0d	|- ( ph -> ( ( A -s B ) = 0s <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		subseq0d.1	|- ( ph -> A e. No )
2		subseq0d.2	|- ( ph -> B e. No )
3		subsid	|- ( B e. No -> ( B -s B ) = 0s )
4	2 3	syl	|- ( ph -> ( B -s B ) = 0s )
5	4	eqeq2d	|- ( ph -> ( ( A -s B ) = ( B -s B ) <-> ( A -s B ) = 0s ) )
6	1 2 2	subscan2d	|- ( ph -> ( ( A -s B ) = ( B -s B ) <-> A = B ) )
7	5 6	bitr3d	|- ( ph -> ( ( A -s B ) = 0s <-> A = B ) )