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

Theorem sssucid 6236
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 4099 . 2 𝐴 ⊆ (𝐴 ∪ {𝐴})
2 df-suc 6165 . 2 suc 𝐴 = (𝐴 ∪ {𝐴})
31, 2sseqtrri 3952 1 𝐴 ⊆ suc 𝐴
Colors of variables: wff setvar class
Syntax hints:  cun 3879  wss 3881  {csn 4525  suc csuc 6161
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-suc 6165
This theorem is referenced by:  trsuc  6243  suceloni  7508  limsssuc  7545  oaordi  8155  omeulem1  8191  oelim2  8204  nnaordi  8227  phplem4  8683  php  8685  onomeneq  8693  fiint  8779  cantnfval2  9116  cantnfle  9118  cantnfp1lem3  9127  cnfcomlem  9146  ranksuc  9278  fseqenlem1  9435  pwsdompw  9615  fin1a2lem12  9822  canthp1lem2  10064  satfvsucsuc  32722  satffunlem2lem2  32763  satffunlem2  32765  nosupbday  33315  nosupbnd1  33324  nosupbnd2lem1  33325  limsucncmpi  33903  finxpreclem3  34807  clsk1independent  40744  grur1cld  40935  suctrALT  41527  suctrALT2VD  41537  suctrALT2  41538  suctrALTcf  41623  suctrALTcfVD  41624  suctrALT3  41625
  Copyright terms: Public domain W3C validator