Definition df-suc 4365

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 4406). 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 4359	. 2 class suc 𝐴
3	1	csn 3589	. . 3 class {𝐴}
4	1, 3	cun 3125	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1353	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4396  elsuci  4397  elsucg  4398  elsuc2g  4399  nfsuc  4402  suc0  4405  sucprc  4406  unisuc  4407  unisucg  4408  sssucid  4409  iunsuc  4414  sucexb  4490  ordsucim  4493  ordsucss  4497  2ordpr  4517  orddif  4540  sucprcreg  4542  elomssom  4598  omsinds  4615  tfrlemisucfn  6315  tfr1onlemsucfn  6331  tfrcllemsucfn  6344  rdgisuc1  6375  df2o3  6421  oasuc  6455  omsuc  6463  enpr2d  6807  phplem1  6842  fiunsnnn  6871  unsnfi  6908  fiintim  6918  fidcenumlemrks  6942  fidcenumlemr  6944  nnnninfeq2  7117  nninfwlpoimlemg  7163  pm54.43  7179  dju1en  7202  pw1nel3  7220  sucpw1nel3  7222  frecfzennn  10396  hashp1i  10758  ennnfonelemg  12371  ennnfonelemhdmp1  12377  ennnfonelemkh  12380  ennnfonelemhf1o  12381  bdcsuc  14192  bdeqsuc  14193  bj-sucexg  14234  bj-nntrans  14263  bj-nnelirr  14265  bj-omtrans  14268  nninfsellemdc  14320  nninfsellemsuc  14322