Definition df-suc 4468

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 4509). 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 4462	. 2 class suc 𝐴
3	1	csn 3669	. . 3 class {𝐴}
4	1, 3	cun 3198	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1397	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4499  elsuci  4500  elsucg  4501  elsuc2g  4502  nfsuc  4505  suc0  4508  sucprc  4509  unisuc  4510  unisucg  4511  sssucid  4512  iunsuc  4517  sucexb  4595  ordsucim  4598  ordsucss  4602  2ordpr  4622  orddif  4645  sucprcreg  4647  elomssom  4703  omsinds  4720  tfrlemisucfn  6490  tfr1onlemsucfn  6506  tfrcllemsucfn  6519  rdgisuc1  6550  df2o3  6597  oasuc  6632  omsuc  6640  enpr2d  6997  phplem1  7038  fiunsnnn  7070  unsnfi  7111  fiintim  7123  fidcenumlemrks  7152  fidcenumlemr  7154  nnnninfeq2  7328  nninfwlpoimlemg  7374  pm54.43  7395  dju1en  7428  pw1nel3  7449  sucpw1nel3  7451  frecfzennn  10689  hashp1i  11075  ennnfonelemg  13042  ennnfonelemhdmp1  13048  ennnfonelemkh  13051  ennnfonelemhf1o  13052  bdcsuc  16526  bdeqsuc  16527  bj-sucexg  16568  bj-nntrans  16597  bj-nnelirr  16599  bj-omtrans  16602  nninfsellemdc  16663  nninfsellemsuc  16665