Theorem sssucid 6407

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 4132	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝐴})
2		df-suc 6331	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
3	1, 2	sseqtrri 3985	1 ⊢ 𝐴 ⊆ suc 𝐴

Syntax hints:   ∪ cun 3901   ⊆ wss 3903  {csn 4582  suc csuc 6327

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-suc 6331

This theorem is referenced by:  trsuc  6414  limsssuc  7802  oaordi  8483  omeulem1  8519  oelim2  8533  nnaordi  8556  naddcllem  8614  phplem2  9141  php  9143  enp1i  9191  fiint  9239  cantnfval2  9590  cantnfle  9592  cantnfp1lem3  9601  cnfcomlem  9620  ttrclss  9641  ranksuc  9789  fseqenlem1  9946  pwsdompw  10125  fin1a2lem12  10333  canthp1lem2  10576  nosupbnd1  27694  nosupbnd2lem1  27695  noinfbnd1  27709  noinfbnd2lem1  27710  bdaypw2n0bndlem  28471  satfvsucsuc  35581  satffunlem2lem2  35622  satffunlem2  35624  limsucncmpi  36661  finxpreclem3  37648  dfsuccl4  38725  press  38750  suceldisj  39069  insucid  43760  minregex  43890  clsk1independent  44402  grur1cld  44588  suctrALT  45181  suctrALT2VD  45191  suctrALT2  45192  suctrALTcf  45277  suctrALTcfVD  45278  suctrALT3  45279