Theorem sssucid 6399

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

Syntax hints:   ∪ cun 3899   ⊆ wss 3901  {csn 4580  suc csuc 6319

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-suc 6323

This theorem is referenced by:  trsuc  6406  limsssuc  7792  oaordi  8473  omeulem1  8509  oelim2  8523  nnaordi  8546  naddcllem  8604  phplem2  9129  php  9131  enp1i  9179  fiint  9227  cantnfval2  9578  cantnfle  9580  cantnfp1lem3  9589  cnfcomlem  9608  ttrclss  9629  ranksuc  9777  fseqenlem1  9934  pwsdompw  10113  fin1a2lem12  10321  canthp1lem2  10564  nosupbnd1  27682  nosupbnd2lem1  27683  noinfbnd1  27697  noinfbnd2lem1  27698  bdaypw2n0bndlem  28459  satfvsucsuc  35559  satffunlem2lem2  35600  satffunlem2  35602  limsucncmpi  36639  finxpreclem3  37598  dfsuccl4  38648  press  38672  insucid  43645  minregex  43775  clsk1independent  44287  grur1cld  44473  suctrALT  45066  suctrALT2VD  45076  suctrALT2  45077  suctrALTcf  45162  suctrALTcfVD  45163  suctrALT3  45164