Metamath Proof Explorer

Theorem exeupre2

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

Ref Expression
Assertion exeupre2 
|- ( E. m suc m = N <-> E! m suc m = N )

Proof

Step Hyp Ref Expression
1 mopre 
 |-  E* m suc m = N
2 moeuex 
 |-  ( E* m suc m = N -> ( E. m suc m = N <-> E! m suc m = N ) )
3 1 2 ax-mp 
 |-  ( E. m suc m = N <-> E! m suc m = N )