Theorem sssucid 6475

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

Syntax hints:   ∪ cun 3974   ⊆ wss 3976  {csn 4648  suc csuc 6397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-suc 6401

This theorem is referenced by:  trsuc  6482  sucexeloniOLD  7846  suceloniOLD  7848  limsssuc  7887  oaordi  8602  omeulem1  8638  oelim2  8651  nnaordi  8674  naddcllem  8732  phplem2  9271  php  9273  phplem4OLD  9283  phpOLD  9285  onomeneqOLD  9292  enp1i  9341  fiint  9394  fiintOLD  9395  cantnfval2  9738  cantnfle  9740  cantnfp1lem3  9749  cnfcomlem  9768  ttrclss  9789  ranksuc  9934  fseqenlem1  10093  pwsdompw  10272  fin1a2lem12  10480  canthp1lem2  10722  nosupbnd1  27777  nosupbnd2lem1  27778  noinfbnd1  27792  noinfbnd2lem1  27793  satfvsucsuc  35333  satffunlem2lem2  35374  satffunlem2  35376  limsucncmpi  36411  finxpreclem3  37359  insucid  43365  minregex  43496  clsk1independent  44008  grur1cld  44201  suctrALT  44797  suctrALT2VD  44807  suctrALT2  44808  suctrALTcf  44893  suctrALTcfVD  44894  suctrALT3  44895