Theorem preex

Description: The successor-predecessor exists. (Contributed by Peter Mazsa, 12-Jan-2026)

	Ref	Expression
Assertion	preex	⊢ pre 𝑁 ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-pre	⊢ pre 𝑁 = ( ℩ 𝑚 𝑚 ∈ Pred ( SucMap , dom SucMap , 𝑁 ) )
2		iotaex	⊢ ( ℩ 𝑚 𝑚 ∈ Pred ( SucMap , dom SucMap , 𝑁 ) ) ∈ V
3	1 2	eqeltri	⊢ pre 𝑁 ∈ V