Theorem sssucid 6396

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

Syntax hints:   ∪ cun 3897   ⊆ wss 3899  {csn 4577  suc csuc 6316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-un 3904  df-ss 3916  df-suc 6320

This theorem is referenced by:  trsuc  6403  limsssuc  7789  oaordi  8470  omeulem1  8506  oelim2  8519  nnaordi  8542  naddcllem  8600  phplem2  9124  php  9126  enp1i  9173  fiint  9221  cantnfval2  9569  cantnfle  9571  cantnfp1lem3  9580  cnfcomlem  9599  ttrclss  9620  ranksuc  9768  fseqenlem1  9925  pwsdompw  10104  fin1a2lem12  10312  canthp1lem2  10554  nosupbnd1  27663  nosupbnd2lem1  27664  noinfbnd1  27678  noinfbnd2lem1  27679  satfvsucsuc  35420  satffunlem2lem2  35461  satffunlem2  35463  limsucncmpi  36500  finxpreclem3  37448  dfsuccl4  38497  press  38521  insucid  43510  minregex  43641  clsk1independent  44153  grur1cld  44339  suctrALT  44932  suctrALT2VD  44942  suctrALT2  44943  suctrALTcf  45028  suctrALTcfVD  45029  suctrALT3  45030