Definition df-suc 4518

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 4559). 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 A = ( A u. { A } )

Detailed syntax breakdown of Definition df-suc

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	csuc 4512	. 2 class suc A
3	1	csn 3709	. . 3 class { A }
4	1, 3	cun 3218	. 2 class ( A u. { A } )
5	2, 4	wceq 1402	1 wff suc A = ( A u. { A } )

This definition is used by:  suceq  4549  elsuci  4550  elsucg  4551  elsuc2g  4552  nfsuc  4555  suc0  4558  sucprc  4559  unisuc  4560  unisucg  4561  sssucid  4562  iunsuc  4567  sucexb  4646  ordsucim  4649  ordsucss  4653  2ordpr  4673  orddif  4696  sucprcreg  4698  elomssom  4754  omsinds  4771  tfrlemisucfn  6599  tfr1onlemsucfn  6615  tfrcllemsucfn  6628  rdgisuc1  6659  df2o3  6706  oasuc  6741  omsuc  6749  enpr2d  7115  phplem1  7157  fiunsnnn  7189  unsnfi  7230  fiintim  7242  fidcenumlemrks  7275  fidcenumlemr  7277  nnnninfeq2  7475  nninfwlpoimlemg  7521  pm54.43  7542  dju1en  7575  pw1nel3  7596  sucpw1nel3  7598  frecfzennn  10884  hashp1i  11273  ennnfonelemg  13352  ennnfonelemhdmp1  13358  ennnfonelemkh  13361  ennnfonelemhf1o  13362  bdcsuc  17111  bdeqsuc  17112  bj-sucexg  17153  bj-nntrans  17182  bj-nnelirr  17184  bj-omtrans  17187  nninfsellemdc  17259  nninfsellemsuc  17261