Theorem sssucid 6402

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

Syntax hints:   ∪ cun 3909   ⊆ wss 3911  {csn 4585  suc csuc 6322

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-ss 3928  df-suc 6326

This theorem is referenced by:  trsuc  6409  sucexeloniOLD  7766  limsssuc  7806  oaordi  8487  omeulem1  8523  oelim2  8536  nnaordi  8559  naddcllem  8617  phplem2  9146  php  9148  enp1i  9200  fiint  9253  fiintOLD  9254  cantnfval2  9598  cantnfle  9600  cantnfp1lem3  9609  cnfcomlem  9628  ttrclss  9649  ranksuc  9794  fseqenlem1  9953  pwsdompw  10132  fin1a2lem12  10340  canthp1lem2  10582  nosupbnd1  27659  nosupbnd2lem1  27660  noinfbnd1  27674  noinfbnd2lem1  27675  satfvsucsuc  35345  satffunlem2lem2  35386  satffunlem2  35388  limsucncmpi  36426  finxpreclem3  37374  insucid  43385  minregex  43516  clsk1independent  44028  grur1cld  44214  suctrALT  44808  suctrALT2VD  44818  suctrALT2  44819  suctrALTcf  44904  suctrALTcfVD  44905  suctrALT3  44906