Theorem sssucid 6445

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

This proof depends on syntax axioms:   ∪ cun 3897   ⊆ wss 3899  {csn 4584  suc csuc 6364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-suc 6368

This theorem is used by:  trsuc  6452  limsssuc  7861  oaordi  8554  omeulem1  8590  oelim2  8604  nnaordi  8627  naddcllem  8685  phplem2  9220  php  9222  enp1i  9270  fiint  9318  cantnfval2  9670  cantnfle  9672  cantnfp1lem3  9681  cnfcomlem  9700  ttrclss  9721  ranksuc  9882  fseqenlem1  10103  pwsdompw  10281  fin1a2lem12  10489  canthp1lem2  10738  nosupbnd1  28071  nosupbnd2lem1  28072  noinfbnd1  28086  noinfbnd2lem1  28087  bdaypw2n0bndlem  28849  satfvsucsuc  36130  satffunlem2lem2  36171  satffunlem2  36173  nmulprop  36939  limsucncmpi  37233  finxpreclem3  38316  dfsuccl4  39406  press  39431  suceldisj  39750  insucid  44404  minregex  44534  clsk1independent  45045  grur1cld  45229  suctrALT  45807  suctrALT2VD  45817  suctrALT2  45818  suctrALTcf  45903  suctrALTcfVD  45904  suctrALT3  45905