Metamath Proof Explorer

Theorem sucmapsuc

Description: A set is succeeded by its successor. (Contributed by Peter Mazsa, 7-Jan-2026)

Ref Expression
Assertion sucmapsuc 
|- ( M e. V -> M SucMap suc M )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  suc M = suc M
2 sucexg 
 |-  ( M e. V -> suc M e. _V )
3 brsucmap 
 |-  ( ( M e. V /\ suc M e. _V ) -> ( M SucMap suc M <-> suc M = suc M ) )
4 2 3 mpdan 
 |-  ( M e. V -> ( M SucMap suc M <-> suc M = suc M ) )
5 1 4 mpbiri 
 |-  ( M e. V -> M SucMap suc M )