Metamath Proof Explorer

Theorem exeupre

Description: Whenever a predecessor exists, it exists alone. (Contributed by Peter Mazsa, 12-Jan-2026)

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

Proof

Step Hyp Ref Expression
1 brsucmap 
 |-  ( ( m e. _V /\ N e. V ) -> ( m SucMap N <-> suc m = N ) )
2 1 el2v1 
 |-  ( N e. V -> ( m SucMap N <-> suc m = N ) )
3 2 exbidv 
 |-  ( N e. V -> ( E. m m SucMap N <-> E. m suc m = N ) )
4 exeupre2 
 |-  ( E. m suc m = N <-> E! m suc m = N )
5 3 4 bitrdi 
 |-  ( N e. V -> ( E. m m SucMap N <-> E! m suc m = N ) )
6 2 eubidv 
 |-  ( N e. V -> ( E! m m SucMap N <-> E! m suc m = N ) )
7 5 6 bitr4d 
 |-  ( N e. V -> ( E. m m SucMap N <-> E! m m SucMap N ) )