Definition df-suc 4462

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 4503). 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 4456	. 2 class suc A
3	1	csn 3666	. . 3 class { A }
4	1, 3	cun 3195	. 2 class ( A u. { A } )
5	2, 4	wceq 1395	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4493  elsuci  4494  elsucg  4495  elsuc2g  4496  nfsuc  4499  suc0  4502  sucprc  4503  unisuc  4504  unisucg  4505  sssucid  4506  iunsuc  4511  sucexb  4589  ordsucim  4592  ordsucss  4596  2ordpr  4616  orddif  4639  sucprcreg  4641  elomssom  4697  omsinds  4714  tfrlemisucfn  6470  tfr1onlemsucfn  6486  tfrcllemsucfn  6499  rdgisuc1  6530  df2o3  6576  oasuc  6610  omsuc  6618  enpr2d  6972  phplem1  7013  fiunsnnn  7043  unsnfi  7081  fiintim  7093  fidcenumlemrks  7120  fidcenumlemr  7122  nnnninfeq2  7296  nninfwlpoimlemg  7342  pm54.43  7363  dju1en  7395  pw1nel3  7416  sucpw1nel3  7418  frecfzennn  10648  hashp1i  11032  ennnfonelemg  12974  ennnfonelemhdmp1  12980  ennnfonelemkh  12983  ennnfonelemhf1o  12984  bdcsuc  16243  bdeqsuc  16244  bj-sucexg  16285  bj-nntrans  16314  bj-nnelirr  16316  bj-omtrans  16319  nninfsellemdc  16376  nninfsellemsuc  16378