Theorem eupre

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

	Ref	Expression
Assertion	eupre	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ Suc ↔ ∃! 𝑚 𝑚 SucMap 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		df-succl	⊢ Suc = ran SucMap
2	1	eleq2i	⊢ ( 𝑁 ∈ Suc ↔ 𝑁 ∈ ran SucMap )
3		eupre2	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ ran SucMap ↔ ∃! 𝑚 𝑚 SucMap 𝑁 ) )
4	2 3	bitrid	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑁 ∈ Suc ↔ ∃! 𝑚 𝑚 SucMap 𝑁 ) )