Definition df-suc 4518

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 4559). 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 A = ( A u. { A } )

Detailed syntax breakdown of Definition df-suc

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	csuc 4512	. 2 class suc A
3	1	csn 3709	. . 3 class { A }
4	1, 3	cun 3218	. 2 class ( A u. { A } )
5	2, 4	wceq 1402	1 wff suc A = ( A u. { A } )

This definition is used by:  suceq  4549  elsuci  4550  elsucg  4551  elsuc2g  4552  nfsuc  4555  suc0  4558  sucprc  4559  unisuc  4560  unisucg  4561  sssucid  4562  iunsuc  4567  sucexb  4646  ordsucim  4649  ordsucss  4653  2ordpr  4673  orddif  4696  sucprcreg  4698  elomssom  4754  omsinds  4771  tfrlemisucfn  6600  tfr1onlemsucfn  6616  tfrcllemsucfn  6629  rdgisuc1  6660  df2o3  6707  oasuc  6742  omsuc  6750  enpr2d  7117  phplem1  7159  fiunsnnn  7191  unsnfi  7232  fiintim  7244  fidcenumlemrks  7277  fidcenumlemr  7279  nnnninfeq2  7475  nninfwlpoimlemg  7521  pm54.43  7542  dju1en  7575  pw1nel3  7596  sucpw1nel3  7598  frecfzennn  10883  hashp1i  11272  ennnfonelemg  13351  ennnfonelemhdmp1  13357  ennnfonelemkh  13360  ennnfonelemhf1o  13361  bdcsuc  17128  bdeqsuc  17129  bj-sucexg  17170  bj-nntrans  17199  bj-nnelirr  17201  bj-omtrans  17204  nninfsellemdc  17276  nninfsellemsuc  17278