Definition df-suc 4474

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 4515). 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 4468	. 2 class suc A
3	1	csn 3673	. . 3 class { A }
4	1, 3	cun 3199	. 2 class ( A u. { A } )
5	2, 4	wceq 1398	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4505  elsuci  4506  elsucg  4507  elsuc2g  4508  nfsuc  4511  suc0  4514  sucprc  4515  unisuc  4516  unisucg  4517  sssucid  4518  iunsuc  4523  sucexb  4601  ordsucim  4604  ordsucss  4608  2ordpr  4628  orddif  4651  sucprcreg  4653  elomssom  4709  omsinds  4726  tfrlemisucfn  6533  tfr1onlemsucfn  6549  tfrcllemsucfn  6562  rdgisuc1  6593  df2o3  6640  oasuc  6675  omsuc  6683  enpr2d  7040  phplem1  7081  fiunsnnn  7113  unsnfi  7154  fiintim  7166  fidcenumlemrks  7195  fidcenumlemr  7197  nnnninfeq2  7388  nninfwlpoimlemg  7434  pm54.43  7455  dju1en  7488  pw1nel3  7509  sucpw1nel3  7511  frecfzennn  10751  hashp1i  11137  ennnfonelemg  13104  ennnfonelemhdmp1  13110  ennnfonelemkh  13113  ennnfonelemhf1o  13114  bdcsuc  16596  bdeqsuc  16597  bj-sucexg  16638  bj-nntrans  16667  bj-nnelirr  16669  bj-omtrans  16672  nninfsellemdc  16736  nninfsellemsuc  16738