Definition df-suc 4436

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 4477). 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 4430	. 2 class suc 𝐴
3	1	csn 3643	. . 3 class {𝐴}
4	1, 3	cun 3172	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1373	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is referenced by:  suceq  4467  elsuci  4468  elsucg  4469  elsuc2g  4470  nfsuc  4473  suc0  4476  sucprc  4477  unisuc  4478  unisucg  4479  sssucid  4480  iunsuc  4485  sucexb  4563  ordsucim  4566  ordsucss  4570  2ordpr  4590  orddif  4613  sucprcreg  4615  elomssom  4671  omsinds  4688  tfrlemisucfn  6433  tfr1onlemsucfn  6449  tfrcllemsucfn  6462  rdgisuc1  6493  df2o3  6539  oasuc  6573  omsuc  6581  enpr2d  6935  phplem1  6974  fiunsnnn  7004  unsnfi  7042  fiintim  7054  fidcenumlemrks  7081  fidcenumlemr  7083  nnnninfeq2  7257  nninfwlpoimlemg  7303  pm54.43  7324  dju1en  7356  pw1nel3  7377  sucpw1nel3  7379  frecfzennn  10608  hashp1i  10992  ennnfonelemg  12889  ennnfonelemhdmp1  12895  ennnfonelemkh  12898  ennnfonelemhf1o  12899  bdcsuc  16015  bdeqsuc  16016  bj-sucexg  16057  bj-nntrans  16086  bj-nnelirr  16088  bj-omtrans  16091  nninfsellemdc  16149  nninfsellemsuc  16151