Metamath Proof Explorer

Theorem eupre2

Description: Unique predecessor exists on the range of the successor map. (Contributed by Peter Mazsa, 12-Jan-2026)

Ref Expression
Assertion eupre2 
|- ( N e. V -> ( N e. ran SucMap <-> E! m m SucMap N ) )

Proof

Step Hyp Ref Expression
1 elrng 
 |-  ( N e. V -> ( N e. ran SucMap <-> E. m m SucMap N ) )
2 exeupre 
 |-  ( N e. V -> ( E. m m SucMap N <-> E! m m SucMap N ) )
3 1 2 bitrd 
 |-  ( N e. V -> ( N e. ran SucMap <-> E! m m SucMap N ) )