Theorem sssucid 4905

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 3628	. 2 |- A C_ ( A u. { A } )
2		df-suc 4834	. 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 3986   suc csuc 4830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-un 3442  df-in 3444  df-ss 3451  df-suc 4834

This theorem is referenced by:  trsuc  4912  suceloni  6535  limsssuc  6572  oaordi  7096  omeulem1  7132  oelim2  7145  nnaordi  7168  phplem4  7604  php  7606  onomeneq  7612  fiint  7700  cantnfval2  7989  cantnfle  7991  cantnfp1lem3  8000  cantnfval2OLD  8019  cantnfleOLD  8021  cantnfp1lem3OLD  8026  cnfcomlem  8044  cnfcomlemOLD  8052  ranksuc  8184  fseqenlem1  8306  pwsdompw  8485  fin1a2lem12  8692  canthp1lem2  8932  nofulllem5  27992  limsucncmpi  28436  suctrALT  31895  suctrALT2VD  31905  suctrALT2  31906  suctrALTcf  31991  suctrALTcfVD  31992  suctrALT3  31993