Definition df-suc 4497

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 4538). 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 4491	. 2 class suc 𝐴
3	1	csn 3694	. . 3 class {𝐴}
4	1, 3	cun 3212	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1398	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4528  elsuci  4529  elsucg  4530  elsuc2g  4531  nfsuc  4534  suc0  4537  sucprc  4538  unisuc  4539  unisucg  4540  sssucid  4541  iunsuc  4546  sucexb  4624  ordsucim  4627  ordsucss  4631  2ordpr  4651  orddif  4674  sucprcreg  4676  elomssom  4732  omsinds  4749  tfrlemisucfn  6568  tfr1onlemsucfn  6584  tfrcllemsucfn  6597  rdgisuc1  6628  df2o3  6675  oasuc  6710  omsuc  6718  enpr2d  7077  phplem1  7119  fiunsnnn  7151  unsnfi  7192  fiintim  7204  fidcenumlemrks  7236  fidcenumlemr  7238  nnnninfeq2  7433  nninfwlpoimlemg  7479  pm54.43  7500  dju1en  7533  pw1nel3  7554  sucpw1nel3  7556  frecfzennn  10812  hashp1i  11200  ennnfonelemg  13238  ennnfonelemhdmp1  13244  ennnfonelemkh  13247  ennnfonelemhf1o  13248  bdcsuc  16776  bdeqsuc  16777  bj-sucexg  16818  bj-nntrans  16847  bj-nnelirr  16849  bj-omtrans  16852  nninfsellemdc  16914  nninfsellemsuc  16916