Definition df-suc 4511

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 4552). 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 4505	. 2 class suc 𝐴
3	1	csn 3705	. . 3 class {𝐴}
4	1, 3	cun 3218	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1402	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4542  elsuci  4543  elsucg  4544  elsuc2g  4545  nfsuc  4548  suc0  4551  sucprc  4552  unisuc  4553  unisucg  4554  sssucid  4555  iunsuc  4560  sucexb  4639  ordsucim  4642  ordsucss  4646  2ordpr  4666  orddif  4689  sucprcreg  4691  elomssom  4747  omsinds  4764  tfrlemisucfn  6585  tfr1onlemsucfn  6601  tfrcllemsucfn  6614  rdgisuc1  6645  df2o3  6692  oasuc  6727  omsuc  6735  enpr2d  7101  phplem1  7143  fiunsnnn  7175  unsnfi  7216  fiintim  7228  fidcenumlemrks  7260  fidcenumlemr  7262  nnnninfeq2  7459  nninfwlpoimlemg  7505  pm54.43  7526  dju1en  7559  pw1nel3  7580  sucpw1nel3  7582  frecfzennn  10841  hashp1i  11229  ennnfonelemg  13272  ennnfonelemhdmp1  13278  ennnfonelemkh  13281  ennnfonelemhf1o  13282  bdcsuc  16820  bdeqsuc  16821  bj-sucexg  16862  bj-nntrans  16891  bj-nnelirr  16893  bj-omtrans  16896  nninfsellemdc  16958  nninfsellemsuc  16960