Theorem sssucid 6450

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

This proof depends on syntax axioms:   ∪ cun 3906   ⊆ wss 3908  {csn 4594  suc csuc 6369

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 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-suc 6373

This theorem is used by:  trsuc  6457  limsssuc  7855  oaordi  8540  omeulem1  8576  oelim2  8590  nnaordi  8613  naddcllem  8671  phplem2  9199  php  9201  enp1i  9249  fiint  9296  cantnfval2  9648  cantnfle  9650  cantnfp1lem3  9659  cnfcomlem  9678  ttrclss  9699  ranksuc  9847  fseqenlem1  10027  pwsdompw  10205  fin1a2lem12  10413  canthp1lem2  10656  nosupbnd1  27915  nosupbnd2lem1  27916  noinfbnd1  27930  noinfbnd2lem1  27931  bdaypw2n0bndlem  28693  satfvsucsuc  35877  satffunlem2lem2  35918  satffunlem2  35920  nmulprop  36702  limsucncmpi  36996  finxpreclem3  38079  dfsuccl4  39163  press  39188  suceldisj  39507  insucid  44170  minregex  44300  clsk1independent  44812  grur1cld  44996  suctrALT  45574  suctrALT2VD  45584  suctrALT2  45585  suctrALTcf  45670  suctrALTcfVD  45671  suctrALT3  45672