Theorem dfsuccl2

Description: Alternate definition of the class of all successors. (Contributed by Peter Mazsa, 29-Jan-2026)

	Ref	Expression
Assertion	dfsuccl2	⊢ Suc = { 𝑛 ∣ ∃ 𝑚 suc 𝑚 = 𝑛 }

Proof

Step	Hyp	Ref	Expression
1		df-succl	⊢ Suc = ran SucMap
2		df-sucmap	⊢ SucMap = { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }
3	2	rneqi	⊢ ran SucMap = ran { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }
4		rnopab	⊢ ran { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 } = { 𝑛 ∣ ∃ 𝑚 suc 𝑚 = 𝑛 }
5	1 3 4	3eqtri	⊢ Suc = { 𝑛 ∣ ∃ 𝑚 suc 𝑚 = 𝑛 }