Definition df-suc 4494

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 4535). 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 4488	. 2 class suc A
3	1	csn 3691	. . 3 class { A }
4	1, 3	cun 3211	. 2 class ( A u. { A } )
5	2, 4	wceq 1398	1 wff suc A = ( A u. { A } )

This definition is referenced by:  suceq  4525  elsuci  4526  elsucg  4527  elsuc2g  4528  nfsuc  4531  suc0  4534  sucprc  4535  unisuc  4536  unisucg  4537  sssucid  4538  iunsuc  4543  sucexb  4621  ordsucim  4624  ordsucss  4628  2ordpr  4648  orddif  4671  sucprcreg  4673  elomssom  4729  omsinds  4746  tfrlemisucfn  6557  tfr1onlemsucfn  6573  tfrcllemsucfn  6586  rdgisuc1  6617  df2o3  6664  oasuc  6699  omsuc  6707  enpr2d  7066  phplem1  7108  fiunsnnn  7140  unsnfi  7181  fiintim  7193  fidcenumlemrks  7225  fidcenumlemr  7227  nnnninfeq2  7422  nninfwlpoimlemg  7468  pm54.43  7489  dju1en  7522  pw1nel3  7543  sucpw1nel3  7545  frecfzennn  10792  hashp1i  11179  ennnfonelemg  13171  ennnfonelemhdmp1  13177  ennnfonelemkh  13180  ennnfonelemhf1o  13181  bdcsuc  16667  bdeqsuc  16668  bj-sucexg  16709  bj-nntrans  16738  bj-nnelirr  16740  bj-omtrans  16743  nninfsellemdc  16805  nninfsellemsuc  16807