Definition df-suc 4108

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 4149). 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 4102	. 2 class suc A
3	1	csn 3375	. . 3 class { A }
4	1, 3	cun 2915	. 2 class ( A u. { A } )
5	2, 4	wceq 1243	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4139  elsuci  4140  elsucg  4141  elsuc2g  4142  nfsuc  4145  suc0  4148  sucprc  4149  unisuc  4150  unisucg  4151  sssucid  4152  iunsuc  4157  sucexb  4223  ordsucim  4226  ordsucss  4230  2ordpr  4249  orddif  4271  sucprcreg  4273  elnn  4328  tfrlemisucfn  5938  rdgisuc1  5971  df2o3  6014  oasuc  6044  omsuc  6051  phplem1  6315  fiunsnnn  6338  frecfzennn  9203  bdcsuc  10000  bdeqsuc  10001  bj-sucexg  10042  bj-nntrans  10076  bj-nnelirr  10078  bj-omtrans  10081