Theorem sssucid 6448

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

This proof depends on syntax axioms:   ⊆ wss 3896   ∪ cun 4148  {csn 4584  suc csuc 6367

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150  df-suc 6371

This theorem is used by:  trsuc  6455  limsssuc  7865  oaordi  8562  omeulem1  8598  oelim2  8612  nnaordi  8635  naddcllem  8693  phplem2  9228  php  9230  enp1i  9278  fiint  9326  cantnfval2  9677  cantnfle  9679  cantnfp1lem3  9688  cnfcomlem  9707  ttrclss  9728  ranksuc  9889  fseqenlem1  10110  pwsdompw  10288  fin1a2lem12  10496  canthp1lem2  10745  nosupbnd1  28080  nosupbnd2lem1  28081  noinfbnd1  28095  noinfbnd2lem1  28096  bdaypw2n0bndlem  28858  satfvsucsuc  36248  satffunlem2lem2  36289  satffunlem2  36291  nmulprop  37063  limsucncmpi  37357  finxpreclem3  38453  dfsuccl4  39543  press  39568  suceldisj  39887  insucid  44542  minregex  44672  clsk1independent  45183  grur1cld  45367  suctrALT  45944  suctrALT2VD  45954  suctrALT2  45955  suctrALTcf  46040  suctrALTcfVD  46041  suctrALT3  46042