Definition df-succf

Description: Define the successor function. See brsuccf for its value. (Contributed by Scott Fenton, 14-Apr-2014)

	Ref	Expression
Assertion	df-succf	|- Succ = ( Cup o. ( _I (x) Singleton ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csuccf	|- Succ
1		ccup	|- Cup
2		cid	|- _I
3		csingle	|- Singleton
4	2 3	ctxp	|- ( _I (x) Singleton )
5	1 4	ccom	|- ( Cup o. ( _I (x) Singleton ) )
6	0 5	wceq	|- Succ = ( Cup o. ( _I (x) Singleton ) )