Definition df-suc 4343

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 4384). 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 4337	. 2 class suc A
3	1	csn 3570	. . 3 class { A }
4	1, 3	cun 3109	. 2 class ( A u. { A } )
5	2, 4	wceq 1342	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4374  elsuci  4375  elsucg  4376  elsuc2g  4377  nfsuc  4380  suc0  4383  sucprc  4384  unisuc  4385  unisucg  4386  sssucid  4387  iunsuc  4392  sucexb  4468  ordsucim  4471  ordsucss  4475  2ordpr  4495  orddif  4518  sucprcreg  4520  elomssom  4576  omsinds  4593  tfrlemisucfn  6283  tfr1onlemsucfn  6299  tfrcllemsucfn  6312  rdgisuc1  6343  df2o3  6389  oasuc  6423  omsuc  6431  enpr2d  6774  phplem1  6809  fiunsnnn  6838  unsnfi  6875  fiintim  6885  fidcenumlemrks  6909  fidcenumlemr  6911  nnnninfeq2  7084  pm54.43  7137  dju1en  7160  pw1nel3  7178  sucpw1nel3  7180  frecfzennn  10351  hashp1i  10712  ennnfonelemg  12273  ennnfonelemhdmp1  12279  ennnfonelemkh  12282  ennnfonelemhf1o  12283  bdcsuc  13597  bdeqsuc  13598  bj-sucexg  13639  bj-nntrans  13668  bj-nnelirr  13670  bj-omtrans  13673  nninfsellemdc  13724  nninfsellemsuc  13726