Theorem sssucid 6342

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

Step	Hyp	Ref	Expression
1		ssun1 4111	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝐴})
2		df-suc 6271	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
3	1, 2	sseqtrri 3963	1 ⊢ 𝐴 ⊆ suc 𝐴

Syntax hints:   ∪ cun 3890   ⊆ wss 3892  {csn 4567  suc csuc 6267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-un 3897  df-in 3899  df-ss 3909  df-suc 6271

This theorem is referenced by:  trsuc  6349  sucexeloni  7652  suceloniOLD  7654  limsssuc  7691  oaordi  8362  omeulem1  8398  oelim2  8411  nnaordi  8434  phplem2  8972  php  8974  phplem4OLD  8985  phpOLD  8987  onomeneq  8992  fiint  9069  cantnfval2  9405  cantnfle  9407  cantnfp1lem3  9416  cnfcomlem  9435  ttrclss  9456  ranksuc  9624  fseqenlem1  9781  pwsdompw  9961  fin1a2lem12  10168  canthp1lem2  10410  satfvsucsuc  33323  satffunlem2lem2  33364  satffunlem2  33366  naddcllem  33827  nosupbnd1  33913  nosupbnd2lem1  33914  noinfbnd1  33928  noinfbnd2lem1  33929  limsucncmpi  34630  finxpreclem3  35560  clsk1independent  41626  grur1cld  41820  suctrALT  42416  suctrALT2VD  42426  suctrALT2  42427  suctrALTcf  42512  suctrALTcfVD  42513  suctrALT3  42514