Theorem sssucid 6466

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

Syntax hints:   ∪ cun 3961   ⊆ wss 3963  {csn 4631  suc csuc 6388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980  df-suc 6392

This theorem is referenced by:  trsuc  6473  sucexeloniOLD  7830  suceloniOLD  7832  limsssuc  7871  oaordi  8583  omeulem1  8619  oelim2  8632  nnaordi  8655  naddcllem  8713  phplem2  9243  php  9245  phplem4OLD  9255  phpOLD  9257  onomeneqOLD  9264  enp1i  9311  fiint  9364  fiintOLD  9365  cantnfval2  9707  cantnfle  9709  cantnfp1lem3  9718  cnfcomlem  9737  ttrclss  9758  ranksuc  9903  fseqenlem1  10062  pwsdompw  10241  fin1a2lem12  10449  canthp1lem2  10691  nosupbnd1  27774  nosupbnd2lem1  27775  noinfbnd1  27789  noinfbnd2lem1  27790  satfvsucsuc  35350  satffunlem2lem2  35391  satffunlem2  35393  limsucncmpi  36428  finxpreclem3  37376  insucid  43393  minregex  43524  clsk1independent  44036  grur1cld  44228  suctrALT  44824  suctrALT2VD  44834  suctrALT2  44835  suctrALTcf  44920  suctrALTcfVD  44921  suctrALT3  44922