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

Theorem sssucid 5503
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 3599 . 2  |-  A  C_  ( A  u.  { A } )
2 df-suc 5432 . 2  |-  suc  A  =  ( A  u.  { A } )
31, 2sseqtr4i 3467 1  |-  A  C_  suc  A
Colors of variables: wff setvar class
Syntax hints:    u. cun 3404    C_ wss 3406   {csn 3970   suc csuc 5428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-un 3411  df-in 3413  df-ss 3420  df-suc 5432
This theorem is referenced by:  trsuc  5510  suceloni  6645  limsssuc  6682  oaordi  7252  omeulem1  7288  oelim2  7301  nnaordi  7324  phplem4  7759  php  7761  onomeneq  7767  fiint  7853  cantnfval2  8179  cantnfle  8181  cantnfp1lem3  8190  cnfcomlem  8209  ranksuc  8341  fseqenlem1  8460  pwsdompw  8639  fin1a2lem12  8846  canthp1lem2  9083  nofulllem5  30607  limsucncmpi  31117  finxpreclem3  31797  suctrALT  37232  suctrALT2VD  37242  suctrALT2  37243  suctrALTcf  37329  suctrALTcfVD  37330  suctrALT3  37331
  Copyright terms: Public domain W3C validator