Definition df-suc 4293

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 4334). 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 4287	. 2 class suc A
3	1	csn 3527	. . 3 class { A }
4	1, 3	cun 3069	. 2 class ( A u. { A } )
5	2, 4	wceq 1331	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4324  elsuci  4325  elsucg  4326  elsuc2g  4327  nfsuc  4330  suc0  4333  sucprc  4334  unisuc  4335  unisucg  4336  sssucid  4337  iunsuc  4342  sucexb  4413  ordsucim  4416  ordsucss  4420  2ordpr  4439  orddif  4462  sucprcreg  4464  elnn  4519  omsinds  4535  tfrlemisucfn  6221  tfr1onlemsucfn  6237  tfrcllemsucfn  6250  rdgisuc1  6281  df2o3  6327  oasuc  6360  omsuc  6368  enpr2d  6711  phplem1  6746  fiunsnnn  6775  unsnfi  6807  fiintim  6817  fidcenumlemrks  6841  fidcenumlemr  6843  pm54.43  7046  dju1en  7069  frecfzennn  10199  hashp1i  10556  ennnfonelemg  11916  ennnfonelemhdmp1  11922  ennnfonelemkh  11925  ennnfonelemhf1o  11926  bdcsuc  13078  bdeqsuc  13079  bj-sucexg  13120  bj-nntrans  13149  bj-nnelirr  13151  bj-omtrans  13154  nninfsellemdc  13206  nninfsellemsuc  13208