Metamath Proof Explorer

Theorem dfsucmap4

Description: Alternate definition of the successor map. (Contributed by Peter Mazsa, 28-Jan-2026)

Ref Expression
Assertion dfsucmap4 
|- SucMap = ( m e. _V |-> suc m )

Proof

Step Hyp Ref Expression
1 eqcom 
 |-  ( n = suc m <-> suc m = n )
2 1 opabbii 
 |-  { <. m , n >. | n = suc m } = { <. m , n >. | suc m = n }
3 mptv 
 |-  ( m e. _V |-> suc m ) = { <. m , n >. | n = suc m }
4 df-sucmap 
 |-  SucMap = { <. m , n >. | suc m = n }
5 2 3 4 3eqtr4ri 
 |-  SucMap = ( m e. _V |-> suc m )