Theorem sssucid 5517

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

Syntax hints:   u. cun 3435   C_ wss 3437   {csn 3997   suc csuc 5442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-un 3442  df-in 3444  df-ss 3451  df-suc 5446

This theorem is referenced by:  trsuc  5524  suceloni  6652  limsssuc  6689  oaordi  7253  omeulem1  7289  oelim2  7302  nnaordi  7325  phplem4  7758  php  7760  onomeneq  7766  fiint  7852  cantnfval2  8177  cantnfle  8179  cantnfp1lem3  8188  cnfcomlem  8207  ranksuc  8339  fseqenlem1  8457  pwsdompw  8636  fin1a2lem12  8843  canthp1lem2  9080  nofulllem5  30594  limsucncmpi  31104  finxpreclem3  31743  suctrALT  37127  suctrALT2VD  37137  suctrALT2  37138  suctrALTcf  37224  suctrALTcfVD  37225  suctrALT3  37226