Theorem sssucid 6414

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

Syntax hints:   ∪ cun 3912   ⊆ wss 3914  {csn 4589  suc csuc 6334

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 3449  df-un 3919  df-ss 3931  df-suc 6338

This theorem is referenced by:  trsuc  6421  sucexeloniOLD  7786  limsssuc  7826  oaordi  8510  omeulem1  8546  oelim2  8559  nnaordi  8582  naddcllem  8640  phplem2  9169  php  9171  enp1i  9224  fiint  9277  fiintOLD  9278  cantnfval2  9622  cantnfle  9624  cantnfp1lem3  9633  cnfcomlem  9652  ttrclss  9673  ranksuc  9818  fseqenlem1  9977  pwsdompw  10156  fin1a2lem12  10364  canthp1lem2  10606  nosupbnd1  27626  nosupbnd2lem1  27627  noinfbnd1  27641  noinfbnd2lem1  27642  satfvsucsuc  35352  satffunlem2lem2  35393  satffunlem2  35395  limsucncmpi  36433  finxpreclem3  37381  insucid  43392  minregex  43523  clsk1independent  44035  grur1cld  44221  suctrALT  44815  suctrALT2VD  44825  suctrALT2  44826  suctrALTcf  44911  suctrALTcfVD  44912  suctrALT3  44913