Definition df-suc 4369

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 4410). 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 4363	. 2 class suc A
3	1	csn 3592	. . 3 class { A }
4	1, 3	cun 3127	. 2 class ( A u. { A } )
5	2, 4	wceq 1353	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4400  elsuci  4401  elsucg  4402  elsuc2g  4403  nfsuc  4406  suc0  4409  sucprc  4410  unisuc  4411  unisucg  4412  sssucid  4413  iunsuc  4418  sucexb  4494  ordsucim  4497  ordsucss  4501  2ordpr  4521  orddif  4544  sucprcreg  4546  elomssom  4602  omsinds  4619  tfrlemisucfn  6320  tfr1onlemsucfn  6336  tfrcllemsucfn  6349  rdgisuc1  6380  df2o3  6426  oasuc  6460  omsuc  6468  enpr2d  6812  phplem1  6847  fiunsnnn  6876  unsnfi  6913  fiintim  6923  fidcenumlemrks  6947  fidcenumlemr  6949  nnnninfeq2  7122  nninfwlpoimlemg  7168  pm54.43  7184  dju1en  7207  pw1nel3  7225  sucpw1nel3  7227  frecfzennn  10419  hashp1i  10781  ennnfonelemg  12394  ennnfonelemhdmp1  12400  ennnfonelemkh  12403  ennnfonelemhf1o  12404  bdcsuc  14403  bdeqsuc  14404  bj-sucexg  14445  bj-nntrans  14474  bj-nnelirr  14476  bj-omtrans  14479  nninfsellemdc  14530  nninfsellemsuc  14532