ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-suc GIF version

Definition df-suc 4174
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 4215). 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
StepHypRef Expression
1 cA . . 3 class 𝐴
21csuc 4168 . 2 class suc 𝐴
31csn 3431 . . 3 class {𝐴}
41, 3cun 2986 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1287 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
Colors of variables: wff set class
This definition is referenced by:  suceq  4205  elsuci  4206  elsucg  4207  elsuc2g  4208  nfsuc  4211  suc0  4214  sucprc  4215  unisuc  4216  unisucg  4217  sssucid  4218  iunsuc  4223  sucexb  4289  ordsucim  4292  ordsucss  4296  2ordpr  4315  orddif  4338  sucprcreg  4340  elnn  4395  omsinds  4410  tfrlemisucfn  6045  tfr1onlemsucfn  6061  tfrcllemsucfn  6074  rdgisuc1  6105  df2o3  6151  oasuc  6181  omsuc  6189  phplem1  6522  fiunsnnn  6551  unsnfi  6583  pm54.43  6765  frecfzennn  9764  hashp1i  10118  bdcsuc  11240  bdeqsuc  11241  bj-sucexg  11282  bj-nntrans  11315  bj-nnelirr  11317  bj-omtrans  11320  nninfsellemdc  11371  nninfsellemsuc  11373
  Copyright terms: Public domain W3C validator