Definition df-suc 4407

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 4448). 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 4401	. 2 class suc A
3	1	csn 3623	. . 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  4438  elsuci  4439  elsucg  4440  elsuc2g  4441  nfsuc  4444  suc0  4447  sucprc  4448  unisuc  4449  unisucg  4450  sssucid  4451  iunsuc  4456  sucexb  4534  ordsucim  4537  ordsucss  4541  2ordpr  4561  orddif  4584  sucprcreg  4586  elomssom  4642  omsinds  4659  tfrlemisucfn  6391  tfr1onlemsucfn  6407  tfrcllemsucfn  6420  rdgisuc1  6451  df2o3  6497  oasuc  6531  omsuc  6539  enpr2d  6885  phplem1  6922  fiunsnnn  6951  unsnfi  6989  fiintim  7001  fidcenumlemrks  7028  fidcenumlemr  7030  nnnninfeq2  7204  nninfwlpoimlemg  7250  pm54.43  7269  dju1en  7296  pw1nel3  7314  sucpw1nel3  7316  frecfzennn  10535  hashp1i  10919  ennnfonelemg  12645  ennnfonelemhdmp1  12651  ennnfonelemkh  12654  ennnfonelemhf1o  12655  bdcsuc  15610  bdeqsuc  15611  bj-sucexg  15652  bj-nntrans  15681  bj-nnelirr  15683  bj-omtrans  15686  nninfsellemdc  15741  nninfsellemsuc  15743