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

Theorem sssucid 5800
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 𝐴 ⊆ suc 𝐴

Proof of Theorem sssucid
StepHypRef Expression
1 ssun1 3774 . 2 𝐴 ⊆ (𝐴 ∪ {𝐴})
2 df-suc 5727 . 2 suc 𝐴 = (𝐴 ∪ {𝐴})
31, 2sseqtr4i 3636 1 𝐴 ⊆ suc 𝐴
Colors of variables: wff setvar class
Syntax hints:  cun 3570  wss 3572  {csn 4175  suc csuc 5723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-un 3577  df-in 3579  df-ss 3586  df-suc 5727
This theorem is referenced by:  trsuc  5808  suceloni  7010  limsssuc  7047  oaordi  7623  omeulem1  7659  oelim2  7672  nnaordi  7695  phplem4  8139  php  8141  onomeneq  8147  fiint  8234  cantnfval2  8563  cantnfle  8565  cantnfp1lem3  8574  cnfcomlem  8593  ranksuc  8725  fseqenlem1  8844  pwsdompw  9023  fin1a2lem12  9230  canthp1lem2  9472  nosupbday  31835  nosupbnd1  31844  nosupbnd2lem1  31845  limsucncmpi  32428  finxpreclem3  33210  clsk1independent  38170  suctrALT  38887  suctrALT2VD  38897  suctrALT2  38898  suctrALTcf  38984  suctrALTcfVD  38985  suctrALT3  38986
  Copyright terms: Public domain W3C validator