Theorem sssucid 6444

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

Syntax hints:   ∪ cun 3911   ⊆ wss 3913  {csn 4594  suc csuc 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-suc 6367

This theorem is referenced by:  trsuc  6451  limsssuc  7845  oaordi  8530  omeulem1  8566  oelim2  8580  nnaordi  8603  naddcllem  8661  phplem2  9188  php  9190  enp1i  9238  fiint  9285  cantnfval2  9637  cantnfle  9639  cantnfp1lem3  9648  cnfcomlem  9667  ttrclss  9688  ranksuc  9836  fseqenlem1  10007  pwsdompw  10185  fin1a2lem12  10394  canthp1lem2  10637  nosupbnd1  27843  nosupbnd2lem1  27844  noinfbnd1  27858  noinfbnd2lem1  27859  bdaypw2n0bndlem  28621  satfvsucsuc  35755  satffunlem2lem2  35796  satffunlem2  35798  nmulprop  36580  limsucncmpi  36844  finxpreclem3  37926  dfsuccl4  39012  press  39037  suceldisj  39356  insucid  44021  minregex  44151  clsk1independent  44663  grur1cld  44847  suctrALT  45425  suctrALT2VD  45435  suctrALT2  45436  suctrALTcf  45521  suctrALTcfVD  45522  suctrALT3  45523