Theorem sssucid 4955

Description: A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.)

Assertion

Ref	Expression
sssucid	|- A C_ suc A

Proof of Theorem sssucid

Step	Hyp	Ref	Expression
1		ssun1 3667	. 2 |- A C_ ( A u. { A } )
2		df-suc 4884	. 2 |- suc A = ( A u. { A } )
3	1, 2	sseqtr4i 3537	1 |- A C_ suc A

Syntax hints:   u. cun 3474   C_ wss 3476   {csn 4027   suc csuc 4880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-suc 4884

This theorem is referenced by:  trsuc  4962  suceloni  6626  limsssuc  6663  oaordi  7192  omeulem1  7228  oelim2  7241  nnaordi  7264  phplem4  7696  php  7698  onomeneq  7704  fiint  7793  cantnfval2  8084  cantnfle  8086  cantnfp1lem3  8095  cantnfval2OLD  8114  cantnfleOLD  8116  cantnfp1lem3OLD  8121  cnfcomlem  8139  cnfcomlemOLD  8147  ranksuc  8279  fseqenlem1  8401  pwsdompw  8580  fin1a2lem12  8787  canthp1lem2  9027  nofulllem5  29040  limsucncmpi  29484  suctrALT  32706  suctrALT2VD  32716  suctrALT2  32717  suctrALTcf  32802  suctrALTcfVD  32803  suctrALT3  32804