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

Theorem sssucid 4469
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 3338 . 2  |-  A  C_  ( A  u.  { A } )
2 df-suc 4398 . 2  |-  suc  A  =  ( A  u.  { A } )
31, 2sseqtr4i 3211 1  |-  A  C_  suc  A
Colors of variables: wff set class
Syntax hints:    u. cun 3150    C_ wss 3152   {csn 3640   suc csuc 4394
This theorem is referenced by:  trsuc  4476  suceloni  4604  limsssuc  4641  oaordi  6544  omeulem1  6580  oelim2  6593  nnaordi  6616  phplem4  7043  php  7045  onomeneq  7050  fiint  7133  cantnfval2  7370  cantnfle  7372  cantnfp1lem3  7382  cnfcomlem  7402  ranksuc  7537  fseqenlem1  7651  pwsdompw  7830  fin1a2lem12  8037  canthp1lem2  8275  nofulllem5  24360  limsucncmpi  24884  suctrALT2VD  28612  suctrALT2  28613  suctrALTcf  28698  suctrALTcfVD  28699  suctrALT3  28700  suctrALT4  28704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-suc 4398
  Copyright terms: Public domain W3C validator