Definition df-suc 4372

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 4413). 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 4366	. 2 class suc A
3	1	csn 3593	. . 3 class { A }
4	1, 3	cun 3128	. 2 class ( A u. { A } )
5	2, 4	wceq 1353	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4403  elsuci  4404  elsucg  4405  elsuc2g  4406  nfsuc  4409  suc0  4412  sucprc  4413  unisuc  4414  unisucg  4415  sssucid  4416  iunsuc  4421  sucexb  4497  ordsucim  4500  ordsucss  4504  2ordpr  4524  orddif  4547  sucprcreg  4549  elomssom  4605  omsinds  4622  tfrlemisucfn  6325  tfr1onlemsucfn  6341  tfrcllemsucfn  6354  rdgisuc1  6385  df2o3  6431  oasuc  6465  omsuc  6473  enpr2d  6817  phplem1  6852  fiunsnnn  6881  unsnfi  6918  fiintim  6928  fidcenumlemrks  6952  fidcenumlemr  6954  nnnninfeq2  7127  nninfwlpoimlemg  7173  pm54.43  7189  dju1en  7212  pw1nel3  7230  sucpw1nel3  7232  frecfzennn  10426  hashp1i  10790  ennnfonelemg  12404  ennnfonelemhdmp1  12410  ennnfonelemkh  12413  ennnfonelemhf1o  12414  bdcsuc  14635  bdeqsuc  14636  bj-sucexg  14677  bj-nntrans  14706  bj-nnelirr  14708  bj-omtrans  14711  nninfsellemdc  14762  nninfsellemsuc  14764