Theorem sssucid 6417

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

Syntax hints:   ∪ cun 3915   ⊆ wss 3917  {csn 4592  suc csuc 6337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-suc 6341

This theorem is referenced by:  trsuc  6424  sucexeloniOLD  7789  limsssuc  7829  oaordi  8513  omeulem1  8549  oelim2  8562  nnaordi  8585  naddcllem  8643  phplem2  9175  php  9177  enp1i  9231  fiint  9284  fiintOLD  9285  cantnfval2  9629  cantnfle  9631  cantnfp1lem3  9640  cnfcomlem  9659  ttrclss  9680  ranksuc  9825  fseqenlem1  9984  pwsdompw  10163  fin1a2lem12  10371  canthp1lem2  10613  nosupbnd1  27633  nosupbnd2lem1  27634  noinfbnd1  27648  noinfbnd2lem1  27649  satfvsucsuc  35359  satffunlem2lem2  35400  satffunlem2  35402  limsucncmpi  36440  finxpreclem3  37388  insucid  43399  minregex  43530  clsk1independent  44042  grur1cld  44228  suctrALT  44822  suctrALT2VD  44832  suctrALT2  44833  suctrALTcf  44918  suctrALTcfVD  44919  suctrALT3  44920