Definition df-suc 4251

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 4292). 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 4245	. 2 class suc A
3	1	csn 3491	. . 3 class { A }
4	1, 3	cun 3033	. 2 class ( A u. { A } )
5	2, 4	wceq 1312	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4282  elsuci  4283  elsucg  4284  elsuc2g  4285  nfsuc  4288  suc0  4291  sucprc  4292  unisuc  4293  unisucg  4294  sssucid  4295  iunsuc  4300  sucexb  4371  ordsucim  4374  ordsucss  4378  2ordpr  4397  orddif  4420  sucprcreg  4422  elnn  4477  omsinds  4493  tfrlemisucfn  6173  tfr1onlemsucfn  6189  tfrcllemsucfn  6202  rdgisuc1  6233  df2o3  6279  oasuc  6312  omsuc  6320  phplem1  6697  fiunsnnn  6726  unsnfi  6758  fiintim  6768  fidcenumlemrks  6791  fidcenumlemr  6793  pm54.43  6993  dju1en  7014  frecfzennn  10086  hashp1i  10443  ennnfonelemg  11755  ennnfonelemhdmp1  11761  ennnfonelemkh  11764  ennnfonelemhf1o  11765  bdcsuc  12761  bdeqsuc  12762  bj-sucexg  12803  bj-nntrans  12832  bj-nnelirr  12834  bj-omtrans  12837  nninfsellemdc  12887  nninfsellemsuc  12889