Definition df-suc 4403

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 4444). 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 𝐴 = (𝐴 ∪ {𝐴})

Detailed syntax breakdown of Definition df-suc

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	csuc 4397	. 2 class suc 𝐴
3	1	csn 3619	. . 3 class {𝐴}
4	1, 3	cun 3152	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1364	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4434  elsuci  4435  elsucg  4436  elsuc2g  4437  nfsuc  4440  suc0  4443  sucprc  4444  unisuc  4445  unisucg  4446  sssucid  4447  iunsuc  4452  sucexb  4530  ordsucim  4533  ordsucss  4537  2ordpr  4557  orddif  4580  sucprcreg  4582  elomssom  4638  omsinds  4655  tfrlemisucfn  6379  tfr1onlemsucfn  6395  tfrcllemsucfn  6408  rdgisuc1  6439  df2o3  6485  oasuc  6519  omsuc  6527  enpr2d  6873  phplem1  6910  fiunsnnn  6939  unsnfi  6977  fiintim  6987  fidcenumlemrks  7014  fidcenumlemr  7016  nnnninfeq2  7190  nninfwlpoimlemg  7236  pm54.43  7252  dju1en  7275  pw1nel3  7293  sucpw1nel3  7295  frecfzennn  10500  hashp1i  10884  ennnfonelemg  12563  ennnfonelemhdmp1  12569  ennnfonelemkh  12572  ennnfonelemhf1o  12573  bdcsuc  15442  bdeqsuc  15443  bj-sucexg  15484  bj-nntrans  15513  bj-nnelirr  15515  bj-omtrans  15518  nninfsellemdc  15570  nninfsellemsuc  15572