Definition df-suc 4356

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 4397). 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 4350	. 2 class suc A
3	1	csn 3583	. . 3 class { A }
4	1, 3	cun 3119	. 2 class ( A u. { A } )
5	2, 4	wceq 1348	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4387  elsuci  4388  elsucg  4389  elsuc2g  4390  nfsuc  4393  suc0  4396  sucprc  4397  unisuc  4398  unisucg  4399  sssucid  4400  iunsuc  4405  sucexb  4481  ordsucim  4484  ordsucss  4488  2ordpr  4508  orddif  4531  sucprcreg  4533  elomssom  4589  omsinds  4606  tfrlemisucfn  6303  tfr1onlemsucfn  6319  tfrcllemsucfn  6332  rdgisuc1  6363  df2o3  6409  oasuc  6443  omsuc  6451  enpr2d  6795  phplem1  6830  fiunsnnn  6859  unsnfi  6896  fiintim  6906  fidcenumlemrks  6930  fidcenumlemr  6932  nnnninfeq2  7105  nninfwlpoimlemg  7151  pm54.43  7167  dju1en  7190  pw1nel3  7208  sucpw1nel3  7210  frecfzennn  10382  hashp1i  10745  ennnfonelemg  12358  ennnfonelemhdmp1  12364  ennnfonelemkh  12367  ennnfonelemhf1o  12368  bdcsuc  13915  bdeqsuc  13916  bj-sucexg  13957  bj-nntrans  13986  bj-nnelirr  13988  bj-omtrans  13991  nninfsellemdc  14043  nninfsellemsuc  14045