Theorem sssucid 6397

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

Syntax hints:   ∪ cun 3897   ⊆ wss 3899  {csn 4578  suc csuc 6317

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 2115  ax-9 2123  ax-ext 2706

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916  df-suc 6321

This theorem is referenced by:  trsuc  6404  limsssuc  7790  oaordi  8471  omeulem1  8507  oelim2  8521  nnaordi  8544  naddcllem  8602  phplem2  9127  php  9129  enp1i  9177  fiint  9225  cantnfval2  9576  cantnfle  9578  cantnfp1lem3  9587  cnfcomlem  9606  ttrclss  9627  ranksuc  9775  fseqenlem1  9932  pwsdompw  10111  fin1a2lem12  10319  canthp1lem2  10562  nosupbnd1  27680  nosupbnd2lem1  27681  noinfbnd1  27695  noinfbnd2lem1  27696  bdaypw2n0s  28420  satfvsucsuc  35508  satffunlem2lem2  35549  satffunlem2  35551  limsucncmpi  36588  finxpreclem3  37537  dfsuccl4  38587  press  38611  insucid  43587  minregex  43717  clsk1independent  44229  grur1cld  44415  suctrALT  45008  suctrALT2VD  45018  suctrALT2  45019  suctrALTcf  45104  suctrALTcfVD  45105  suctrALT3  45106