Definition df-suc 4419

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 4460). 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 4413	. 2 class suc A
3	1	csn 3633	. . 3 class { A }
4	1, 3	cun 3164	. 2 class ( A u. { A } )
5	2, 4	wceq 1373	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4450  elsuci  4451  elsucg  4452  elsuc2g  4453  nfsuc  4456  suc0  4459  sucprc  4460  unisuc  4461  unisucg  4462  sssucid  4463  iunsuc  4468  sucexb  4546  ordsucim  4549  ordsucss  4553  2ordpr  4573  orddif  4596  sucprcreg  4598  elomssom  4654  omsinds  4671  tfrlemisucfn  6412  tfr1onlemsucfn  6428  tfrcllemsucfn  6441  rdgisuc1  6472  df2o3  6518  oasuc  6552  omsuc  6560  enpr2d  6913  phplem1  6951  fiunsnnn  6980  unsnfi  7018  fiintim  7030  fidcenumlemrks  7057  fidcenumlemr  7059  nnnninfeq2  7233  nninfwlpoimlemg  7279  pm54.43  7300  dju1en  7327  pw1nel3  7345  sucpw1nel3  7347  frecfzennn  10573  hashp1i  10957  ennnfonelemg  12807  ennnfonelemhdmp1  12813  ennnfonelemkh  12816  ennnfonelemhf1o  12817  bdcsuc  15853  bdeqsuc  15854  bj-sucexg  15895  bj-nntrans  15924  bj-nnelirr  15926  bj-omtrans  15929  nninfsellemdc  15984  nninfsellemsuc  15986