Theorem sssucid 6028

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 3986	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝐴})
2		df-suc 5956	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
3	1, 2	sseqtr4i 3846	1 ⊢ 𝐴 ⊆ suc 𝐴

Syntax hints:   ∪ cun 3778   ⊆ wss 3780  {csn 4381  suc csuc 5952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-un 3785  df-in 3787  df-ss 3794  df-suc 5956

This theorem is referenced by:  trsuc  6035  suceloni  7253  limsssuc  7290  oaordi  7873  omeulem1  7909  oelim2  7922  nnaordi  7945  phplem4  8391  php  8393  onomeneq  8399  fiint  8486  cantnfval2  8823  cantnfle  8825  cantnfp1lem3  8834  cnfcomlem  8853  ranksuc  8985  fseqenlem1  9140  pwsdompw  9321  fin1a2lem12  9528  canthp1lem2  9770  nosupbday  32194  nosupbnd1  32203  nosupbnd2lem1  32204  limsucncmpi  32783  finxpreclem3  33565  clsk1independent  38862  suctrALT  39573  suctrALT2VD  39583  suctrALT2  39584  suctrALTcf  39670  suctrALTcfVD  39671  suctrALT3  39672