Theorem negs11

Description: Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		fveq2	Could not format ( ( -us ` A ) = ( -us ` B ) -> ( -us ` ( -us ` A ) ) = ( -us ` ( -us ` B ) ) ) : No typesetting found for |- ( ( -us ` A ) = ( -us ` B ) -> ( -us ` ( -us ` A ) ) = ( -us ` ( -us ` B ) ) ) with typecode |-
2		negnegs	Could not format ( A e. No -> ( -us ` ( -us ` A ) ) = A ) : No typesetting found for |- ( A e. No -> ( -us ` ( -us ` A ) ) = A ) with typecode |-
3		negnegs	Could not format ( B e. No -> ( -us ` ( -us ` B ) ) = B ) : No typesetting found for |- ( B e. No -> ( -us ` ( -us ` B ) ) = B ) with typecode |-
4	2 3	eqeqan12d	Could not format ( ( A e. No /\ B e. No ) -> ( ( -us ` ( -us ` A ) ) = ( -us ` ( -us ` B ) ) <-> A = B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( -us ` ( -us ` A ) ) = ( -us ` ( -us ` B ) ) <-> A = B ) ) with typecode |-
5	1 4	imbitrid	Could not format ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) = ( -us ` B ) -> A = B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) = ( -us ` B ) -> A = B ) ) with typecode |-
6		fveq2	Could not format ( A = B -> ( -us ` A ) = ( -us ` B ) ) : No typesetting found for |- ( A = B -> ( -us ` A ) = ( -us ` B ) ) with typecode |-
7	5 6	impbid1	Could not format ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) = ( -us ` B ) <-> A = B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) = ( -us ` B ) <-> A = B ) ) with typecode |-