Metamath Proof Explorer

Theorem eupre

Description: Unique predecessor exists on the successor class. (Contributed by Peter Mazsa, 27-Jan-2026)

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

Proof

Step Hyp Ref Expression
1 df-succl 
 |-  Suc = ran SucMap
2 1 eleq2i 
 |-  ( N e. Suc <-> N e. ran SucMap )
3 eupre2 
 |-  ( N e. V -> ( N e. ran SucMap <-> E! m m SucMap N ) )
4 2 3 bitrid 
 |-  ( N e. V -> ( N e. Suc <-> E! m m SucMap N ) )