Definition df-suc 4418

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 4459). 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 4412	. 2 class suc 𝐴
3	1	csn 3633	. . 3 class {𝐴}
4	1, 3	cun 3164	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1373	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4449  elsuci  4450  elsucg  4451  elsuc2g  4452  nfsuc  4455  suc0  4458  sucprc  4459  unisuc  4460  unisucg  4461  sssucid  4462  iunsuc  4467  sucexb  4545  ordsucim  4548  ordsucss  4552  2ordpr  4572  orddif  4595  sucprcreg  4597  elomssom  4653  omsinds  4670  tfrlemisucfn  6410  tfr1onlemsucfn  6426  tfrcllemsucfn  6439  rdgisuc1  6470  df2o3  6516  oasuc  6550  omsuc  6558  enpr2d  6911  phplem1  6949  fiunsnnn  6978  unsnfi  7016  fiintim  7028  fidcenumlemrks  7055  fidcenumlemr  7057  nnnninfeq2  7231  nninfwlpoimlemg  7277  pm54.43  7298  dju1en  7325  pw1nel3  7343  sucpw1nel3  7345  frecfzennn  10571  hashp1i  10955  ennnfonelemg  12774  ennnfonelemhdmp1  12780  ennnfonelemkh  12783  ennnfonelemhf1o  12784  bdcsuc  15816  bdeqsuc  15817  bj-sucexg  15858  bj-nntrans  15887  bj-nnelirr  15889  bj-omtrans  15892  nninfsellemdc  15947  nninfsellemsuc  15949