Definition df-suc 4301

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 4342). 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 𝐴 = (𝐴 ∪ {𝐴})

Detailed syntax breakdown of Definition df-suc

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	csuc 4295	. 2 class suc 𝐴
3	1	csn 3532	. . 3 class {𝐴}
4	1, 3	cun 3074	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1332	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4332  elsuci  4333  elsucg  4334  elsuc2g  4335  nfsuc  4338  suc0  4341  sucprc  4342  unisuc  4343  unisucg  4344  sssucid  4345  iunsuc  4350  sucexb  4421  ordsucim  4424  ordsucss  4428  2ordpr  4447  orddif  4470  sucprcreg  4472  elnn  4527  omsinds  4543  tfrlemisucfn  6229  tfr1onlemsucfn  6245  tfrcllemsucfn  6258  rdgisuc1  6289  df2o3  6335  oasuc  6368  omsuc  6376  enpr2d  6719  phplem1  6754  fiunsnnn  6783  unsnfi  6815  fiintim  6825  fidcenumlemrks  6849  fidcenumlemr  6851  pm54.43  7063  dju1en  7086  frecfzennn  10230  hashp1i  10588  ennnfonelemg  11952  ennnfonelemhdmp1  11958  ennnfonelemkh  11961  ennnfonelemhf1o  11962  bdcsuc  13249  bdeqsuc  13250  bj-sucexg  13291  bj-nntrans  13320  bj-nnelirr  13322  bj-omtrans  13325  nninfsellemdc  13381  nninfsellemsuc  13383