Definition df-suc 4474

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 4515). 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 4468	. 2 class suc 𝐴
3	1	csn 3673	. . 3 class {𝐴}
4	1, 3	cun 3199	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1398	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4505  elsuci  4506  elsucg  4507  elsuc2g  4508  nfsuc  4511  suc0  4514  sucprc  4515  unisuc  4516  unisucg  4517  sssucid  4518  iunsuc  4523  sucexb  4601  ordsucim  4604  ordsucss  4608  2ordpr  4628  orddif  4651  sucprcreg  4653  elomssom  4709  omsinds  4726  tfrlemisucfn  6533  tfr1onlemsucfn  6549  tfrcllemsucfn  6562  rdgisuc1  6593  df2o3  6640  oasuc  6675  omsuc  6683  enpr2d  7040  phplem1  7081  fiunsnnn  7113  unsnfi  7154  fiintim  7166  fidcenumlemrks  7195  fidcenumlemr  7197  nnnninfeq2  7371  nninfwlpoimlemg  7417  pm54.43  7438  dju1en  7471  pw1nel3  7492  sucpw1nel3  7494  frecfzennn  10734  hashp1i  11120  ennnfonelemg  13087  ennnfonelemhdmp1  13093  ennnfonelemkh  13096  ennnfonelemhf1o  13097  bdcsuc  16579  bdeqsuc  16580  bj-sucexg  16621  bj-nntrans  16650  bj-nnelirr  16652  bj-omtrans  16655  nninfsellemdc  16719  nninfsellemsuc  16721