Definition df-suc 4407

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 4448). 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 4401	. 2 class suc 𝐴
3	1	csn 3623	. . 3 class {𝐴}
4	1, 3	cun 3155	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1364	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4438  elsuci  4439  elsucg  4440  elsuc2g  4441  nfsuc  4444  suc0  4447  sucprc  4448  unisuc  4449  unisucg  4450  sssucid  4451  iunsuc  4456  sucexb  4534  ordsucim  4537  ordsucss  4541  2ordpr  4561  orddif  4584  sucprcreg  4586  elomssom  4642  omsinds  4659  tfrlemisucfn  6391  tfr1onlemsucfn  6407  tfrcllemsucfn  6420  rdgisuc1  6451  df2o3  6497  oasuc  6531  omsuc  6539  enpr2d  6885  phplem1  6922  fiunsnnn  6951  unsnfi  6989  fiintim  7001  fidcenumlemrks  7028  fidcenumlemr  7030  nnnninfeq2  7204  nninfwlpoimlemg  7250  pm54.43  7271  dju1en  7298  pw1nel3  7316  sucpw1nel3  7318  frecfzennn  10537  hashp1i  10921  ennnfonelemg  12647  ennnfonelemhdmp1  12653  ennnfonelemkh  12656  ennnfonelemhf1o  12657  bdcsuc  15634  bdeqsuc  15635  bj-sucexg  15676  bj-nntrans  15705  bj-nnelirr  15707  bj-omtrans  15710  nninfsellemdc  15765  nninfsellemsuc  15767