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

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