Definition df-suc 4128

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 4169). 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 4122	. 2 class suc 𝐴
3	1	csn 3400	. . 3 class {𝐴}
4	1, 3	cun 2972	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1285	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4159  elsuci  4160  elsucg  4161  elsuc2g  4162  nfsuc  4165  suc0  4168  sucprc  4169  unisuc  4170  unisucg  4171  sssucid  4172  iunsuc  4177  sucexb  4243  ordsucim  4246  ordsucss  4250  2ordpr  4269  orddif  4292  sucprcreg  4294  elnn  4348  tfrlemisucfn  5967  tfr1onlemsucfn  5983  tfrcllemsucfn  5996  rdgisuc1  6027  df2o3  6072  oasuc  6102  omsuc  6109  phplem1  6377  fiunsnnn  6405  unsnfi  6429  pm54.43  6508  frecfzennn  9497  sizep1i  9823  bdcsuc  10814  bdeqsuc  10815  bj-sucexg  10856  bj-nntrans  10889  bj-nnelirr  10891  bj-omtrans  10894