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

Theorem sssucid 4427
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 3299 . 2  |-  A  C_  ( A  u.  { A } )
2 df-suc 4356 . 2  |-  suc  A  =  ( A  u.  { A } )
31, 2sseqtr4i 3172 1  |-  A  C_  suc  A
Colors of variables: wff set class
Syntax hints:    u. cun 3111    C_ wss 3113   {csn 3600   suc csuc 4352
This theorem is referenced by:  trsuc  4434  suceloni  4562  limsssuc  4599  oaordi  6498  omeulem1  6534  oelim2  6547  nnaordi  6570  phplem4  6997  php  6999  onomeneq  7004  fiint  7087  cantnfval2  7324  cantnfle  7326  cantnfp1lem3  7336  cnfcomlem  7356  ranksuc  7491  fseqenlem1  7605  pwsdompw  7784  fin1a2lem12  7991  canthp1lem2  8229  axfelem13  23713  axfelem18  23718  limsucncmpi  24245  suctrALT2VD  27646  suctrALT2  27647  suctrALTcf  27732  suctrALTcfVD  27733  suctrALT3  27734  suctrALT4  27738
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-un 3118  df-in 3120  df-ss 3127  df-suc 4356
  Copyright terms: Public domain W3C validator