Theorem sssucid 6447

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

This proof depends on syntax axioms:   ∪ cun 3904   ⊆ wss 3906  {csn 4591  suc csuc 6366

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-suc 6370

This theorem is used by:  trsuc  6454  limsssuc  7852  oaordi  8537  omeulem1  8573  oelim2  8587  nnaordi  8610  naddcllem  8668  phplem2  9196  php  9198  enp1i  9246  fiint  9293  cantnfval2  9645  cantnfle  9647  cantnfp1lem3  9656  cnfcomlem  9675  ttrclss  9696  ranksuc  9844  fseqenlem1  10024  pwsdompw  10202  fin1a2lem12  10410  canthp1lem2  10653  nosupbnd1  27929  nosupbnd2lem1  27930  noinfbnd1  27944  noinfbnd2lem1  27945  bdaypw2n0bndlem  28707  satfvsucsuc  35894  satffunlem2lem2  35935  satffunlem2  35937  nmulprop  36719  limsucncmpi  37013  finxpreclem3  38096  dfsuccl4  39181  press  39206  suceldisj  39525  insucid  44188  minregex  44318  clsk1independent  44830  grur1cld  45014  suctrALT  45592  suctrALT2VD  45602  suctrALT2  45603  suctrALTcf  45688  suctrALTcfVD  45689  suctrALT3  45690