Metamath Proof Explorer


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 ) )