Metamath Proof Explorer

Theorem negs11

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

Ref Expression
Assertion negs11 
|- ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) = ( -us ` B ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( ( -us ` A ) = ( -us ` B ) -> ( -us ` ( -us ` A ) ) = ( -us ` ( -us ` B ) ) )
2 negnegs 
 |-  ( A e. No -> ( -us ` ( -us ` A ) ) = A )
3 negnegs 
 |-  ( B e. No -> ( -us ` ( -us ` B ) ) = B )
4 2 3 eqeqan12d 
 |-  ( ( A e. No /\ B e. No ) -> ( ( -us ` ( -us ` A ) ) = ( -us ` ( -us ` B ) ) <-> A = B ) )
5 1 4 imbitrid 
 |-  ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) = ( -us ` B ) -> A = B ) )
6 fveq2 
 |-  ( A = B -> ( -us ` A ) = ( -us ` B ) )
7 5 6 impbid1 
 |-  ( ( A e. No /\ B e. No ) -> ( ( -us ` A ) = ( -us ` B ) <-> A = B ) )