Theorem sssucid 6270

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

Syntax hints:   ∪ cun 3936   ⊆ wss 3938  {csn 4569  suc csuc 6195

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-in 3945  df-ss 3954  df-suc 6199

This theorem is referenced by:  trsuc  6277  suceloni  7530  limsssuc  7567  oaordi  8174  omeulem1  8210  oelim2  8223  nnaordi  8246  phplem4  8701  php  8703  onomeneq  8710  fiint  8797  cantnfval2  9134  cantnfle  9136  cantnfp1lem3  9145  cnfcomlem  9164  ranksuc  9296  fseqenlem1  9452  pwsdompw  9628  fin1a2lem12  9835  canthp1lem2  10077  satfvsucsuc  32614  satffunlem2lem2  32655  satffunlem2  32657  nosupbday  33207  nosupbnd1  33216  nosupbnd2lem1  33217  limsucncmpi  33795  finxpreclem3  34676  clsk1independent  40403  grur1cld  40575  suctrALT  41167  suctrALT2VD  41177  suctrALT2  41178  suctrALTcf  41263  suctrALTcfVD  41264  suctrALT3  41265