Theorem sssucid 6400

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

Syntax hints:   ∪ cun 3888   ⊆ wss 3890  {csn 4568  suc csuc 6320

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 3432  df-un 3895  df-ss 3907  df-suc 6324

This theorem is referenced by:  trsuc  6407  limsssuc  7795  oaordi  8475  omeulem1  8511  oelim2  8525  nnaordi  8548  naddcllem  8606  phplem2  9133  php  9135  enp1i  9183  fiint  9231  cantnfval2  9584  cantnfle  9586  cantnfp1lem3  9595  cnfcomlem  9614  ttrclss  9635  ranksuc  9783  fseqenlem1  9940  pwsdompw  10119  fin1a2lem12  10327  canthp1lem2  10570  nosupbnd1  27695  nosupbnd2lem1  27696  noinfbnd1  27710  noinfbnd2lem1  27711  bdaypw2n0bndlem  28472  satfvsucsuc  35566  satffunlem2lem2  35607  satffunlem2  35609  limsucncmpi  36646  finxpreclem3  37726  dfsuccl4  38812  press  38837  suceldisj  39156  insucid  43852  minregex  43982  clsk1independent  44494  grur1cld  44680  suctrALT  45273  suctrALT2VD  45283  suctrALT2  45284  suctrALTcf  45369  suctrALTcfVD  45370  suctrALT3  45371