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

Theorem sssucid 4960
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

Proof of Theorem sssucid
StepHypRef Expression
1 ssun1 3666 . 2
2 df-suc 4889 . 2
31, 2sseqtr4i 3536 1
Colors of variables: wff setvar class
Syntax hints:  u.cun 3473  C_wss 3475  {csn 4029  succsuc 4885
This theorem is referenced by:  trsuc  4967  suceloni  6648  limsssuc  6685  oaordi  7214  omeulem1  7250  oelim2  7263  nnaordi  7286  phplem4  7719  php  7721  onomeneq  7727  fiint  7817  cantnfval2  8109  cantnfle  8111  cantnfp1lem3  8120  cantnfval2OLD  8139  cantnfleOLD  8141  cantnfp1lem3OLD  8146  cnfcomlem  8164  cnfcomlemOLD  8172  ranksuc  8304  fseqenlem1  8426  pwsdompw  8605  fin1a2lem12  8812  canthp1lem2  9052  nofulllem5  29466  limsucncmpi  29910  suctrALT  33626  suctrALT2VD  33636  suctrALT2  33637  suctrALTcf  33722  suctrALTcfVD  33723  suctrALT3  33724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482  df-ss 3489  df-suc 4889
  Copyright terms: Public domain W3C validator