Theorem sssucid 6388

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

Syntax hints:   ∪ cun 3895   ⊆ wss 3897  {csn 4573  suc csuc 6308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914  df-suc 6312

This theorem is referenced by:  trsuc  6395  limsssuc  7780  oaordi  8461  omeulem1  8497  oelim2  8510  nnaordi  8533  naddcllem  8591  phplem2  9114  php  9116  enp1i  9163  fiint  9211  cantnfval2  9559  cantnfle  9561  cantnfp1lem3  9570  cnfcomlem  9589  ttrclss  9610  ranksuc  9758  fseqenlem1  9915  pwsdompw  10094  fin1a2lem12  10302  canthp1lem2  10544  nosupbnd1  27653  nosupbnd2lem1  27654  noinfbnd1  27668  noinfbnd2lem1  27669  satfvsucsuc  35409  satffunlem2lem2  35450  satffunlem2  35452  limsucncmpi  36487  finxpreclem3  37435  insucid  43444  minregex  43575  clsk1independent  44087  grur1cld  44273  suctrALT  44866  suctrALT2VD  44876  suctrALT2  44877  suctrALTcf  44962  suctrALTcfVD  44963  suctrALT3  44964