Theorem sssucid 6343

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

Syntax hints:   ∪ cun 3885   ⊆ wss 3887  {csn 4561  suc csuc 6268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-suc 6272

This theorem is referenced by:  trsuc  6350  sucexeloni  7658  suceloniOLD  7660  limsssuc  7697  oaordi  8377  omeulem1  8413  oelim2  8426  nnaordi  8449  phplem2  8991  php  8993  phplem4OLD  9003  phpOLD  9005  onomeneqOLD  9012  fiint  9091  cantnfval2  9427  cantnfle  9429  cantnfp1lem3  9438  cnfcomlem  9457  ttrclss  9478  ranksuc  9623  fseqenlem1  9780  pwsdompw  9960  fin1a2lem12  10167  canthp1lem2  10409  satfvsucsuc  33327  satffunlem2lem2  33368  satffunlem2  33370  naddcllem  33831  nosupbnd1  33917  nosupbnd2lem1  33918  noinfbnd1  33932  noinfbnd2lem1  33933  limsucncmpi  34634  finxpreclem3  35564  minregex  41141  clsk1independent  41656  grur1cld  41850  suctrALT  42446  suctrALT2VD  42456  suctrALT2  42457  suctrALTcf  42542  suctrALTcfVD  42543  suctrALT3  42544