Definition df-suc 4074

Description: Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1". Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 4115). Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
df-suc	|- suc A = (A u. {A })

Detailed syntax breakdown of Definition df-suc

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	csuc 4068	. 2 class suc A
3	1	csn 3367	. . 3 class {A }
4	1, 3	cun 2909	. 2 class (A u. {A })
5	2, 4	wceq 1242	1 wff suc A = (A u. {A })

This definition is referenced by:  suceq  4105  elsuci  4106  elsucg  4107  elsuc2g  4108  nfsuc  4111  suc0  4114  sucprc  4115  unisuc  4116  unisucg  4117  sssucid  4118  iunsuc  4123  sucexb  4189  ordsucim  4192  ordsucss  4196  onsucelsucexmidlem  4214  sucprcreg  4227  elnn  4271  tfrlemisucfn  5879  rdgisuc1  5911  df2o3  5953  oasuc  5983  omsuc  5990  frecfzennn  8864  bdcsuc  9315  bdeqsuc  9316  bj-sucexg  9353  bj-nntrans  9385  bj-nnelirr  9387  bj-omtrans  9390