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  27602  nosupbnd2lem1  27603  noinfbnd1  27617  noinfbnd2lem1  27618  satfvsucsuc  35325  satffunlem2lem2  35366  satffunlem2  35368  limsucncmpi  36406  finxpreclem3  37354  insucid  43365  minregex  43496  clsk1independent  44008  grur1cld  44194  suctrALT  44788  suctrALT2VD  44798  suctrALT2  44799  suctrALTcf  44884  suctrALTcfVD  44885  suctrALT3  44886