Definition df-suc 4466

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 4507). 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 4460	. 2 class suc 𝐴
3	1	csn 3667	. . 3 class {𝐴}
4	1, 3	cun 3196	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1395	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4497  elsuci  4498  elsucg  4499  elsuc2g  4500  nfsuc  4503  suc0  4506  sucprc  4507  unisuc  4508  unisucg  4509  sssucid  4510  iunsuc  4515  sucexb  4593  ordsucim  4596  ordsucss  4600  2ordpr  4620  orddif  4643  sucprcreg  4645  elomssom  4701  omsinds  4718  tfrlemisucfn  6485  tfr1onlemsucfn  6501  tfrcllemsucfn  6514  rdgisuc1  6545  df2o3  6592  oasuc  6627  omsuc  6635  enpr2d  6992  phplem1  7033  fiunsnnn  7063  unsnfi  7104  fiintim  7116  fidcenumlemrks  7143  fidcenumlemr  7145  nnnninfeq2  7319  nninfwlpoimlemg  7365  pm54.43  7386  dju1en  7418  pw1nel3  7439  sucpw1nel3  7441  frecfzennn  10678  hashp1i  11064  ennnfonelemg  13014  ennnfonelemhdmp1  13020  ennnfonelemkh  13023  ennnfonelemhf1o  13024  bdcsuc  16411  bdeqsuc  16412  bj-sucexg  16453  bj-nntrans  16482  bj-nnelirr  16484  bj-omtrans  16487  nninfsellemdc  16548  nninfsellemsuc  16550