MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sssucid Structured version   Unicode version

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
StepHypRef Expression
1 ssun1 3581 . 2  |-  A  C_  ( A  u.  { A } )
2 df-suc 4798 . 2  |-  suc  A  =  ( A  u.  { A } )
31, 2sseqtr4i 3450 1  |-  A  C_  suc  A
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator