Theorem sssucid 6392

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

Syntax hints:   ∪ cun 3881   ⊆ wss 3883  {csn 4555  suc csuc 6312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-suc 6316

This theorem is referenced by:  trsuc  6399  limsssuc  7790  oaordi  8471  omeulem1  8507  oelim2  8521  nnaordi  8544  naddcllem  8602  phplem2  9129  php  9131  enp1i  9179  fiint  9227  cantnfval2  9581  cantnfle  9583  cantnfp1lem3  9592  cnfcomlem  9611  ttrclss  9632  ranksuc  9780  fseqenlem1  9937  pwsdompw  10116  fin1a2lem12  10324  canthp1lem2  10567  nosupbnd1  27696  nosupbnd2lem1  27697  noinfbnd1  27711  noinfbnd2lem1  27712  bdaypw2n0bndlem  28473  satfvsucsuc  35593  satffunlem2lem2  35634  satffunlem2  35636  limsucncmpi  36673  finxpreclem3  37755  dfsuccl4  38841  press  38866  suceldisj  39185  insucid  43848  minregex  43978  clsk1independent  44490  grur1cld  44676  suctrALT  45269  suctrALT2VD  45279  suctrALT2  45280  suctrALTcf  45365  suctrALTcfVD  45366  suctrALT3  45367