Theorem sssucid 6464

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

Syntax hints:   ∪ cun 3949   ⊆ wss 3951  {csn 4626  suc csuc 6386

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-suc 6390

This theorem is referenced by:  trsuc  6471  sucexeloniOLD  7830  suceloniOLD  7832  limsssuc  7871  oaordi  8584  omeulem1  8620  oelim2  8633  nnaordi  8656  naddcllem  8714  phplem2  9245  php  9247  phplem4OLD  9257  phpOLD  9259  onomeneqOLD  9266  enp1i  9313  fiint  9366  fiintOLD  9367  cantnfval2  9709  cantnfle  9711  cantnfp1lem3  9720  cnfcomlem  9739  ttrclss  9760  ranksuc  9905  fseqenlem1  10064  pwsdompw  10243  fin1a2lem12  10451  canthp1lem2  10693  nosupbnd1  27759  nosupbnd2lem1  27760  noinfbnd1  27774  noinfbnd2lem1  27775  satfvsucsuc  35370  satffunlem2lem2  35411  satffunlem2  35413  limsucncmpi  36446  finxpreclem3  37394  insucid  43416  minregex  43547  clsk1independent  44059  grur1cld  44251  suctrALT  44846  suctrALT2VD  44856  suctrALT2  44857  suctrALTcf  44942  suctrALTcfVD  44943  suctrALT3  44944