Definition df-suc 4349

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 4390). 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 4343	. 2 class suc A
3	1	csn 3576	. . 3 class { A }
4	1, 3	cun 3114	. 2 class ( A u. { A } )
5	2, 4	wceq 1343	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4380  elsuci  4381  elsucg  4382  elsuc2g  4383  nfsuc  4386  suc0  4389  sucprc  4390  unisuc  4391  unisucg  4392  sssucid  4393  iunsuc  4398  sucexb  4474  ordsucim  4477  ordsucss  4481  2ordpr  4501  orddif  4524  sucprcreg  4526  elomssom  4582  omsinds  4599  tfrlemisucfn  6292  tfr1onlemsucfn  6308  tfrcllemsucfn  6321  rdgisuc1  6352  df2o3  6398  oasuc  6432  omsuc  6440  enpr2d  6783  phplem1  6818  fiunsnnn  6847  unsnfi  6884  fiintim  6894  fidcenumlemrks  6918  fidcenumlemr  6920  nnnninfeq2  7093  pm54.43  7146  dju1en  7169  pw1nel3  7187  sucpw1nel3  7189  frecfzennn  10361  hashp1i  10723  ennnfonelemg  12336  ennnfonelemhdmp1  12342  ennnfonelemkh  12345  ennnfonelemhf1o  12346  bdcsuc  13762  bdeqsuc  13763  bj-sucexg  13804  bj-nntrans  13833  bj-nnelirr  13835  bj-omtrans  13838  nninfsellemdc  13890  nninfsellemsuc  13892