Theorem sssucid 6405

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

Syntax hints:   ∪ cun 3887   ⊆ wss 3889  {csn 4567  suc csuc 6325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-suc 6329

This theorem is referenced by:  trsuc  6412  limsssuc  7801  oaordi  8481  omeulem1  8517  oelim2  8531  nnaordi  8554  naddcllem  8612  phplem2  9139  php  9141  enp1i  9189  fiint  9237  cantnfval2  9590  cantnfle  9592  cantnfp1lem3  9601  cnfcomlem  9620  ttrclss  9641  ranksuc  9789  fseqenlem1  9946  pwsdompw  10125  fin1a2lem12  10333  canthp1lem2  10576  nosupbnd1  27678  nosupbnd2lem1  27679  noinfbnd1  27693  noinfbnd2lem1  27694  bdaypw2n0bndlem  28455  satfvsucsuc  35547  satffunlem2lem2  35588  satffunlem2  35590  limsucncmpi  36627  finxpreclem3  37709  dfsuccl4  38795  press  38820  suceldisj  39139  insucid  43831  minregex  43961  clsk1independent  44473  grur1cld  44659  suctrALT  45252  suctrALT2VD  45262  suctrALT2  45263  suctrALTcf  45348  suctrALTcfVD  45349  suctrALT3  45350