Definition df-suc 4462

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 4503). 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 4456	. 2 class suc 𝐴
3	1	csn 3666	. . 3 class {𝐴}
4	1, 3	cun 3195	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1395	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4493  elsuci  4494  elsucg  4495  elsuc2g  4496  nfsuc  4499  suc0  4502  sucprc  4503  unisuc  4504  unisucg  4505  sssucid  4506  iunsuc  4511  sucexb  4589  ordsucim  4592  ordsucss  4596  2ordpr  4616  orddif  4639  sucprcreg  4641  elomssom  4697  omsinds  4714  tfrlemisucfn  6476  tfr1onlemsucfn  6492  tfrcllemsucfn  6505  rdgisuc1  6536  df2o3  6583  oasuc  6618  omsuc  6626  enpr2d  6980  phplem1  7021  fiunsnnn  7051  unsnfi  7089  fiintim  7101  fidcenumlemrks  7128  fidcenumlemr  7130  nnnninfeq2  7304  nninfwlpoimlemg  7350  pm54.43  7371  dju1en  7403  pw1nel3  7424  sucpw1nel3  7426  frecfzennn  10656  hashp1i  11040  ennnfonelemg  12982  ennnfonelemhdmp1  12988  ennnfonelemkh  12991  ennnfonelemhf1o  12992  bdcsuc  16267  bdeqsuc  16268  bj-sucexg  16309  bj-nntrans  16338  bj-nnelirr  16340  bj-omtrans  16343  nninfsellemdc  16406  nninfsellemsuc  16408