Definition df-suc 4417

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 4458). 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 4411	. 2 class suc 𝐴
3	1	csn 3632	. . 3 class {𝐴}
4	1, 3	cun 3163	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1372	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4448  elsuci  4449  elsucg  4450  elsuc2g  4451  nfsuc  4454  suc0  4457  sucprc  4458  unisuc  4459  unisucg  4460  sssucid  4461  iunsuc  4466  sucexb  4544  ordsucim  4547  ordsucss  4551  2ordpr  4571  orddif  4594  sucprcreg  4596  elomssom  4652  omsinds  4669  tfrlemisucfn  6409  tfr1onlemsucfn  6425  tfrcllemsucfn  6438  rdgisuc1  6469  df2o3  6515  oasuc  6549  omsuc  6557  enpr2d  6910  phplem1  6948  fiunsnnn  6977  unsnfi  7015  fiintim  7027  fidcenumlemrks  7054  fidcenumlemr  7056  nnnninfeq2  7230  nninfwlpoimlemg  7276  pm54.43  7297  dju1en  7324  pw1nel3  7342  sucpw1nel3  7344  frecfzennn  10569  hashp1i  10953  ennnfonelemg  12745  ennnfonelemhdmp1  12751  ennnfonelemkh  12754  ennnfonelemhf1o  12755  bdcsuc  15778  bdeqsuc  15779  bj-sucexg  15820  bj-nntrans  15849  bj-nnelirr  15851  bj-omtrans  15854  nninfsellemdc  15909  nninfsellemsuc  15911