Definition df-succl

Description: Define Suc as the class of all successors, i.e. the range of the successor map: n e. Suc iff E. m suc m = n (see dfsuccl2 ). By injectivity of suc ( suc11reg ), every n e. Suc has at most one predecessor, which is exactly what pre n ( df-pre ) names. Cf. dfsuccl3 and dfsuccl4 . (Contributed by Peter Mazsa, 25-Jan-2026)

	Ref	Expression
Assertion	df-succl	|- Suc = ran SucMap

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csuccl	|- Suc
1		csucmap	|- SucMap
2	1	crn	|- ran SucMap
3	0 2	wceq	|- Suc = ran SucMap