Definition df-suc 4516

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 4557). 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 4510	. 2 class suc 𝐴
3	1	csn 3709	. . 3 class {𝐴}
4	1, 3	cun 3218	. 2 class (𝐴 ∪ {𝐴})
5	2, 4	wceq 1402	1 wff suc 𝐴 = (𝐴 ∪ {𝐴})

This definition is used by:  suceq  4547  elsuci  4548  elsucg  4549  elsuc2g  4550  nfsuc  4553  suc0  4556  sucprc  4557  unisuc  4558  unisucg  4559  sssucid  4560  iunsuc  4565  sucexb  4644  ordsucim  4647  ordsucss  4651  2ordpr  4671  orddif  4694  sucprcreg  4696  elomssom  4752  omsinds  4769  tfrlemisucfn  6595  tfr1onlemsucfn  6611  tfrcllemsucfn  6624  rdgisuc1  6655  df2o3  6702  oasuc  6737  omsuc  6745  enpr2d  7111  phplem1  7153  fiunsnnn  7185  unsnfi  7226  fiintim  7238  fidcenumlemrks  7270  fidcenumlemr  7272  nnnninfeq2  7469  nninfwlpoimlemg  7515  pm54.43  7536  dju1en  7569  pw1nel3  7590  sucpw1nel3  7592  frecfzennn  10863  hashp1i  11251  ennnfonelemg  13294  ennnfonelemhdmp1  13300  ennnfonelemkh  13303  ennnfonelemhf1o  13304  bdcsuc  16906  bdeqsuc  16907  bj-sucexg  16948  bj-nntrans  16977  bj-nnelirr  16979  bj-omtrans  16982  nninfsellemdc  17053  nninfsellemsuc  17055