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

Theorem sssucid 4468
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 3339 . 2  |-  A  C_  ( A  u.  { A } )
2 df-suc 4397 . 2  |-  suc  A  =  ( A  u.  { A } )
31, 2sseqtr4i 3212 1  |-  A  C_  suc  A
Colors of variables: wff set class
Syntax hints:    u. cun 3151    C_ wss 3153   {csn 3641   suc csuc 4393
This theorem is referenced by:  trsuc  4475  suceloni  4603  limsssuc  4640  oaordi  6539  omeulem1  6575  oelim2  6588  nnaordi  6611  phplem4  7038  php  7040  onomeneq  7045  fiint  7128  cantnfval2  7365  cantnfle  7367  cantnfp1lem3  7377  cnfcomlem  7397  ranksuc  7532  fseqenlem1  7646  pwsdompw  7825  fin1a2lem12  8032  canthp1lem2  8270  axfelem13  23759  axfelem18  23764  limsucncmpi  24291  suctrALT2VD  27880  suctrALT2  27881  suctrALTcf  27966  suctrALTcfVD  27967  suctrALT3  27968  suctrALT4  27972
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158  df-in 3160  df-ss 3167  df-suc 4397
  Copyright terms: Public domain W3C validator