Definition df-suc 4461

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 4502). 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 4455	. 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  4492  elsuci  4493  elsucg  4494  elsuc2g  4495  nfsuc  4498  suc0  4501  sucprc  4502  unisuc  4503  unisucg  4504  sssucid  4505  iunsuc  4510  sucexb  4588  ordsucim  4591  ordsucss  4595  2ordpr  4615  orddif  4638  sucprcreg  4640  elomssom  4696  omsinds  4713  tfrlemisucfn  6468  tfr1onlemsucfn  6484  tfrcllemsucfn  6497  rdgisuc1  6528  df2o3  6574  oasuc  6608  omsuc  6616  enpr2d  6970  phplem1  7009  fiunsnnn  7039  unsnfi  7077  fiintim  7089  fidcenumlemrks  7116  fidcenumlemr  7118  nnnninfeq2  7292  nninfwlpoimlemg  7338  pm54.43  7359  dju1en  7391  pw1nel3  7412  sucpw1nel3  7414  frecfzennn  10643  hashp1i  11027  ennnfonelemg  12969  ennnfonelemhdmp1  12975  ennnfonelemkh  12978  ennnfonelemhf1o  12979  bdcsuc  16201  bdeqsuc  16202  bj-sucexg  16243  bj-nntrans  16272  bj-nnelirr  16274  bj-omtrans  16277  nninfsellemdc  16335  nninfsellemsuc  16337