Theorem sssucid 6440

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-suc 6363

This theorem is used by:  trsuc  6447  limsssuc  7847  oaordi  8534  omeulem1  8570  oelim2  8584  nnaordi  8607  naddcllem  8665  phplem2  9200  php  9202  enp1i  9250  fiint  9297  cantnfval2  9649  cantnfle  9651  cantnfp1lem3  9660  cnfcomlem  9679  ttrclss  9700  ranksuc  9848  fseqenlem1  10028  pwsdompw  10206  fin1a2lem12  10414  canthp1lem2  10663  nosupbnd1  27951  nosupbnd2lem1  27952  noinfbnd1  27966  noinfbnd2lem1  27967  bdaypw2n0bndlem  28729  satfvsucsuc  35945  satffunlem2lem2  35986  satffunlem2  35988  nmulprop  36771  limsucncmpi  37065  finxpreclem3  38148  dfsuccl4  39223  press  39248  suceldisj  39567  insucid  44245  minregex  44375  clsk1independent  44887  grur1cld  45071  suctrALT  45649  suctrALT2VD  45659  suctrALT2  45660  suctrALTcf  45745  suctrALTcfVD  45746  suctrALT3  45747