Theorem sssucid 6428

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

Syntax hints:   ∪ cun 3902   ⊆ wss 3904  {csn 4582  suc csuc 6348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-suc 6352

This theorem is referenced by:  trsuc  6435  limsssuc  7830  oaordi  8515  omeulem1  8551  oelim2  8565  nnaordi  8588  naddcllem  8646  phplem2  9173  php  9175  enp1i  9223  fiint  9271  cantnfval2  9624  cantnfle  9626  cantnfp1lem3  9635  cnfcomlem  9654  ttrclss  9675  ranksuc  9823  fseqenlem1  9980  pwsdompw  10159  fin1a2lem12  10368  canthp1lem2  10611  nosupbnd1  27778  nosupbnd2lem1  27779  noinfbnd1  27793  noinfbnd2lem1  27794  bdaypw2n0bndlem  28556  satfvsucsuc  35715  satffunlem2lem2  35756  satffunlem2  35758  nmulprop  36540  limsucncmpi  36805  finxpreclem3  37887  dfsuccl4  38973  press  38998  suceldisj  39317  insucid  43980  minregex  44110  clsk1independent  44622  grur1cld  44808  suctrALT  45401  suctrALT2VD  45411  suctrALT2  45412  suctrALTcf  45497  suctrALTcfVD  45498  suctrALT3  45499