Theorem sssucid 6268

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

Syntax hints:   ∪ cun 3851   ⊆ wss 3853  {csn 4527  suc csuc 6193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-in 3860  df-ss 3870  df-suc 6197

This theorem is referenced by:  trsuc  6275  suceloni  7570  limsssuc  7607  oaordi  8252  omeulem1  8288  oelim2  8301  nnaordi  8324  phplem4  8806  php  8808  onomeneq  8845  fiint  8926  cantnfval2  9262  cantnfle  9264  cantnfp1lem3  9273  cnfcomlem  9292  ranksuc  9446  fseqenlem1  9603  pwsdompw  9783  fin1a2lem12  9990  canthp1lem2  10232  satfvsucsuc  32994  satffunlem2lem2  33035  satffunlem2  33037  naddcllem  33517  nosupbnd1  33603  nosupbnd2lem1  33604  noinfbnd1  33618  noinfbnd2lem1  33619  limsucncmpi  34320  finxpreclem3  35250  clsk1independent  41274  grur1cld  41464  suctrALT  42060  suctrALT2VD  42070  suctrALT2  42071  suctrALTcf  42156  suctrALTcfVD  42157  suctrALT3  42158