Theorem sssucid 6451

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

Syntax hints:   ∪ cun 3942   ⊆ wss 3944  {csn 4630  suc csuc 6373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-un 3949  df-ss 3961  df-suc 6377

This theorem is referenced by:  trsuc  6458  sucexeloniOLD  7814  suceloniOLD  7816  limsssuc  7855  oaordi  8567  omeulem1  8603  oelim2  8616  nnaordi  8639  naddcllem  8697  phplem2  9233  php  9235  phplem4OLD  9245  phpOLD  9247  onomeneqOLD  9254  enp1i  9304  fiint  9350  cantnfval2  9694  cantnfle  9696  cantnfp1lem3  9705  cnfcomlem  9724  ttrclss  9745  ranksuc  9890  fseqenlem1  10049  pwsdompw  10229  fin1a2lem12  10436  canthp1lem2  10678  nosupbnd1  27693  nosupbnd2lem1  27694  noinfbnd1  27708  noinfbnd2lem1  27709  satfvsucsuc  35106  satffunlem2lem2  35147  satffunlem2  35149  limsucncmpi  36060  finxpreclem3  37003  insucid  42975  minregex  43106  clsk1independent  43618  grur1cld  43811  suctrALT  44407  suctrALT2VD  44417  suctrALT2  44418  suctrALTcf  44503  suctrALTcfVD  44504  suctrALT3  44505