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

Theorem sssucid 4650
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 3502 . 2  |-  A  C_  ( A  u.  { A } )
2 df-suc 4579 . 2  |-  suc  A  =  ( A  u.  { A } )
31, 2sseqtr4i 3373 1  |-  A  C_  suc  A
Colors of variables: wff set class
Syntax hints:    u. cun 3310    C_ wss 3312   {csn 3806   suc csuc 4575
This theorem is referenced by:  trsuc  4657  suceloni  4784  limsssuc  4821  oaordi  6780  omeulem1  6816  oelim2  6829  nnaordi  6852  phplem4  7280  php  7282  onomeneq  7287  fiint  7374  cantnfval2  7613  cantnfle  7615  cantnfp1lem3  7625  cnfcomlem  7645  ranksuc  7780  fseqenlem1  7894  pwsdompw  8073  fin1a2lem12  8280  canthp1lem2  8517  nofulllem5  25615  limsucncmpi  26143  suctrALT2VD  28802  suctrALT2  28803  suctrALTcf  28888  suctrALTcfVD  28889  suctrALT3  28890
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-in 3319  df-ss 3326  df-suc 4579
  Copyright terms: Public domain W3C validator