Metamath Proof Explorer

Theorem brsucmap

Description: Binary relation form of the successor map, general version. (Contributed by Peter Mazsa, 6-Jan-2026)

Ref Expression
Assertion brsucmap 
|- ( ( M e. V /\ N e. W ) -> ( M SucMap N <-> suc M = N ) )

Proof

Step Hyp Ref Expression
1 suceq 
 |-  ( m = M -> suc m = suc M )
2 id 
 |-  ( n = N -> n = N )
3 1 2 eqeqan12d 
 |-  ( ( m = M /\ n = N ) -> ( suc m = n <-> suc M = N ) )
4 df-sucmap 
 |-  SucMap = { <. m , n >. | suc m = n }
5 3 4 brabga 
 |-  ( ( M e. V /\ N e. W ) -> ( M SucMap N <-> suc M = N ) )