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  6476  tfr1onlemsucfn  6492  tfrcllemsucfn  6505  rdgisuc1  6536  df2o3  6583  oasuc  6618  omsuc  6626  enpr2d  6980  phplem1  7021  fiunsnnn  7051  unsnfi  7092  fiintim  7104  fidcenumlemrks  7131  fidcenumlemr  7133  nnnninfeq2  7307  nninfwlpoimlemg  7353  pm54.43  7374  dju1en  7406  pw1nel3  7427  sucpw1nel3  7429  frecfzennn  10660  hashp1i  11045  ennnfonelemg  12990  ennnfonelemhdmp1  12996  ennnfonelemkh  12999  ennnfonelemhf1o  13000  bdcsuc  16326  bdeqsuc  16327  bj-sucexg  16368  bj-nntrans  16397  bj-nnelirr  16399  bj-omtrans  16402  nninfsellemdc  16464  nninfsellemsuc  16466