Definition df-suc 4406

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 4447). 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 4400	. 2 class suc A
3	1	csn 3622	. . 3 class { A }
4	1, 3	cun 3155	. 2 class ( A u. { A } )
5	2, 4	wceq 1364	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4437  elsuci  4438  elsucg  4439  elsuc2g  4440  nfsuc  4443  suc0  4446  sucprc  4447  unisuc  4448  unisucg  4449  sssucid  4450  iunsuc  4455  sucexb  4533  ordsucim  4536  ordsucss  4540  2ordpr  4560  orddif  4583  sucprcreg  4585  elomssom  4641  omsinds  4658  tfrlemisucfn  6382  tfr1onlemsucfn  6398  tfrcllemsucfn  6411  rdgisuc1  6442  df2o3  6488  oasuc  6522  omsuc  6530  enpr2d  6876  phplem1  6913  fiunsnnn  6942  unsnfi  6980  fiintim  6992  fidcenumlemrks  7019  fidcenumlemr  7021  nnnninfeq2  7195  nninfwlpoimlemg  7241  pm54.43  7257  dju1en  7280  pw1nel3  7298  sucpw1nel3  7300  frecfzennn  10518  hashp1i  10902  ennnfonelemg  12620  ennnfonelemhdmp1  12626  ennnfonelemkh  12629  ennnfonelemhf1o  12630  bdcsuc  15526  bdeqsuc  15527  bj-sucexg  15568  bj-nntrans  15597  bj-nnelirr  15599  bj-omtrans  15602  nninfsellemdc  15654  nninfsellemsuc  15656