Definition df-suc 4402

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 4443). 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 4396	. 2 class suc 𝐴
3	1	csn 3618	. . 3 class {𝐴}
4	1, 3	cun 3151	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1364	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4433  elsuci  4434  elsucg  4435  elsuc2g  4436  nfsuc  4439  suc0  4442  sucprc  4443  unisuc  4444  unisucg  4445  sssucid  4446  iunsuc  4451  sucexb  4529  ordsucim  4532  ordsucss  4536  2ordpr  4556  orddif  4579  sucprcreg  4581  elomssom  4637  omsinds  4654  tfrlemisucfn  6377  tfr1onlemsucfn  6393  tfrcllemsucfn  6406  rdgisuc1  6437  df2o3  6483  oasuc  6517  omsuc  6525  enpr2d  6871  phplem1  6908  fiunsnnn  6937  unsnfi  6975  fiintim  6985  fidcenumlemrks  7012  fidcenumlemr  7014  nnnninfeq2  7188  nninfwlpoimlemg  7234  pm54.43  7250  dju1en  7273  pw1nel3  7291  sucpw1nel3  7293  frecfzennn  10497  hashp1i  10881  ennnfonelemg  12560  ennnfonelemhdmp1  12566  ennnfonelemkh  12569  ennnfonelemhf1o  12570  bdcsuc  15372  bdeqsuc  15373  bj-sucexg  15414  bj-nntrans  15443  bj-nnelirr  15445  bj-omtrans  15448  nninfsellemdc  15500  nninfsellemsuc  15502