Definition df-suc 4126

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 4167). 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 4120	. 2 class suc A
3	1	csn 3398	. . 3 class { A }
4	1, 3	cun 2971	. 2 class ( A u. { A } )
5	2, 4	wceq 1284	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4157  elsuci  4158  elsucg  4159  elsuc2g  4160  nfsuc  4163  suc0  4166  sucprc  4167  unisuc  4168  unisucg  4169  sssucid  4170  iunsuc  4175  sucexb  4241  ordsucim  4244  ordsucss  4248  2ordpr  4267  orddif  4290  sucprcreg  4292  elnn  4346  tfrlemisucfn  5961  rdgisuc1  5994  df2o3  6037  oasuc  6067  omsuc  6074  phplem1  6338  fiunsnnn  6365  unsnfi  6384  pm54.43  6459  frecfzennn  9419  bdcsuc  10671  bdeqsuc  10672  bj-sucexg  10713  bj-nntrans  10746  bj-nnelirr  10748  bj-omtrans  10751