Definition df-suc 4492

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 4533). 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 4486	. 2 class suc 𝐴
3	1	csn 3689	. . 3 class {𝐴}
4	1, 3	cun 3209	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1398	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4523  elsuci  4524  elsucg  4525  elsuc2g  4526  nfsuc  4529  suc0  4532  sucprc  4533  unisuc  4534  unisucg  4535  sssucid  4536  iunsuc  4541  sucexb  4619  ordsucim  4622  ordsucss  4626  2ordpr  4646  orddif  4669  sucprcreg  4671  elomssom  4727  omsinds  4744  tfrlemisucfn  6555  tfr1onlemsucfn  6571  tfrcllemsucfn  6584  rdgisuc1  6615  df2o3  6662  oasuc  6697  omsuc  6705  enpr2d  7064  phplem1  7106  fiunsnnn  7138  unsnfi  7179  fiintim  7191  fidcenumlemrks  7223  fidcenumlemr  7225  nnnninfeq2  7420  nninfwlpoimlemg  7466  pm54.43  7487  dju1en  7520  pw1nel3  7541  sucpw1nel3  7543  frecfzennn  10788  hashp1i  11175  ennnfonelemg  13154  ennnfonelemhdmp1  13160  ennnfonelemkh  13163  ennnfonelemhf1o  13164  bdcsuc  16650  bdeqsuc  16651  bj-sucexg  16692  bj-nntrans  16721  bj-nnelirr  16723  bj-omtrans  16726  nninfsellemdc  16788  nninfsellemsuc  16790