Theorem sssucid 4869

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 3581	. 2 |- A C_ ( A u. { A } )
2		df-suc 4798	. 2 |- suc A = ( A u. { A } )
3	1, 2	sseqtr4i 3450	1 |- A C_ suc A

Syntax hints:   u. cun 3387   C_ wss 3389   {csn 3944   suc csuc 4794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-un 3394  df-in 3396  df-ss 3403  df-suc 4798

This theorem is referenced by:  trsuc  4876  suceloni  6547  limsssuc  6584  oaordi  7113  omeulem1  7149  oelim2  7162  nnaordi  7185  phplem4  7618  php  7620  onomeneq  7626  fiint  7712  cantnfval2  8001  cantnfle  8003  cantnfp1lem3  8012  cantnfval2OLD  8031  cantnfleOLD  8033  cantnfp1lem3OLD  8038  cnfcomlem  8056  cnfcomlemOLD  8064  ranksuc  8196  fseqenlem1  8318  pwsdompw  8497  fin1a2lem12  8704  canthp1lem2  8942  nofulllem5  29631  limsucncmpi  30063  suctrALT  33972  suctrALT2VD  33982  suctrALT2  33983  suctrALTcf  34069  suctrALTcfVD  34070  suctrALT3  34071