Definition df-suc 4498

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 4539). 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 4492	. 2 class suc A
3	1	csn 3695	. . 3 class { A }
4	1, 3	cun 3212	. 2 class ( A u. { A } )
5	2, 4	wceq 1398	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4529  elsuci  4530  elsucg  4531  elsuc2g  4532  nfsuc  4535  suc0  4538  sucprc  4539  unisuc  4540  unisucg  4541  sssucid  4542  iunsuc  4547  sucexb  4625  ordsucim  4628  ordsucss  4632  2ordpr  4652  orddif  4675  sucprcreg  4677  elomssom  4733  omsinds  4750  tfrlemisucfn  6569  tfr1onlemsucfn  6585  tfrcllemsucfn  6598  rdgisuc1  6629  df2o3  6676  oasuc  6711  omsuc  6719  enpr2d  7078  phplem1  7120  fiunsnnn  7152  unsnfi  7193  fiintim  7205  fidcenumlemrks  7237  fidcenumlemr  7239  nnnninfeq2  7434  nninfwlpoimlemg  7480  pm54.43  7501  dju1en  7534  pw1nel3  7555  sucpw1nel3  7557  frecfzennn  10816  hashp1i  11204  ennnfonelemg  13243  ennnfonelemhdmp1  13249  ennnfonelemkh  13252  ennnfonelemhf1o  13253  bdcsuc  16791  bdeqsuc  16792  bj-sucexg  16833  bj-nntrans  16862  bj-nnelirr  16864  bj-omtrans  16867  nninfsellemdc  16929  nninfsellemsuc  16931