Theorem sssucid 4945

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

Syntax hints:   u. cun 3459   C_ wss 3461   {csn 4014   suc csuc 4870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-in 3468  df-ss 3475  df-suc 4874

This theorem is referenced by:  trsuc  4952  suceloni  6633  limsssuc  6670  oaordi  7197  omeulem1  7233  oelim2  7246  nnaordi  7269  phplem4  7701  php  7703  onomeneq  7709  fiint  7799  cantnfval2  8091  cantnfle  8093  cantnfp1lem3  8102  cantnfval2OLD  8121  cantnfleOLD  8123  cantnfp1lem3OLD  8128  cnfcomlem  8146  cnfcomlemOLD  8154  ranksuc  8286  fseqenlem1  8408  pwsdompw  8587  fin1a2lem12  8794  canthp1lem2  9034  nofulllem5  29442  limsucncmpi  29886  suctrALT  33494  suctrALT2VD  33504  suctrALT2  33505  suctrALTcf  33590  suctrALTcfVD  33591  suctrALT3  33592