Definition df-suc 4468

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 4509). 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 4462	. 2 class suc 𝐴
3	1	csn 3669	. . 3 class {𝐴}
4	1, 3	cun 3198	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1397	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4499  elsuci  4500  elsucg  4501  elsuc2g  4502  nfsuc  4505  suc0  4508  sucprc  4509  unisuc  4510  unisucg  4511  sssucid  4512  iunsuc  4517  sucexb  4595  ordsucim  4598  ordsucss  4602  2ordpr  4622  orddif  4645  sucprcreg  4647  elomssom  4703  omsinds  4720  tfrlemisucfn  6489  tfr1onlemsucfn  6505  tfrcllemsucfn  6518  rdgisuc1  6549  df2o3  6596  oasuc  6631  omsuc  6639  enpr2d  6996  phplem1  7037  fiunsnnn  7069  unsnfi  7110  fiintim  7122  fidcenumlemrks  7151  fidcenumlemr  7153  nnnninfeq2  7327  nninfwlpoimlemg  7373  pm54.43  7394  dju1en  7427  pw1nel3  7448  sucpw1nel3  7450  frecfzennn  10687  hashp1i  11073  ennnfonelemg  13023  ennnfonelemhdmp1  13029  ennnfonelemkh  13032  ennnfonelemhf1o  13033  bdcsuc  16475  bdeqsuc  16476  bj-sucexg  16517  bj-nntrans  16546  bj-nnelirr  16548  bj-omtrans  16551  nninfsellemdc  16612  nninfsellemsuc  16614