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

Definition df-suc 4261
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 4302). 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 4255 . 2 class suc 𝐴
31csn 3495 . . 3 class {𝐴}
41, 3cun 3037 . 2 class (𝐴 ∪ {𝐴})
52, 4wceq 1314 1 wff suc 𝐴 = (𝐴 ∪ {𝐴})
Colors of variables: wff set class
This definition is referenced by:  suceq  4292  elsuci  4293  elsucg  4294  elsuc2g  4295  nfsuc  4298  suc0  4301  sucprc  4302  unisuc  4303  unisucg  4304  sssucid  4305  iunsuc  4310  sucexb  4381  ordsucim  4384  ordsucss  4388  2ordpr  4407  orddif  4430  sucprcreg  4432  elnn  4487  omsinds  4503  tfrlemisucfn  6187  tfr1onlemsucfn  6203  tfrcllemsucfn  6216  rdgisuc1  6247  df2o3  6293  oasuc  6326  omsuc  6334  enpr2d  6677  phplem1  6712  fiunsnnn  6741  unsnfi  6773  fiintim  6783  fidcenumlemrks  6807  fidcenumlemr  6809  pm54.43  7012  dju1en  7033  frecfzennn  10139  hashp1i  10496  ennnfonelemg  11811  ennnfonelemhdmp1  11817  ennnfonelemkh  11820  ennnfonelemhf1o  11821  bdcsuc  12880  bdeqsuc  12881  bj-sucexg  12922  bj-nntrans  12951  bj-nnelirr  12953  bj-omtrans  12956  nninfsellemdc  13008  nninfsellemsuc  13010
  Copyright terms: Public domain W3C validator