Definition df-suc 4514

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 4555). 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 4508	. 2 class suc A
3	1	csn 3708	. . 3 class { A }
4	1, 3	cun 3218	. 2 class ( A u. { A } )
5	2, 4	wceq 1402	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4545  elsuci  4546  elsucg  4547  elsuc2g  4548  nfsuc  4551  suc0  4554  sucprc  4555  unisuc  4556  unisucg  4557  sssucid  4558  iunsuc  4563  sucexb  4642  ordsucim  4645  ordsucss  4649  2ordpr  4669  orddif  4692  sucprcreg  4694  elomssom  4750  omsinds  4767  tfrlemisucfn  6588  tfr1onlemsucfn  6604  tfrcllemsucfn  6617  rdgisuc1  6648  df2o3  6695  oasuc  6730  omsuc  6738  enpr2d  7104  phplem1  7146  fiunsnnn  7178  unsnfi  7219  fiintim  7231  fidcenumlemrks  7263  fidcenumlemr  7265  nnnninfeq2  7462  nninfwlpoimlemg  7508  pm54.43  7529  dju1en  7562  pw1nel3  7583  sucpw1nel3  7585  frecfzennn  10844  hashp1i  11232  ennnfonelemg  13275  ennnfonelemhdmp1  13281  ennnfonelemkh  13284  ennnfonelemhf1o  13285  bdcsuc  16823  bdeqsuc  16824  bj-sucexg  16865  bj-nntrans  16894  bj-nnelirr  16896  bj-omtrans  16899  nninfsellemdc  16961  nninfsellemsuc  16963