Definition df-suc 4516

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 4557). 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 4510	. 2 class suc 𝐴
3	1	csn 3709	. . 3 class {𝐴}
4	1, 3	cun 3218	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1402	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is used by:  suceq  4547  elsuci  4548  elsucg  4549  elsuc2g  4550  nfsuc  4553  suc0  4556  sucprc  4557  unisuc  4558  unisucg  4559  sssucid  4560  iunsuc  4565  sucexb  4644  ordsucim  4647  ordsucss  4651  2ordpr  4671  orddif  4694  sucprcreg  4696  elomssom  4752  omsinds  4769  tfrlemisucfn  6595  tfr1onlemsucfn  6611  tfrcllemsucfn  6624  rdgisuc1  6655  df2o3  6702  oasuc  6737  omsuc  6745  enpr2d  7111  phplem1  7153  fiunsnnn  7185  unsnfi  7226  fiintim  7238  fidcenumlemrks  7270  fidcenumlemr  7272  nnnninfeq2  7470  nninfwlpoimlemg  7516  pm54.43  7537  dju1en  7570  pw1nel3  7591  sucpw1nel3  7593  frecfzennn  10878  hashp1i  11267  ennnfonelemg  13346  ennnfonelemhdmp1  13352  ennnfonelemkh  13355  ennnfonelemhf1o  13356  bdcsuc  17072  bdeqsuc  17073  bj-sucexg  17114  bj-nntrans  17143  bj-nnelirr  17145  bj-omtrans  17148  nninfsellemdc  17219  nninfsellemsuc  17221